2) ecjm Л и В формулы, то (Л&В), (Л V В), {Л = В) формулы;

3) если А формула, то ~~iA формула;

4) ecjm А{х) формула, содержащая переменную ж, то

УхА{х), ЧхА{х) (2.3)

формулы. 4. Дополнительные аксиомы.

УхА{х) АЦ), АЦ) ЗжЛ(а)),

тдеЬ = t{xi, ...,х„) - терм и в формуле Л нет кванторов Ух{, Зж; {г = 1,...,п).

4. Дополнительные правила вывода.

В А{х) В Уа)Л(а))

Л(ж) В За;Л(а)) В

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

Появление в теории аксиом, разрешающих «навешивание кванторов» по знакам операций или предикатов, приводит к исчислениям высших порядков. Исчисление предикатов - это теория первого порядка.

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

2.3.2. Полнота и непротиворечивость исчисления предикатов

Теорема 2.5 (Гёдель, 1930). Для исчисления предикатов справедливо утверждение:

\= А тогда и только тогда, когда h А. Доказательство. См. [46, с.71,78].

Теорема 2.6. Исчисление предикатов - полная теория.

Доказательство. Следует из утверждения «= А влечет h А» теоремы 2.5.

Теорема 2.7. Исчисление предикатов - непротиворечивая теория.

Доказательство. Следует из утверждения А влечет \= А» теоремы 2.5. Действительно, если бы была доказуема формула А = В&1~В, то была бы общезначимой формула B&i~iB. Но последняя формула ложна.

2.4. формальная арифметика

2.4.1. Эгалитарные теории

Теория, содержащая исчисление предикатов, называется эгалитарной, если она имеет дополнительный двуместный предикат = {,), для которого выполняются две нелогические аксиомы:

1. Уж(= {х,х)У,

2. = {х,у) {А{...,х,...,у,...) =>А{...,у,...,у,...)).

Здесь А произвольная формула.

Вместо = (ж, у) пишут х = у. Таким образом, эгалитарная теория - это просто теория с равенством.

2.4.2. Язык и правила вывода формальной арифметики

Формальная арифметика - это эгалитарное прикладное исчисление, в котором flonojmHTejibHO имеются:

1. Предметная константа 0.

2. Двуместные операции -- и • и одноместная операция .

3. Знак равенства • = •.

4. Нелогические аксиомы равенства (§2.4.1) и следующие нелогические аксиомы арифметики;

(Л{0)Шх{Л{х) Л{х)))УхЛ{х)

{t[ = t2) (fl = и)

-(f=0)

(fl = и) ((*2 =и) (fl =и)) (<1 = и) (tl = fa) t + 0 = t

{ti+t2) = {tl+t2y

to = o

где A - любая формула, a t,ti,t2 - любые термы.

Первая аксиома - это известный способ доказательства посредством математической индукции. Если вместо t писать t + 1, то ясно, что f - это следующее натуральное число, идущее за t. Другими словами, аксиомы арифметики определяют натуральные числа и правила оперирования с ними с помощью операций сложения и умножения.

2.4.3. Непротиворечивость формальной арифметики. Теорема Генцена

Метод математической индукции, который входит в качестве аксиомы в формальную арифметику, может быть усилен за счет расширения области его применения до так называемых трансфинитных чисел [4, которые, как видно из их названия, «идут следом» за финитными, т.е. натуральными числами. Получается более мощный способ доказательства теорем, названный методом трансфинитной uHj/Kuu [4.

Теорема 2.8 (Генцен, 1936). Непротиворечивость формальной арифметики доказывается в более широкой формальной теории, содержащей арифметику и принцип трансфинитной индукции.

Доказательство. См. [46, с.283-295.

«Траке» - за, финитный* - конечный.