ВУЗ:
Составители:
Рубрика:
теоремы теории A истинны в интерпретации ω. Поэтому ω является
(нормальной) моделью элементарной арифметики. Аксиомы A1)–A7)
выбраны так, чтобы все обычные факты, истинные в ω и выразимые
в теории A, были бы доказуемы в A. Это объясняет принятое для ω
название — стандартная модель элементарной арифметики.
Пример 4. Докажем ` 0 + x = x. Используем схему аксиом
индукции, выбрав в качестве A(x) формулу 0 + x = x.
1. 0 + 0 = 0 (из A3) с помощью Gen и Q1) при t = 0).
2. 0 + x
0
= (0 + x)
0
(аналогично из A4).
3. 0 + x = x ⇒ 0 + x
0
= x
0
(аналогично из 2 и E2).
4. 0 + 0 = 0 ∧∀x(0 + x = x ⇒ 0 + x
0
= x
0
) (1 и Gen, 3).
5. ∀x(0 + x = x) (1, 4 и A7).
6. 0 + x = x (Q1 и MP).
Упражнение 1. Пусть 1 обозначает терм 0
0
, 2 — 0
00
, 4 — 0
0000
. Докажите в
элементарной арифметике:
1) 2 6= 4; 3) x
0
= x + 1;
2) x
0
6= x; 4) (x + y) + z = x + (y + z).
Формальная теория T называется полной, если для всякого пред-
ложения F , выразимого в этой теории, справедливо T ` F или T ` ¬F .
Формальная теория T называется разрешимой, если существует ал-
горитм, позволяющий для любого предложения F определить, верно
T ` F или нет. Формальная теория T называется категоричной, если
она имеет единственную с точностью до изоморфизма модель.
Элементарная арифметика является неполной, неразрешимой и
некатегоричной теорией.
Хотя очень не просто привести пример истинного в ω, но не до-
казуемого в A утверждения, такие примеры существуют.
В заключение приведем пример формальной теории второго по-
рядка. В логике второго порядка, помимо предметных переменных, до-
пускаются функциональные и предикатные переменные и кванторы по
таким переменным.
V. Формальная арифметика второго порядка A
2
. Содержит:
1) два сорта переменных: переменные для натуральных чисел
x, y, z, . . . (сорт 0) и переменные для подмножеств множества ω нату-
ральных чисел X, Y, Z, . . . (сорт 1);
2) символы элементарной арифметики =, 0,
0
, +, ·, а также новый
предикатный символ ∈, связывающий объекты сорта 0 и сорта 1;
3) все аксиомы элементарной арифметики с той лишь разницей,
что в схеме аксиом индукции в качестве формулы A(x) можно брать
75
