herbrandscher Satz

von dem französischen Mathematiker und Logiker Jacques Herbrand (* 1908, † 1931) 1929 bewiesener Satz: Ist A eine Aussage der Prädikatenlogik, so lässt sich eine Disjunktion A₁ ∨ ... ∨ A_n von aussagenlogischen Aussagen konstruieren (»herbrandsche Disjunktion«) mit folgender Eigenschaft: Ist A beweisbar, so auch A₁ ∨ ... ∨