Теорема 2.5 (Гёдель, 1930). Для исчисления предикатов спра-
ведливо утверждение:
|= А тогда и только тогда, когда |-A.
Теорема 2.6. Исчисление предикатов - полная теория.
Доказательство. Следует из утверждения «|= А влечет |- А» те-
оремы 2.5.
Теорема 2.7. Исчисление предикатов - непротиворечивая тео-
рия.
Доказательство. Следует из утверждения "|- A влечет |= А»
теоремы 2.5. Действительно, если бы была доказуема формула
А = В&неВ, то была бы общезначимой формула В&неВ. Но послед-
няя формула ложна.