25. Аксиматические теории первого порядка

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

Перед тем, как перейти к обсуждению технических подробностей, относящихся к такого рода теориям полезно будет составить некоторое общее интуитивное представление о том, что они собой представляют. Мы будем исходить из данного в § 3.3 описания первичных терминов неформальной теории как некоторого множества X И некоторых связанных с X констант. Мы считали тогда, что каждая такая константа есть либо элемент множества X (т. е. является предметной константой), либо некоторое подмножество множества XN (иными словами, есть некоторое отношение или операция в X). Теперь мы сможем сопоставить каждому отношению и операции в X Некоторой предикат. Скажем, П-местному отношению[2] мы сопоставим предикатную букву Р (x1, x2, ...., хn) таким образом, что простой формуле Р (y1, y2,…, yn) будет приписываться значение Т при значениях , приписанных, соответственно, аргументам , в том и только в том случае, когда . Теперь, однако, мы предпочитаем вместо «предикатные буквы» говорить предикатные символы, оставляя термин «предикатные буквы» для обозначения каких-либо фиксированных предикатов. Итак, в качестве первичных терминов теории у нас будет некоторое множество X, затем (быть может, пустое) множество предметных констант (элементов множества X) и, наконец, некоторое множество предикатных символов. Рассмотрим теперь формальную теорию, формальными символами которой являются предметные константы, имеющиеся в интересующей нас неформальной теории, бесконечный список предметных переменных, предикатные символы, определенные, исходя из рассматриваемой неформальной теории описанным выше образом, и логические символы исчисления предикатов. В качестве аксиом теории мы возьмем аксиомы соответствующей неформальной теории и аксиомы исчисления предикатов. Правилами вывода будут правила вывода исчисления предикатов. То, что получается в результате, — это и есть аксиоматическая теория первого порядка! Когда исчисление предикатов включается таким образом в какую-либо аксиоматическую теорию, получающуюся в результате теорию часто называют прикладным исчислением предикатов — в отличие от описанного в § 3.7 не имеющего никаких «примесей» чистого исчисления предикатов.

Перед тем, как уточнить понятие теории первого порядка «по всем правилам», к которым мы пытаемся приучить читателя, предварительно скажем еще несколько слов. В большинстве теорий, которые могут быть аксиоматизированы как теории первого порядка, используется понятие равенства. Мы покажем сейчас, каким образом теория равенства присоединяется к чистому исчислению предикатов. Согласно интуитивному пониманию, соотношение «Х = у» означает, что Х и Y - это один и тот же предмет или что «X» и «Y» суть имена одного и того же предмета. Все свойства равенства, используемые в математике, сводятся к тому, что 1) оно есть отношение эквивалентности и 2) оно обладает следующим подстановочным свойством: если Х = у и Q есть результат замены одного или нескольких вхождений «X» в высказывание Р вхождениями «Y», то Q имеет то же значение, что и Р. Оказывается, свойства симметричности и транзитивности равенства можно вывести из подстановочного свойства и рефлексивности. Мы установим это, представив в виде аксиоматической теории исчисление предикатов первого порядка с равенством. Такое исчисление получается расширением описанного в § 3.7 исчисления за счет включения 1) предикатного символа = в число формальных символов теории, 2) пункта «если Х и У - переменные, то (Х = у) — формула» в определение формулы и 3) аксиомы

(РС7) (А) (А = A)

И схемы аксиом

(РС8). Если Х, у, Z — различные переменные и A(Z) свободна для Х и для У, то (X)(Y)(X = Y → (A(X) → A(Y))).

Мы можем теперь дать точное описание теории первого порядка T. Формальные символы теории следующие:

(Is) Некоторое множество предметных констант (быть может, пустое).

(IIS) Бесконечная последовательность предметных переменных

(IIIS) Множество предикатных символов, содержащее символ =.

(IVS) Логические символы исчисления предикатов и скобки.

Предикатные символы обозначаются как символы отношений или как символы операций. Любой N—местный предикатный символ, в зависимости от его назначения, будет называться символом N-местного отношения или символом N—арной операции. В частности, = понимается как символ бинарного отношения. Символы отношений и операций и предметные константы — это нелогические константы теории T. Символ равенства и логические символы исчисления предикатов — это логические константы теории T. Символ равенства, хотя и рассматривается как логическая константа, включается в число символов отношений.

Дальнейшее описание теории T требует прежде всего индуктивного определения терма:

(It) Предметная переменная и предметная константа суть термы.

(IIt) Если — термы и A - символ N—местной операции, то A() — терм.

(IIIt) Никаких других термов, кроме определенных согласно (It) и (IIt), в T нет.

Определение формулы тоже индуктивное:

(If) Если A — символ N—местного отношения, а — термы, то А() — формула. В частности, если R и S — термы, то (R = S) — формула.

(IIf) Если А и В - формулы, то ~(A) и (A)(В) - формулы.

(IIIf) Если A - формула, а Х — переменная, то (X) A - формула.

(IVf) Формулами теории T являются лишь цепочки, состоящие из символов и термов T, являющиеся таковыми согласно (If) — (IIIf).

Мы будем пользоваться в T всеми сокращениями, соглашениями и определениями, принятыми нами для исчисления предикатов. Кроме того, (r = s)будет сокращенно записываться в виде R = S, a ~ (R = S) в виде R ≠ S. Единственный пункт из приведенного описания теории T, к которому читатель не был подготовлен предыдущим изложением, — это понятие терма. Согласно естественной интерпретации, терм - это имя некоторого предмета. Кроме переменных и предметных констант, термами являются цепочки, образованные из переменных и предметных констант посредством символов операций, поскольку в подразумеваемой интерпретации они истолковываются как значения некоторых функций.

< Предыдущая		Следующая >