Satz von Herbrand

Der Satz von Herbrand ist ein Satz der mathematischen Logik, der 1930 vom französischen Logiker Jacques Herbrand publiziert wurde. Er macht eine Aussage darüber, wann eine prädikatenlogische Formel ohne Gleichheit allgemeingültig oder erfüllbar ist und erlaubt eine Reduktion auf Allgemeingültigkeit oder Erfüllbarkeit in der Aussagenlogik.

Der Satz besagt:

Sei ${\displaystyle \varphi }$ eine geschlossene prädikatenlogische Formel ohne Gleichheit.

Dann gibt es eine (aus ${\displaystyle \varphi }$ berechenbare) quantorenfreie Formel ${\displaystyle \psi }$, sodass gilt: ${\displaystyle \varphi }$ ist eine Tautologie genau dann, wenn es variablenfreie Substitutionsinstanzen ${\displaystyle \psi _{1},\psi _{2},\dots ,\psi _{n}}$ von ${\displaystyle \psi }$ gibt, sodass

${\displaystyle \psi _{1}\vee \psi _{2}\vee \dots \vee \psi _{n}}$

eine aussagenlogische Tautologie ist.