Математическая логика и теория алгоритмов
|
       Исчисление предикатов, которое не содержит предметных констант, функторов, предикатов и собственных аксиом, называется чистым. Исчисление предикатов, которое содержит предметные константы и (или), функторы и (или) предикаты и связывающие их собственные аксиомы, называется прикладным. Исчисление предикатов, в котором кванторы могут связывать только предметные переменные, но не могут связывать функторы, предикаты или иные множества объектов, называются исчислениями высших порядков.
       Значение формулы определено лишь тогда, когда задана какая-нибудь интерпретация входящих в нее символов. Под интерпретацией (моделью) будем понимать предметную область
с определенными на ней n-арными предикатами.
       Дадим некоторые определения:
- Формула А выполнима в данной модели, если существует набор
значений свободных переменных
формулы А;
- Формула А истинна в данной модели, если она принимает значение Истина на любом наборе
значений своих свободных переменных
;
- Формула A общезначима или (тождественно истинна в логике предикатов), если она истинна в любой интерпретации;
- Формула A выполнима (в логике предикатов), если существует модель, в которой A выполнима;
- Формула А – тавтология в ИП, если тавтологией является формула, полученная из А опусканием всех кванторов и термов вместе со всеми соответствующими скобками и переменными. Например, аксиома
является тавтологией, поскольку формула
тавтология.
Теорема.Если формула А – тавтология в ИП, то А является теоремой в ИП и может быть введена с использованием лишь аксиом A1,A2,A3 и правила вывода МР(Modus Ponens).
       Теорема не требует доказательства.
Теорема. (Теорема Геделя о полноте исчисления предикатов). Формула доказуема в исчислении предикатов тогда и только тогда, когда формула общезначима.
Доказательство.Покажем только необходимость утверждения, поскольку доказательство достаточности более сложное. Аксиомы ИП являются общезначимыми формулами. При использовании правил вывода для общезначимых формул можно получить только общезначимую формулу.
       Теорема доказана.
Теорема. (Теорема Черча о неразрешимости исчисления предикатов). ИП является полуразрешимой теорией.
       Теорема не требует доказательства.