Математическая логика и теория алгоритмов

1.12 Теоремы об ИП первого порядка

назад | оглавление | вперёд

 

       Исчисление предикатов, которое не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которое содержит предметные константы и (или), функторы и (или) предикаты и связывающие их собственные аксиомы, называется прикладным. Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы, предикаты или иные множества объектов, называются исчислениями высших порядков.

       Значение формулы определено лишь тогда, когда задана какая-нибудь интерпретация входящих в нее символов. Под интерпретацией (моделью) будем понимать предметную область с определенными на ней n-арными предикатами.

       Дадим некоторые определения:

Теорема.Если формула А – тавтология в ИП, то А является теоремой в ИП и может быть введена с использованием лишь аксиом A1,A2,A3 и правила вывода МР(Modus Ponens).
       Теорема не требует доказательства.

Теорема. (Теорема Геделя о полноте исчисления предикатов). Формула доказуема в исчислении предикатов тогда и только тогда, когда формула общезначима.
Доказательство.Покажем только необходимость утверждения, поскольку доказательство достаточности более сложное. Аксиомы ИП являются общезначимыми формулами. При использовании правил вывода для общезначимых формул можно получить только общезначимую формулу.
       Теорема доказана.

Теорема. (Теорема Черча о неразрешимости исчисления предикатов). ИП является полуразрешимой теорией.
       Теорема не требует доказательства.


назад | оглавление | вперёд