Определим синтаксис языка первого порядка. Алфавит языка первого порядка состоит из логических символов Ú, Ø, $, =, из символов переменных  и из нелогических символов. К логическим символам отнесём символы скобок и запятой. В качестве символов переменных будем использовать также x, y, z, u, v и т.д. Логические символы одинаковы для всех языков первого порядка. Нелогическими называются символы операций, символы предикатов и символы констант. Язык первого порядка L задаётся как множество нелогических символов. Если L = Æ, то L называется языком чистого равенства.

Каждому s Î L ставится в соответствие #(s) Î w. Если s – константа, то #(s) = 0. Если R – символ предиката, такого, что #(R) = n, то R называется символом n-местного предиката. Если f – символ операции, и #(f) = n, то f называется символом n-арной операции. Для предикатов и операций число #(R) (соответственно #(f)) больше 0, и оно называется местностью (соответственно арностью). Объединение множеств символов операций и констант составляет множество функциональных символов, позволяющее строить термы языка L на множестве .

К предикатам языка L мы всегда относим бинарный предикат  (равенство). Определим формулы языка L.

Атомной формулой языка L называется выражение вида: , где  – термы языка L, а R Î L – символ n-местного предиката. В частности, выражение  будет атомарной формулой для любых термов языка L. Множество всех формул языка L определяется как наименьшее множество выражений, которое содержит все атомные формулы и удовлетворяет условиям: если q и y – формулы, а x – переменная, то выражения , Øq, $xq  – формулы. Формулы q и y называются подформулами формулы , формула q – подформулой формул Øq  и $xq.

Будем предполагать, что другие логические связки служат сокращениям:

(q & y)       для Ø(Øq Ú Øy),

(q ® y)      для (Øq Ú y),

" x q          для Ø$ x Øq.

Формула   Øx = y   обычно записывается как  x ¹ y. Примеры формул:

" x $ y P (x, y, x È z),             $ x (y £ x ® y = x).

Замена переменных

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

" y (y = z) ® $ z (z < x)

первое вхождение переменной z свободно, а второе – связанное. Переменная x является свободной, а y – связанной. Формальное определение свободных и связанных переменных следующее:

1) все вхождения переменных в атомных формулах свободны;

2) свободные вхождения x в Øq есть в точности свободные вхождения x в q;

3) свободные вхождения x в  состоят из свободных вхождений x в q и свободных вхождений x в y;

1) если x и y – различные переменные, то свободные вхождения x в формулу $ y q соответствуют свободным вхождениям x в формулу q;

2) в формуле $ x q нет свободных вхождений переменной x.

Запись: q(x) указывает на то, что формула q содержит свободные вхождения переменной x. Если c – символ константы, то q(с) означает формулу, полученную заменой всех свободных вхождений x в q на с. Например, если q(x) = $y((y = x) & " x (x = y)), то q(c) = $y((y = c) & " x (x = y).

Мы пишем:  для указания того, что q содержит свободные переменные среди . Применяется запись:  для обозначения формулы, в которой все свободные вхождения каждой из переменных  формулы q заменяются на терм , . Таким образом, q(с) является сокращением обозначения q(х/с).

Формула, не содержащая свободных переменных, называется предложением.

Может случиться, что при замене переменной термом нарушается очевидный принцип, согласно которому замена переменной в равных формулах даёт равные формулы. Например, пусть t = f(y), q(z) = $y(y < z). Тогда после замены получаем: . С другой стороны, q(z) = $x(x < z), и, значит, . Получаем не равные формулы. Поэтому перед подстановкой терма  в формулу q(х) связанные переменные, содержащиеся в  будем переименовывать на символы, не встречающиеся в .

Другой выход следующий: терм t называется свободным для переменной x в формуле q(х), если никакое свободное вхождение x в q не лежит в области действия кванторов  и , где  входит в t. В этом случае замена q(х/t) допускается.

При подстановках констант противоречия не возникают.

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

Исчисление предикатов

Для того чтобы определить формальную теорию, связанную с языком первого порядка, введём логические аксиомы и правила вывода языка L. Логические аксиомы подразделяются на 3 группы:

1) Аксиомы предложений: всякая формула q языка L, которая может быт получена из некоторой тавтологии исчисления высказываний K (описанного в разд. 3 с помощью аксиом К1 – К10) в результате подстановки формул языка L на место высказывательных символов, есть логическая аксиома языка L. Всякая такая формула называется тавтологией языка первого порядка L.

2) Аксиомы кванторов

· если q и y – формулы языка L, то имеют место следующие аксиомы:

("x (q ® y)) ® (q ® "x y), если х не входит свободно в q;

("x (q ® y)) ® (($ x q) ® y), если х не входит свободно в y;

· для каждой формулы q(х) и терма t, свободного для x, имеют место кванторные аксиомы:

" х q(х) ® q(t);

q(t) ® $ х q(х).

3) Аксиомы равенства

t = t для любого терма t;

(t = s) & q(t) ® q(s), для любых формул q(х) и термов s, t, для которых х свободна в q, а s и t свободны для х (здесь q(t) означает формулу q(x/t)).

Правила вывода

(MP)      Из формул q и q ® y выводится y (Modus Ponens).

(Gen)     Из формулы q выводится " x q (правило обобщения).

Таким образом, определена формальная теория, (разд.3.4), в которой есть формулы, аксиомы и правила вывода. Эта теория называется исчислением предикатов L.

Запись:  å q означает, что существует вывод формулы q из логических аксиом и формул из множества å. Если Æ q, то q – теорема исчисления предикатов L. Множество å называется противоречивым, если для каждой формулы q языка L существует вывод:  å q. В противном случае å называется непротиворечивым. Предложение q называется непротиворечивым, если множество {q} непротиворечиво. Множество формул å называется максимально непротиворечивым, если оно не является собственным подмножеством некоторого непротиворечивого множества.

Легко доказать следующие свойства непротиворечивых множеств:

1) Множество å непротиворечиво, если и только если каждое его конечное подмножество непротиворечиво.

2) Пусть q – предложение. Тогда множество å È {q} противоречиво, если и только если å Øq.

3) Пусть å – максимально непротиворечивое множество. Тогда для любых предложений q и y имеет место:

(i) å q, если и только если q Î å;

(ii) q Ï å, если и только если Øq Î å;

(iii) (q & y) Î å, если и только если q Î å и y Î å;

4) Каждое непротиворечивое множество предложений содержится в некотором максимальном непротиворечивом множестве предложений.

Теорема (о непротиворечивости исчисления предикатов). Нет формул q исчисления предикатов L, для которых существуют выводы:  q  и  Øq.

Доказательство. Каждой формуле q поставим в соответствие формулу h(q) исчисления высказываний K, множество символов P которого состоит из предикатов RÎL. Формулу h(q) определим по индукции:

1)  для атомных формул;

2) ,          ,

,

,   для любых формул ;

3) h("xq) = h(q),         h($xq)  = h(q).

Для всякой логической аксиомы q формула h(q) будет тавтологией в K. Если бы для некоторой формулы q существовали выводы q и Øq, то формулы h(q) и Øh(q) были бы тавтологиями в исчислении высказываний. Поскольку исчисление высказываний непротиворечиво, это невозможно. Стало быть, нет формул q, для которых существуют выводы:   q  и Øq.