Построение теории 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); |
7) Y → X ∨ Y ; |
Еще четыре схемы связаны с кванторами (ниже 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);