Entscheidungsproblem (Prädikatenlogik)

Das Problem zu entscheiden, ob eine gegebene FO-Formel allgemeingültig (oder erfüllbar) ist.
Satz (Church, Turing 1936/37): Das Allgemeingültigkeitsproblem der Prädikatenlogik ist unentscheidbar. Es gibt keinen Algorithmus, der für jede Formel in endlicher Zeit korrekt Ja oder Nein liefert.
Dies steht im Gegensatz zur Aussagenlogik, die entscheidbar ist.