Аксиомы и правила вывода исчисления предикатов 1-го порядка

Исчисление предикатов первого порядка (сокращенно ИП1) является формальной теорией, теоремы которой суть логически общезначимые формулы.

ИП1 имеет пять схем аксиом, из которых первые три схемы совпадают со схемами аксиом исчисления высказываний (ИВ), а еще две схемы имеют вид:

(4) , где терм свободен для переменной в формуле ;

(5) , где формула не содержит свободных вхождений переменной .

Полезно рассмотреть контрпримеры, показывающие важность условий логической общезначимости формул схем аксиом (4) и (5).

1) Пусть формула A в схеме (4) есть , где - какой-нибудь предикатный символ арности 2, а терм t= . Очевидно, этот терм не свободен для переменной в формуле A. Согласно схеме (4) получим формулу . Возьмем интерпретацию, в которой символу сопоставляется предикат тождества (совпадения элементов области интерпретации), а область интерпретации содержит не менее двух различных элементов. Тогда посылка записанной выше импликации истинна в выбранной интерпретации, а заключение ложно. Стало быть, и вся импликация ложна, и формула, полученная из схемы (4), не является логически общезначимой.

2) Пусть в схеме (5) формула A совпадает с формулой B и совпадает с атомарной формулой для какого-то предикатного символа арности 1.

Тогда формула , полученная из схемы (5), не является логически общезначимой, так как ее посылка истинна в любой интерпретации, а для заключения можно найти интерпретацию, в которой оно ложно[4].

ИП1 имеет два правила (точнее, две схемы правил) вывода, из которых первое есть известное нам правило MP, а второе, называемое правилом обобщения (сокращенное обозначение – Gen), есть однопосылочное правило вида:

.

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

Например, для произвольного предикатного символа арности 1 формула будет логически общезначимой, так как является тавтологией вида .

Как и ИВ, ИП1 является теорией полной и непротиворечивой, т.е. может быть доказана следующая теорема:

Теорема 1. 1) Теория ИП1 непротиворечива, т.е. если доказана формула F, то ее отрицание не является теоремой ИП1.

2) Теория ИП1 полна, т.е. формула есть теорема теории ИП1 тогда и только тогда, когда она логически общезначима. #

Как и в ИВ, в ИП1 может быть доказана теорема дедукции, но при некоторых ограничениях на вывод.

Рассмотрим в этой связи понятие зависимости формул в выводе.

Пусть

некоторый вывод в ИП1 из множества формул G, и пусть формула A ÎG. Тогда, по определению, формула указанного вывода, совпадающая с A, зависит от A, и если есть результат применения правила MP или Gen к формулам, зависящим от A, то она также считается зависящей от A.

Например, построим вывод

├ .

Имеем:

1. A – гипотеза;

2. - правило Gen, шаг 1;

3. - гипотеза;

4. B – правило MP, шаги 2 и 3;

5. - правило Gen, шаг 4.

В приведенном выводе от формулы A зависят формулы 2, 4 и 5 шагов.

С учетом понятия зависимости формул теорема дедукции для ИП1 формулируется следующим образом:

Теорема 2 (теорема дедукции для исчисления предикатов 1-го порядка). Если G, A ├ B, причем существует такой вывод формулы B из множества формул G È {A}, в котором ни при каком применении правила Gen к формулам, зависящем в этом выводе от формулы A, не связывается квантором никакая свободная переменная формулы A, то G ├ A ®B. #

Доказательство основано на двух утверждениях:

Утверждение 1. Если формула есть тавтология, то есть теорема ИП1, причем она может быть выведена применением только схем (1) – (3) и правила MP.

Утверждение 2. Если формула не зависит от формулы в выводе ├ , то ├ .

[Мендельсон, с. 68-69.]

Далее индукция по длине вывода.

Базис и переход при применении правила MP доказываются точно так же, как и ИВ (с учетом утверждения 1).

Пусть теперь формула в выводе из получена применением правила Gen к некоторой формуле , т.е. есть . Тогда формула не зависит в выводе из от формулы или не является свободной переменной формулы .

Если не зависит от , то, согласно утверждению 2, имеем ├ , и, применяя Gen, получим ├ , т.е. ├ . Тогда по первой схеме аксиом имеем , и после применения MP получим G ├ A ®B.

Пусть теперь переменная не есть свободная переменная формулы . Тогда используем схему (5):

.

Далее: ├ (по предположению индукции) ; (Gen).

Итак, ├ . Применяя MP к полученной формуле и к подстановке в схему (5), получим ├ , что и требовалось.

Так, в рассмотренном выше примере при условии, что в формулах A и B нет свободных вхождений переменной , то применение теоремы дедукции даст секвенцию ├ . В этом случае можно применить теорему дедукции второй раз и доказать формулу .

Важное свойство ИП1 характеризует также следующая метатеорема, называемая правилом индивидуализации.

Теорема 3. Имеет место следующая секвенция:

├ ,

каков бы ни был терм t, свободный для переменной x в формуле A.

Доказательство немедленно получается из схемы (4) применением правила MP.