Построение теории P

Теория

Язык алгебры предикатов как расширение языка алгебры высказываний. Аксиомы исчисления предикатов: схемы аксиом исчисления высказываний плюс 4 аксиомы с кванторами: 11) ∀xX → Xxt; 12)∀x(Y → X(x)) → (Y → ∀xX(x)); 13) Xxt → ∃xX; 14) ∀x(X(x) → Y) → (∃x X(x) → Y ). Правила вывода: 1∗ X, X → Y      Y ; 2∗      X    ∀xX       . Вывод и вывод из гипотез. Структурное ограничение. Секвенции.

Исчисление предикатов строится как расширение исчисления высказываний. Основная цель та же: формализовать доказательство различного рода утверждений. Исчисление предикатов — составная часть любой формальной теории, отвечающая за логическую часть теории. Если говорить об алгебре предикатов как таковой, уместно ограничиться простейшим вариантом логико-математического языка, оставляя за кадром детали предметной области. Для нас несущественно, как образуются термы, поскольку они целиком относятся к предметной области. Мы под предметной переменной можем понимать любой терм. Кроме того, для нас не является существенным, сколько сортов предметных переменных есть в теории. Можем считать, что один сорт. В то же время мы не можем совсем игнорировать предметные переменные, поскольку именно с ними связано функционирование кванторов.

Учитывая это, будем строить теорию P , языком Ω которой является односортный логико- математический язык с пустым множеством констант и пустым множеством функциональных символов. При этом каждый терм этого языка будет элементарным, т.е. предметной переменной единственного сорта. Поскольку подстановка в формуле связана с предметными переменными, то в нашем языке подстановка есть замена одних предметных переменных другими.

Упрощается и интерпретация рассматриваемого языка. Достаточно задать единую предметную область для всех предметных переменных и указать отображение, которое n-арному предикатному символу ставит в соответствие булеву функцию от n переменных, а в случае 0-арного предикатного символа символ 0 или 1.

Зададим аксиомы исчисления предикатов в виде некоторого набора схем аксиом. Первые десять схем повторяют схемы исчисления высказываний:

1) X → (Y → X);
2) X → Y → (X → (Y → Z) → (X → Z));
3) X∧Y → X;
4) X ∧ Y → Y ;
5) (X → Y) → ((X → Z) → (X → Y ∧Z));
6) X → X ∨ Y;

7) Y → X ∨ Y ;
8) X → Z → (Y → Z → (X∨Y → Z));
9) X → Y → (¬Y → ¬X);
10) ¬¬X → X;
11) X → ¬¬X.

Еще четыре схемы связаны с кванторами (ниже Xxt — правильная подстановка терма t вместо переменной x, Y не содержит свободных вхождений переменной x):

12) ∀x X → Xxt;
13) ∀x(Y → X(x)) → (Y → ∀xX(x));
14) Xxt → ∃xX;
15) ∀x(X(x) → Y) → (∃xX(x) → Y).
В дополнение к правилу modus ponens добавляется правило обобщения: 1∗ X,X → Y;

1*X, X → Y      Y ;

2*      X    ∀xX       .

Как и в исчислении высказываний выводом называем последовательность формул языка, в которой каждая формула либо аксиома, либо получена по одному из правил вывода из предшествующих формул. Также вводим понятие вывода из гипотез Γ, в котором в последовательности формул могут находиться формулы из списка Γ. Однако для вывода из гипотез введем дополнительное структурное требование: если формула ∀x X получена по правилу обобщения, то во всех гипотезах, используемых для вывода этой формулы, переменная x не должна иметь свободных вхождений. Указанное структурное требование не касается аксиом. Поэтому в выводе без гипотез его можно не учитывать.

Смысл сформулированного структурного ограничения становится понятным, если учесть, что вывод должен сохранять истинность формул. Правило модус поненс сохраняет истинность формул при фиксированной модели и фиксированной оценке, а именно: если θ — оценка формулы X → Y в данной модели M, то из истинности Xθ и (X → Y )θ следует истинность Y θ. Правило обобщения нарушает фиксированность оценки при выводе.

Впрочем, структурное ограничение касается лишь частного вывода. Мы могли бы это ограничение не учитывать, но тогда нам придется считаться с ним при ”сшивке“ частных выводов в окончательный вывод без гипотез. Поясним сказанное. Выводимость из X формулы ∀x X следует увязать с выводимостью формулы X → ∀x X , т.е. с тем, что эта формула есть тавтология. Но если переменная x входит в X свободно, то при некоторой интерпретации для некоторого объекта a формула Xax будет ложной, а для некоторого объекта b формула Xxb — истинной. В этом случае ∀xX в соответствии с интерпретацией всеобщности будет ложной формулой при любой оценке, а это приведет к ложности X → ∀x X . Однако эта формула будет тавтологией, если X не имеет свободных вхождений x.

Мы сохраняем запись Γ ⊢ X, означающую, что X выводима из гипотез Γ. Эту запись называем секвенцией.

Пример 5.1. Пусть переменная y не имеет свободных вхождений в X. Тогда ⊢ ∀xX → → ∀y (Xxy). Действительно:

1) ∀x X → Xxy (схема аксиом 14);

2) ∀y (∀x X → Xxy) (по правилу обобщения из 1);

3) ∀y (∀xX → Xxy) → (∀xX → ∀yXxy) (схема аксиом 12);

4 )∀xX → ∀yXxy (по правилу модус поненс из 3 и 4);