Совокупность отношений элементов языка

Однако, добавление правил вывода для кванторов второго порядка ведёт к формальной системе которая корректна, но не полна.

Пример: Теория линейного порядка

Арифметика первого порядка

Мы будем упрощать запись формул сигнатуры арифметики первого порядка (6) введением следующего обозначения: a будет записываться как 0, s(t) как t' , f(t1, t2) как t1+t2, и g(t1, t2) как t1 · t2. Аксиомы арифметики первого порядка являются универсальным замыканием следующих формул:

1. x' № 0.

2. x'= y'Й x = y.

3. (F(0) & " v (F(v) Й F(v'))) Й " v F(v) для любой формулы F(v).

4. x + 0 = x.

5. x + y'= (x + y)'.

6. x · 0 = 0.

7. x · y'= x · y + x.

*

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

В следующих формулах 1 обозначает терм 0', 2 – 0'', и 4 – 0''''. Через t1 Ј t2 мы обозначаем формулу $ v(t2 = t1 + v), где v – первая объектная переменная, которая не встречается в t1, t2.

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

3.34 2 № 4.

3.35 x' № x.

3.36 x'= x + 1.

3.37 x Ј x.

Нестандартные модели арифметики

Термы 0, 0', 0'', ... называются цифрами. Модель M арифметики первого порядка стандартна, если для каждого c О |M| существует цифра t такая, что tM = c.

3.38 Модель арифметики первого порядка (7) стандартна.

В соответствие с задачей 3.40, существуют модели арифметики первого порядка, которые не обладают этим свойством. Чтобы доказать существование такой модели, полезно рассмотреть следующую теорию первого порядка G. Сигнатура G получается из сигнатуры арифметики первого порядка добавлением буквы b в качестве новой объектной константы. Множество аксиом G получается из множества аксиом арифметики первого порядка добавлением формул b № 0, b № 0', b № 0'', ... в качестве новых аксиом.

3.39 G непротиворечива.

3.40 Арифметика первого порядка имеет нестандартную модель.

Существование нестандартных моделей арифметики следует из теоремы Сколема (1920), который обобщил раннюю работу Леопольда Лёвенхейма (1915). Возможность таких моделей резко контрастирует с результатом задачи 1.41. Разница связана с тем, что язык арифметики первого порядка является слишком ограниченным для выражения аксиомы индукции. ``Арифметика второго порядка'', в которой схема индукции заменяется по аксиоме (8), не имеет нестандартных моделей.

Теорема неполноты Гёделя

Пусть M – нестандартная модель арифметики первого порядка. Может случится что M ``не отличима'' от модели (7) в том смысле, что для любой замкнутой формулы F арифметики первого порядка F истинно при M тогда и только тогда, когда F истинно при (7). Но некоторые нестандартные модели не обладают этим свойством: может существовать предложение F такое, что при M предложение F истинно, а при (7) ¬F истинно. Так как и M и интерпретация (7) являются моделями арифметики первого порядка, значит ни F, ни ¬F не являются теоремами, а это означает, что арифметика первого порядка неполна. Этот факт, известный как теорема неполноты Гёделя, был доказан Куртом Гёделем в 1931 году.