<<

стр. 2
(всего 3)

СОДЕРЖАНИЕ

>>

A
Таким образом нами была доказана эквивалентность закона исключенного тре-
тьего и правила сведения к противоречию.
Подход интуиционистов нельзя отметать сразу, поскольку уверенными можно
быть в истинности только проверяемых утверждений. Рассмотрим в качестве
примера утверждение о бесконечной последовательности бит, например

(i) данная последовательность состоит только из единиц;

(ii) в данной последовательности есть хотя бы один нуль.
36 Элементы теории доказательств


Очевидно, что ни одно из этих утверждений не может быть проверено (для про-
верки их понадобилось бы бесконечное время). Классическая логика тем не ме-
нее утверждает, что ровно одно из утверждений (i) и (ii) является истинным
(в силу закона исключенного третьего (TND)). Интуиционистский же подход в
данном случае является более осторожным: поскольку ни одно из рассматривае-
мых утверждений практически проверено быть не может, то нельзя утверждать
истинность того, что “верно либо (i), либо (ii)”.

6.3 Подстановки в термах и формулах
Для того, чтобы сформулировать правила введения кванторов всеобщности и
существования, будем считать неразличимыми формулы, которые отличаются
только именами связанных переменных. Например, ?yP (x, y) и ?zP (x, z) будем
считать одной и той же формулой.
Нам также понадобится ввести операцию замены переменных в формуле. В
дальнейшем будем понимать под обозначением P[t/x], где P ? L? , x ? Var, и
I
?
t ? TER(LI ) замену всех вхождений переменной x на терм t. Мы определим
замену переменных для языка логики первого порядка следующим образом.

Определение 6.6 (Замена переменных для термов). Пусть s, t ? TER,
x ? Var. Определим замену s[t/x] следующим образом.
(i) Если s = c ? Const, то s[t/x] := c.

(ii) Если s = y ? Var, причем y отлично от x, то s[t/x] := y.

(iii) Если s = x ? Var, то s[t/x] := t.

(iv) Если s = f k (t1 , . . . , tk ), где f k k-арный функциональный символ, и
t1 , . . . , tk ? TER(L? ), то s[t/x] := f k (t1 [t/x], ..., tk [t/x].
I

Пример 6.2 Пусть c символ константы, x, y символы предметных пере-
менных, а f тернарный функциональный символ. Тогда

f (s(x, c), c, y) f (x, s(x, y), y)/x = f (s(f (x, s(x, y), y), c), c, y)

Определение 6.7 (замена переменных для правильных формул). Пусть
t ? TER(L? ), x ? Var, P, Q ? ?, Ak k-арный предикатный символ. Определим
I
замену так:
(i) Если P атомная формула, т. е. P = Ak (t1 , ..., tk ), то

P[t/x] = Ak (t1 , ..., tk )[t/x] := Ak (t1 [t/x], ..., tk [t/x]).
6.3 Подстановки в термах и формулах 37


(ii) Если P = (¬Q), то
P[t/x] := (¬Q[t/x]).

(iii) Если P = (R ? Q), то

(P)[t/x] = (R[t/x] ? Q[t/x]),

где ? это один из символов ?, ? или >.
(iv) Если P = (?yQ), где ? один из кванторов ? или ?, то

1. Если y = x и y ? V AR(t), то (?yQ)[t/x] = (?yQ[t/x])., где V AR(t) –
множество всех символов предметных переменных в терме t.
2. Если y = x, но y ? V AR(t), то (?yQ)[t/x] = (?rQ[r/y][t/x]), где r ?
V AR(t) (см. пример).
3. Если y = x, то замена не делается, т. е. (?xQ)[t/x] = (?xQ).

Пример 6.3 Пусть < – бинарный предикатный символ (вместо < (x, y) будем
писать x < y), f – унарный функциональный символ, x и y – символы предмет-
ных переменных. Тогда

?y (x < y) f (y)/x = ?z (f (y) < z)

(а не ?y (f (y) < y)).

Теперь мы можем сформулировать правила введения и исключения для кван-
торов всеобщности и существования:
?xA
правило исключения ?xA A [y/x]
(?e)
где y ? T ER(L? )
квантора всеобщности A [y/x]
I


Если ? A [y/x] то ? ?xA
A [y/x]
правило введения
(?i) если y ?
/ free(Q)
квантора всеобщности ?xA
Q??

Заметим, что в последнем правиле весьма важно предположение о том, что y
не входит свободно ни в одну из формул множества ? (иначе говоря, y – “произ-
вольная” переменная). Это правило иногда формулируют так: если ? A [y/x]
для произвольного y, то ? A для любого x. Опустить “предположение” о произ-
вольности y здесь нельзя. Например, введем в арифметике Пеано две формулы
с одной свободной переменной: Odd(x) и Even(x), означающие по смыслу, что x
соответственно “нечетное” или “четное” число. Запишем их следующим образом

Even(x) := ?y(2 · y = x),
38 Элементы теории доказательств


где 2 := s(s(0)),

Odd(x) := Even(s(x))

Тогда в силу доказанного правила (id) имеем Odd(y) Even(S(y))

Однако неверно, что Odd(y) ?xEven(s(x)). То есть из нечетности некоторого
y не следует четность всех чисел! Правило введения квантора всеобщности было
применено неправильно, поскольку символ предикатной переменной y, входящий
в формулу, не являлся произвольным (он входил свободно в формулу-посылку).
Правила введения и исключения для квантора существования следующие:
правило введения
A[t/x]
A[t/x] ?xA
(?i) квантора
где t ? T ER(L? ) ?xA
I
существования

[A[y/x]]1
Если ?, A[y/x] C ?xA
правило исключения
C
то ?, ?xA C
квантора
(?e) 1
C
где y ?/ f ree(Q)
существования
Q???C
В качестве примера докажем следующую метатеорему:


Теорема 6.2 ?x (A (x) > ?yA(y)) для любой формулы A ? L? с одной свобод-
ной переменной.


В вольной формулировке утверждение данной теоремы можно проинтерпре-
тировать следующим образом: можно доказать, что найдется такой человек, что
если он носит шляпу, то и все люди носят шляпу (или что существует такая
лошадь, что если она синяя, то остальные лошади также синие).
Доказательство: Сначала докажем, что ¬A(x) ?x(A(x) > ?y(A(y))). Дока-
зательство представим в виде дерева
[¬A(x)]2 [A(x)]1
(?i)
??e
?y(A(y))
(1, >i)
A(x) > ?yA(y)
(?i)
?x(A(x) > ?yA(y))
Теперь предположим дополнительно, что ¬?x(A(x) > ?yA(y)). Получим
6.3 Подстановки в термах и формулах 39



?x(A(x) > ?yA(y)) [¬?x(A(x) > ?yA(y))]2
(?i)
?(?e)
A(x)
(?i)
?yA(y)
(>i)
A(x) > ?yA(y)
(?i)
?x(A(x) > ?yA(y))
При доказательстве было использовано новое правило вывода B A > B. Спра-
ведливость такого правила вывода доказывается так:

[A]2 B
B (2 >i)
A>B
Таким образом доказано, что ?x (A (x) > ?yA(y)) .
В интуиционистской теории данная метатеорема неверна (использован закон ис-
ключенного третьего (TND)). Объясняется же она просто: либо все люди носят
шляпы, либо есть человек, который шляпу не носит, тогда он и есть искомый.
В качестве второго примера докажем, что в арифметике Пеано никакой эле-
мент не следует сам за собой.


Теорема 6.3
(P A) ?x (¬s (x) = x) .


Доказательство: Будем пользоваться принципом математической индукции.
Доказательство построим в несколько этапов.



1. База индукции:
(P A) ¬s (0) = 0. Доказательство использует аксиому(P A1 ).

?x¬s (x) = 0
¬s (0) = 0


2. Докажем (P A) ?x (¬s (x) = x > ¬s (s (x)) = s (x)). Доказательство удоб-
но представить в виде дерева
40 Элементы теории доказательств


?x?y(s(x) = s(y) > x = y)
?y(s(x) = s(y) > x = y)
s(x) = s(s(x)) > x = s(x) [s(x) = s(s(x))]1
x = s(x) [¬x = s(x)]2
?1
¬s(x) = s(s(x))
2
¬x = s(x) > ¬s(x) = s(s(x))
?x(¬x = s(x) > ¬s(x) = s(s(x)))


3. Используя результаты шагов 1 и 2 и правило (?i) получаем


(P A) s (0) = 0 ? ?x (¬s (x) = x > ¬s (s (x)) = s (x)) .

4. Произведем подстановку в схему аксиом индукции (P A7 ) на место P фор-
мулы с одной свободной переменной

P (x) := ¬s (x) = x.

В результате получим

(P A) s (0) = 0 ? ?x (¬s (x) = x > ¬s (s (x)) = s (x)) > ?x(¬s (x) = x).

5. Из результатов шагов 3 и 4, с помощью правила modus ponens получим

(P A) ?x¬s (x) = x,

что и требовалось доказать.



6.4 Корректность и полнота естественной дедукции
Напомним определения корректности и полноты формальной системы.

Определение 6.8 Формальная система для языка L? называется

• корректнoй, если для любых ? ? L? , P ? L? из ? P следует ? |= P;

• полнoй, если для любых ? ? L? , P ? L? из ? |= P следует ? P.
6.4 Корректность и полнота естественной дедукции 41


Иначе говоря, формальная система корректна, если для произвольного на-
бора формул ? все выводимые (доказуемые в данной формальной системе) из
него формулы являются семантическими следствиями ?, и полна, если, наобо-
рот, все семантические следствия ? выводимы из ? при помощи этой формальной
системы. Иногда пользуются и следующими более слабыми понятиями, которые
требуют выполнения соответствующих условий только для ? = ?.

Определение 6.9 Формальная система для языка L? называется

• корректнoй в слабом смысле, если для любой формулы P ? L? из P
следует |= P;

• полнoй в слабом смысле, если для любой формулы P ? L? из |= P следует
P.

Требование корректности формальной системы является совершенно есте-
ственным. Действительно, если формальная система корректной не является,
то найдется такая система аксиом ? и такая теорема P, что P можно доказать
с использованием этой формальной системы и множества посылок ?, но в то
же время P семантически не следует из ?. Так что такая формальная систе-
ма не удовлетворяет своему предназначению – формальными синтаксическими
манипуляциями выводить именно только логические следствия. Другое дело –
свойство полноты. Оно является в некотором смысле более сильным, так как
означает возможность при помощи данной формальной системы вывести любое
логическое следствие произвольного множества формул ?.

Теорема 6.4 (о корректности) Естественная дедукция корректна.

Доказательство: Пусть ? ? L? , P ? L? и ? P. Докажем ? |= P индукцией
по глубине n дерева вывода формулы P (т. е. количеству шагов вывода). Иначе
говоря, сначала докажем ? |= P для случая деревьев, в которых не использовано
ни одно правило вывода (n = 0), затем, предполагая, что ? |= P доказано для
всех деревьев вывода глубиной n ? k, докажем справедливость этого утвержде-
ния для случая n = k + 1. При этом в силу принципа математической индукции
утверждение будет доказано для всех возможных деревьев вывода ? P незави-
симо от глубины.
База индукции. Пусть n = 0. Тогда P ? ?, а значит, ? |= P.
Шаг индукции. Пусть утверждение доказано для всех n ? k. Предположим,
что ? P за n = k + 1 шаг. Рассмотрим все возможные правила вывода, кото-
рые могли быть использованы на последнем шаге для получения формулы P, и
докажем для каждого случая ? |= P.
42 Элементы теории доказательств


(?e) Это значит P = P1 , причем ? P1 ? P2 и за k шагов, а значит, в силу
предположения индукции ? |= P1 ? P2 . Следовательно, в любой модели
всех одновременно формул ? v(P1 ? P2 ) = 1, а значит, v(P) = v(P1 ) = 1, то
есть ? |= P.

(?i) В этом случае P = P1 ? P2 , причем ? P1 и ? P2 не более чем за k шагов,
а значит, в силу предположения индукции ? |= P1 и ? |= P2 . Рассмотрим
любую модель всех одновременно формул ?. Мы только что доказали, что
v(P1 ) = 1 и v(P2 ) = 1, но тогда и v(P) = v(P1 ? P2 ) = 1, иначе говоря,
? |= P.

(> i) Тогда P = P1 > P2 , причем ?, P1 P2 за k шагов, а значит, в силу пред-
положения индукции ?, P1 |= P2 . Рассмотрим любую модель всех одновре-
менно формул ?. Если в этой модели v(P1 ) = 1, то в силу только что дока-
занного v(P2 ) = 1, а значит и v(P) = v(P1 > P2 ) = 1. Но если v(P1 ) = 0, то
v(P) = v(P1 > P2 ) = 1. Таким образом, в любом случае ? |= P.

1. (?i) Тогда P = ?xQ, причем ? Q[y/x] за k шагов. Значит, ? |= Q[y/x] в
силу предположения индукции. Рассмотрим любую интерпретацию (M, ?),
являющуюся моделью всех одновременно формул ?. Тогда для любого b ?
M при ?(y) = b имеем v(Q[y/x]) = 1, а значит, v(P) = v(?xQ) = 1. Следо-
вательно, ? |= P .

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

Упражнение 6.1 Докажите, что из выполнимости множества формул ?
следует его непротиворечивость в естественной дедукции.

Полнота естественной дедукции. Исторически первая теорема о полноте
формальной системы была доказана К. Геделем, поэтому традиционно всякую
теорему о полноте некоторой формальной системы принято называть теоремой
Геделя о полноте этой системы. Соответственно, в данном случае мы имеем дело с
теоремой Геделя о полноте классической естественной дедукции. Доказательство
ее будет основано на следующей теореме:

Теорема 6.5 (о модели) Пусть множество формул ? совместно в смысле
классической естественной дедукции. Тогда ? выполнимо (т. е. имеет модель).

Теорема 6.6 (о полноте) Классическая естественная дедукция полна.
6.4 Корректность и полнота естественной дедукции 43


Доказательство: Пусть ? ? L? , P ? L? такие, что ? |= P. Тогда множество
? ? {¬P} невыполнимо, а значит, в силу теоремы о модели, и несовместно в клас-
сической естественной дедукции. Иначе говоря, ?, ¬P ?. Применяя правило
сведения к противоречию (RAA), или (¬e), получаем ? P.
Для доказательства теоремы о модели нам понадобится ряд вспомогательных
конструкций.

Определение 6.10 Будем говорить, что множество ? ? L? содержит сви-
детелей, если для любой формулы вида ?xP ? L? найдется такой терм t ?
T ER(L? ) (называемый свидетелем), что ?xP > P[t/x] ? ?.

Важно отметить следующее: для того, чтобы множество ? ? L? содержало
свидетелей, мало наличия соответствующих термов-свидетелей только для суще-
ствовательных формул из ?. Они должны найтись для любой существовательной
формулы всего языка L? .

Определение 6.11 ? называется максимально совместным множеством, ес-
ли оно строго не содержится ни в одном другом совместном множестве.

Лемма 6.1 Если множество ? является максимально совместным, то ? P
если и только если P ? ?.

Доказательство: Нетривиальным является только доказательство того, что
? P влечет P ? ?. Предположим противное, т. е. ? P, но P ? ?. Тогда
множество ? ? {P} совместно, что противоречит исходному предположению о
максимальной совместности множества ?. Действительно, иначе бы ?, P ?, а
значит, в силу правила (¬i), ? ¬P, что вместе с предположением ? P приво-
дит к противоречию ? ?.
Теперь мы можем перейти непосредственно к основной конструкции доказа-
тельства теоремы о модели. Зададимся целью построить модель (M? , ?? ) сов-
местного множества формул ?. Для этого выберем в качестве универсума M?
множество термов языка L? , т. е. M? := T ER(L? ). Положим cM? := c для любо-
го символа предметной константы c ? Const, f M? (t1 , t2 , . . . , tn ) := f (t1 , t2 , . . . , tn )
для любого n-арного функционального символа f ? Funcn и

1, A (t1 , t2 , . . . tn ) ? ?,
AM? (t1 , t2 , . . . tn ) :=
0, иначе

для каждого n-арного предикатного символа A ? Predn , и, наконец, ?? (x) := x
для любого символа предметной переменной x ? Var.
44 Элементы теории доказательств


Лемма 6.2 Если ? содержит свидетелей и является максимально совмест-
ным, то (M? , ?? ) |= P, если и только если ? P. В частности, построенная
интерпретация (M? , ?? ) является моделью всех одновременно формул множе-
ства ?.
Доказательство: Для доказательства воспользуемся теоремой об индукции по
структуре формул языка L? .
База индукции. Пусть P – атомная формула, т. е. P = A(t1 , t2 , . . . , tn ). Тогда
непосредственно из нашей конструкции следует, что условие (M? , ?? ) |= P вы-
полняется в том и только в том случае, когда P = A(t1 , t2 , . . . , tn ) ? ?, а это, в
свою очередь, эквивалентно тому, что ? P.
Шаг индукции.
1. Пусть P = ¬Q. Тогда условие (M? , ?? ) |= P эквивалентно условию
(M? , ?? ) |= Q. В силу предположения индукции последнее эквивалентно
? Q, что в силу максимальной совместности ? выполняется, если и только
если Q ? ?. Докажем теперь, что в силу максимальной совместности ?
условие Q ? ? эквивалентно условию ¬Q ? ?. Действительно, если ¬Q ? ?,
то Q ? ?, иначе множество ? не было бы совместным. Если же Q ? ?, то так
как множество ? ? {Q} несовместно в силу предположения о максимальной
совместности множества ?, можно заключить по правилу (¬i), что ? ¬Q,
или ¬Q ? ? в силу леммы 6.1.
Таким образом, доказано, что (M? , ?? ) |= P, если и только если P = ¬Q ? ?.
Но последнее ввиду леммы 6.1 эквивалентно ? P.
2. Пусть P = P1 ? P2 . Тогда условие (M? , ?? ) |= P выполнено, если и только
если одновременно (M? , ?? ) |= P1 и (M? , ?? ) |= P2 . В силу предположения
индукции (M? , ?? ) |= Pi , i = 1, 2, эквивалентно условию ? Pi . Таким
образом, доказано, что (M? , ?? ) |= P, если и только если одновременно ?
P1 и ? P2 . Но последнее эквивалентно ? P = P1 ? P2 . Действительно,
если ? Pi , i = 1, 2, то ? P1 ? P2 в силу правила (?i). Наоборот, пусть
? P1 ? P2 . Тогда ? Pi в силу правил (?e.1) и (?e.2).
3. Пусть P = ?xQ. Тогда условие (M? , ?? ) |= P выполнено, если и только если
существует такой терм t ? T ER(L? ) = M? , что (M? , ?? [t/x]) |= Q. Но по-
следнее условие эквивалентно (M? , ?? ) |= Q[t/x] (докажите это в качестве
упражнения!), что в свою очередь в силу предположения индукции экви-
валентно условию ? Q[t/x]. Докажем, что ? Q[t/x] выполняется тогда
и только тогда, когда ? ?xQ, т. е. ? P. Действительно, из ? P [t/x]
следует ? ?xQ в силу правила (?i). Наоборот, если ? ?xQ, то так как ?
содержит свидетелей, то найдется такой терм-свидетель t ? T ER(L? ), что
?xQ > P [t/x] ? ?. Тогда в силу modus ponens ? Q[t/x].
6.4 Корректность и полнота естественной дедукции 45


Все остальные случаи, соответствующие возможной структуре формулы P (т. е.
случаи P = P1 ?P2 , P = P1 > P2 и P = ?xQ), предлагается разобрать в качестве
упражнения.
Доказанная лемма указывает на возможный путь построения модели для про-
извольного совместного множества формул ?. Действительно, достаточно допол-
нить множество ? до максимально совместного множества, содержащего свиде-
телей. Последнее будет выполнимым, а значит, тем более будет выполнимым и
множество ?. Вся сложность в дополнении множества ? до максимально сов-
местного множества, содержащего свидетелей. К сожалению, в общем случае
выполнить его конструктивно (т.е. непосредственно предъявив конструкцию
расширенного множества) не удастся.
Построим новую сигнатуру ? ? , содержащую ?, а также дополнительно для
каждой формулы вида ?xP ? L? новый (т. е. не содержащийся в ?) символ пред-
метной константы cP , разный для разных формул. В новом языке логики пре-
?
дикатов первого порядка L? := L? содержится, таким образом, весь язык L? . В
этом новом языке дополним множество ? всеми формулами вида ?xP > P[cP /x],
где cP – новый символ предметной константы, соответствующий формуле ?xP.
Полученное расширенное множество обозначим ?? .


Лемма 6.3 Множество ? совместно, если и только если совместно множе-
ство ?? .


Q, где ? ? L? и
Доказательство: Докажем, что из ?, ?xP > P[cP /x]
P, Q ? L? , а cP – новый (т. е. отсутствующий в сигнатуре ? и добавленный в
соответствии с конструкцией ? ? ) символ предметной константы, следует ? Q.
Действительно, если ?, ?xP > P[cP /x] Q, то ? (?xP < P[cP /x]) >
Q в силу правила (> i). Но тогда ? ?xP < P[y/x] > Q, где y – символ
предметной переменной, не входящий свободно ни в формулу Q и ни в одну из
формул множества ? (докажите это!). Из правила (?i) следует при этом ?
?y(?xP > P[y/x] > Q). Но так как ?y(?xP > P[y/x] > Q) ?y(?xP >
P[y/x]) > Q, а ?y(?xP > P[y/x]) > Q (?xP > ?yP) > Q и ?xP > ?yP
(докажите эти утверждения!), то ? Q.
Пусть теперь ?? несовместно, т. е. ?? ?. Это значит, что ?, R1 , . . . , Rn ?
для какого-то конечного числа добавленных формул Ri вида Ri := ?xPi >
P[cPi /x]. Докажем индукцией по n, что тогда ? ?. Действительно, для n = 0
это утверждение тривиально. Но если оно верно для n = k, и ?, R1 , . . . , Rk+1 ?,
то ? , Rk+1 ?, где ? := ? ? {R1 , . . . , Rk }. Так как символ предметной константы
cPk+1 не входит ни в одну из формул ?, то по только что доказанному ? ?, а
значит, ? ? в силу предположения индукции.
46 Элементы теории доказательств


Пусть теперь
L0 := L? , ?0 := ?, ?0 := ?,
Lk+1 := L? , ?
?k+1 := ?? ,
?k+1 := ?k , k ? N,
k k
L? := k?N Lk , ?? := k?N ?k , ?? := k?N ?k .

Лемма 6.4 Пусть множество ? совместно. Тогда множество ?? совместно
и содержит свидетелей.

Доказательство: Рассмотрим произвольную формулу вида ?xQ ? L?? . Тогда
?xQ ? Lk для какого-то k ? N, следовательно, найдется такой добавленный на
k + 1 шаге символ предметной константы cQ ? ?k+1 \ ?k , что ?xQ > Q[cQ /x] ?
?k+1 ? ?? , а значит, множество ?? содержит свидетелей.
Докажем теперь, что ?? совместно. Предположим противное, т.е. ?? ?. Зна-
чит, найдется такое конечное множество посылок ? ? ?? (листья дерева дока-
зательства ?? ?), что ? ?. Но так как по определению последовательность
множеств {?i }i?N расширяющаяся и объединение всех множеств этой последо-
вательности есть ?? , то ? ? ?k для какого-нибудь k ? N. Значит, ?k ?, что
противоречит лемме 6.3, в силу которой все ?i , i ? N совместны.
Следующая лемма, эквивалентная аксиоме выбора в теории множеств, чрез-
вычайно широко используется в математике. Она является ключевым элементом
и доказательства теоремы о модели (а следовательно, и теоремы о полноте клас-
сической естественной дедукции).

Лемма 6.5 (Цорн) Пусть частичный порядок (?, <), таков, что любой содер-
жащийся в нем линейный порядок имеет максимальный элемент. Тогда (?, <)
имеет максимальный элемент.

Теорема 6.7 (Линденбаум) Любое совместное множество формул
содержится в некотором максимальном совместном множестве.

Доказательство: Пусть ? ? L? – заданное совместное множество формул. На
множестве совместных подмножеств языка L? , содержащих ?, введем отношение
порядка следующим образом: будем говорить, что ?1 < ?2 , если ?1 ? ?2 . Cоот-
ветствующий частичный порядок обозначим (?, <). Рассмотрим произвольный
линейный порядок (F, <), содержащийся в (?, <). Докажем, что объединение ?
всех множеств формул из F , является максимальным элементом порядка (F, <).
Очевидно, ? содержит ?. С другой стороны, ? совместно. Действительно, иначе
бы ? ?, а значит, нашлось бы такое конечное множество посылок ? ? ? (листья
дерева доказательства ? ?), что ? ?. Но так как ? – объединение расширя-
ющегося семейства множеств F , то найдется такое множество формул ?0 ? F ,
что ? ? ?0 , а значит, ?0 ?, что противоречит совместности всех элементов F .
6.4 Корректность и полнота естественной дедукции 47


Таким образом, доказано, что любой линейный порядок (F, <), содержащий-
ся в (?, <), имеет максимальный элемент. Для доказательства существования
максимального совместного множества, содержащего ? (т. е. максимального эле-
мента порядка (?, <)), остается сослаться на лемму Цорна.
Теперь мы в состоянии легко доказать теорему о модели 6.5.
Доказательство теоремы 6.5 (о модели):
Пусть ? ? L? – заданное совместное множество формул. Построим язык L? и
множество формул ?? ? L? . В силу леммы 6.4 множество ?? совместно и со-
держит свидетелей. По теореме Линденбаума найдется максимально совместное
множество ?? ? L? , содержащее ?? (поэтому оно тем более будет содержать
свидетелей). Это множество формул выполнимо ввиду леммы 6.2, а значит, тем
более выполнимо и содержащееся в нем множество ?.
Единственной неприятной особенностью конструкции доказательства теоре-
мы о модели является то, что для языков с равенством предикатный символ ра-
венства будет интерпретироваться в построенной модели некоторым бинарным
отношением на соответствующем универсуме, которое, вообще говоря, будет от-
личным от отношения равенства, понимаемого в смысле совпадения элементов
универсума. Однако это доказательство легко исправить с учетом требования ин-
терпретации символа равенства отношением совпадения элементов универсума.
Действительно, достаточно на множестве термов T ER(L? ) расширенного языка
L? ввести отношение эквивалентности “?” следующим образом: будем говорить,
что t1 ? t2 , если атомная формула t1 = t2 содержится во множестве ?? (про-
верьте, что это действительно отношение эквивалентности, т. е. оно рефлексив-
но, симметрично и транзитивно). Тогда в качестве универсума конструируемой
модели выберем фактор-множество M := T ER(L? )/ ? (т.е. множество классов
эквивалентных термов). Обозначая класс термов, эквивалентных данному терму
t, за [t], положим cM := c для каждого символа предметной константы c ? Const,
?
f M ([t1 ], [t2 ], . . . , [tn ]) := [f (t1 , t2 , . . . , tn )] для каждого n-арного функционального
символа f ? Funcn ,

1, A (t1 , t2 , . . . , tn ) ? ??
AM ([t1 ] , [t2 ] , . . . , [tn ]) :=
0, иначе

для каждого n-арного предикатного символа A ? Predn , и, наконец, ?? ([x]) := [x]
для любого символа предметной переменной x ? V ar. Осталось проверить, что
данное определение корректно и действительно задает модель всех одновременно
формул множества ?? , а значит, и меньшего множества ?. Проведите эту провер-
ку самостоятельно в качестве упражнения, фактически только слегка поправляя
доказательство леммы 6.2.
48 Основы теории моделей


7 Основы теории моделей

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


Теорема 7.1 (О семантической компактности)



(i) Множество формул ? ? L? выполнимо (то есть имеет модель) тогда и
только тогда, когда любое его конечное подмножество выполнимо.

(ii) ? логически выводит P тогда и только тогда, когда найдется такое ко-
нечное ? ? ?, что ? |= P.


Доказательство:

(i) Докажем, что если ? выполнимо, то любое его конечное подмножество вы-
полнимо. Если ? выполнимо, то существует такая интерпретация, в кото-
рой все одновременно формулы ? истинны. Значит, эта же интерпретация
является моделью любого подмножества ? ? ?. Необходимость доказана.
Теперь докажем достаточность. Пусть ? невыполнимо, а все конечные под-
множества ? выполнимы, тогда, по теореме о модели, ? несовместно, то
есть ? ?. Но, в силу определения формальной системы, найдется такое
конечное подмножество ? (листья дерева вывода псевдоформулы ?), что
? ?. По теореме о корректности естественной дедукции ? невыполнимо,
что противоречит предположению.

(ii) Для доказательства этого пункта заметим, что в силу теоремы о коррект-
ности и полноте естественной дедукции ? |= P, если и только если ? P,
последнее же, в силу определения формальной системы, возможно, если, и
только если найдется такое конечное ? ? ? (листья дерева доказательства
формулы P), что ? ND P. Снова применяя теорему о корректности и пол-
ноте естественной дедукции получаем, что последнее эквивалентно ? |= P.
49


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

Теорема 7.2 (Лёвенгейма Скулема “сверху вниз”
или о понижении мощности модели)
Пусть множество формул ? ? L? выполнимо. Тогда оно имеет модель мощно-
сти не превышающей мощность языка.

Доказательство: Так как множество ? выполнимо, то оно совместно (в силу
теоремы о корректности естественной дедукции). Рассмотрим теперь более по-
дробно доказательство теоремы о модели. Эта теорема утверждает что любое вы-
полнимое множество имеет модель. Там модель “кроилась” из термов расширен-
ного языка L?? . В силу конструкции, #L?? ? #L? , а значит и #T ER(L?? ) ? #L? .
Таким образом, в силу конструкции, использованной в доказательстве теоремы
о модели, можно утверждать существование модели с мощностью, не превыша-
ющей #T ER(L?? ), а значит и #L? .

Теорема 7.3 (О переходе от конечной к бесконечной мощности)
Если множество формул ? ? L? выполнимо в моделях сколь угодно большой
конечной мощности, ? выполнимо и в бесконечной модели.

Доказательство: Рассмотрим ? := ? ? {P?i }? , где
i=1

P?k := ?x1 . . . ?xk (¬x1 = x2 ? ¬x2 = x3 ? . . . ? ¬x1 = xk ) . (7.1)

Заметим, что формула P?k выполнима во всех моделях, универсум которых со-
держит по меньшей мере k элементов, и только в них. В силу теоремы о ком-
пактности, для проверки выполнимости ? достаточно проверить выполнимость
любого его конечного подмножества ? ? ? . Однако, если ? ? ? конечно, то
? ? ? ? {P?i }n , для конечного n ? N. Множество ? ? {P?i }n выполнимо в
i=1 i=1
той модели ?, которая содержит не менее k элементов. Существование такой мо-
дели предполагается в условии теоремы. Следовательно, в этой же модели тем
более выполнимо и меньшее множество формул ?, а значит и ? выполнимо.
Выполнимость же ? тривиально следует из выполнимости ? .
50 Основы теории моделей


Теорема 7.4 (Лёвенгейма Скулема “снизу вверх”
или о повышении мощности модели)
Пусть ? ? L? имеет бесконечную модель. Тогда, для любого множества A, ?
имеет модель, универсум которой имеет мощность не меньше #A.

Доказательство: Дополним сигнатуру ? языка L? новыми символами кон-
стант вида ca , для всех a ? A, так, чтобы среди добавленных символов не было
бы символов исходной сигнатуры и разным элементам множества A соответство-
вали разные добавленные символы констант. Получим новую сигнатуру ? , такую
что #? ? #A. Таким образом #L? ? #A.
Рассмотрим множество ? := ? ? {¬ca = cb : a, b ? A, a = b}. Рассмотрим произ-
вольное конечное подмножество ? ? ? . В силу конечности ?, имеем

? ? ? ? {¬cai = cbj : i, j ? n}

для некоторого n ? N. По условию теоремы множество формул ? имеет модель
M с бесконечным универсумом. В этой модели закрепим за символами констант
cai элементы M таким образом, чтобы cM = cM при ai = bj . В полученной алгеб-
ai bj
раической системе все формулы множества ? будут истинны, иначе говоря, ?
выполнимо. Следовательно, по теореме о компактности, выполнимо и ? . Заме-
тим теперь, что любая модель множества ? должна иметь мощность не меньшую,
чем #A, так как в ней истинны все формулы вида ca = cb , где a, b ? A и a = b.
Но эта же модель будет автоматически и моделью меньшего множества ?, что и
завершает доказательство теоремы.
Первое весьма нетривиальное приложение доказанных утверждений к арифме-
тике Пеано отвечает на вопрос о существовании нестандартных моделей ариф-
метики.

|=
Следствие 7.1 Формальная арифметика Пеано первого порядка P AI имеет
модели, неизоморфные стандартной, в том числе и модели сколь угодно большой
мощности.

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


как и в теореме о модели модель совместного множества формул, существование
которой утверждается в теореме, не может быть предъявлена в силу неконструк-
тивности доказательства, так и здесь “странные” модели, существование которых
утверждается теоремами Левенгейма–Скулема далеко не всегда могут быть яв-
ным образом сконструированы.
Интересно также сравнить утверждения следствия с теоремой Дедекинда для
арифметики Пеано второго порядка. Приведенное следствие позволяет догадать-
ся, что языки логики первого порядка обладают намного меньшей выразительной
силой, например, охарактеризовать модель с точностью до изоморфизма при по-
мощи аксиом языка логики первого порядка (как это было для языков второго
порядка) невозможно. Действительно, по теореме Левенгейма–Скулема, любое
множество аксиом для арифметических формул арифметики первого порядка,
если только оно выполнимо в стандартной модели, будет выполнимо и в моделях
со сколь угодно большими мощностями.


Теорема 7.5 (Лёвенгейма Скулема Тарского) Пусть ? ? L? имеет бес-
конечную модель, пусть A произвольное множество, такое что #A ? #L? (то
есть #A не меньше мощности языка). Тогда ? имеет модель с универсумом,
равномощным A.


Доказательство: Дополним сигнатуру ? новыми символами констант вида
ca для каждого a ? A, таким образом, чтобы разные элементам множества A
соответствовали разным символам констант. Обозначим

? = ? ? {ca : a ? A}

? = ? ? {¬ca = cb : a, b ? A, a = b} ,
заметим, что ? ? L? . Множество ? в силу предположения имеет бесконечную
модель, следовательно, по теореме Левенгейма-Скулема “снизу вверх”, оно име-
ет модель мощности, превосходящей #A. Иначе говоря, в универсуме найдется
достаточное количество различных элементов, которые можно поставить в со-
ответствие новым константам вида ca , чтобы таким образом получить модель
множества ? .
Поскольку множество ? , таким образом, выполнимо, у него найдется модель
(M, ?), такая что #M < #L? . С другой стороны, #M ? #A, поскольку в
(M, ?) истинны все формулы вида ¬ca = cb , где a, b ? A, a = b. Таким образом,
получим
#A ? #M ? #L? ? #A,
52 Основы теории моделей


иначе говоря #M = #A.
Обратимся ещё раз к вопросу о моделях формальной арифметики Пеано первого
порядка, неизоморфных стандартной. Существование таких моделей уже утвер-
ждалось в следствии 7.1. Сейчас мы докажем несколько более сильное утвер-
ждение, а именно, что формальная арифметика Пеано первого порядка имеет
счетную модель, неизоморфную стандартной.

Теорема 7.6 Существует счетная нестандартная модель арифметики Пеано
|=
первого порядка P AI .

Доказательство:
Дополним формальную арифметику Пеано всеми формулами вида ¬x = n, где
1 := s(0), 2 := s(1), n := s(n ? 1), а именно, определим
|=
? := P AI ? {¬x = n}? ,
n=0


где x – символ предметной переменной. Докажем выполнимость ? , для чего вос-
пользуемся теоремой о компактности. Рассмотрим произвольное конечное под-
множество ? ? ? . Имеем
|=
? ? P AI ? {¬x = n}k
n=0

для некоторого конечного k ? N. Очевидно, что множество {¬x = n}k имеет
n=0
модель (N , ?), где ?(x) := k + 1, а N – стандартная модель арифметики. Эта же
интерпретация является, тем более, и моделью меньшего множества ?. Мы до-
казали, таким образом, выполнимость любого конечного ? ? ? , а значит, в силу
теоремы о компактности, и выполнимость ? . Рассмотрим модель ? , существова-
ние которой мы только что доказали. Она не может быть конечной в силу того,
что в ней должны быть одновременно истинны (P A1 ) и (P A2 ), то есть долж-
на существовать инъективная, но не сюръективная функция, определенная на
универсуме этой модели. Следовательно, по теореме Левенгейма-Скулема “свер-
ху вниз” найдется и счетная модель (M, ?) множества ? (она не может быть
конечной по той же причине).
Осталось доказать, что M неизоморфна N , то есть не существует биекции ?
между натуральным рядом и универсумом M. Предположим, что она существу-
ет, а именно, существует биекция ? : N > M , такая, что и для любого терма n
выполнено ? nN = nM . Тогда ? (x) ? Im (?), иначе в данной модели не была бы
/
верна одна из формул вида ¬x = k, но последнее противоречит сюрьективности
?. Следовательно, M неизморфна N .
53


В отличие от результатов, сформулированных в следствии 7.1, утверждение тео-
ремы 7.6 можно сравнительно легко проинтерпретировать. А именно, “версия”
натурального ряда, существование которой утверждается в этой теореме, вы-
глядит следующим образом. Сначала идут “обычные” натуральные числа, затем
идет число ? M (x), которое не следует ни за каким “обычным” натуральным чис-
лом (заметим, что в стандартной модели таким свойством обладает только число
0). И далее, вслед за числом ? M (x) идут числа sM (? M (x)), sM (sM (? M (x))) . . . Та-
ким образом, естественно считать такого рода числа, которые в этой “версии”
натурального ряда находятся “правее” всех “обычных” натуральных чисел, бес-
конечно большими (они “больше” любого “обычного” натурального числа). На
основе полученного таким образом натурального ряда можно построить, также
как это делается с использованием привычного нам натурального ряда N, новую
версию целых, рациональных и вещественных чисел. Естественно, что в постро-
енной таким образом версии вещественной оси найдутся как бесконечно большие,
так и бесконечно малые числа (соответственно большие и меньшие по модулю
всех “обычных” вещественных чисел). Использовать такую “необычную” ( при-
нято говорить нестандартную) версию чисел очень удобно для альтернативного
построения математического анализа. Например, с использованием нестандарт-
ной вещественной оси можно “изгнать” из анализа “неудобоваримые” определения
предела, бесконечно малой величины, а пользоваться лишь бесконечно малыми
числами. При этом все определения, которые обычно даются с использованием
достаточно тяжелого “языка , ?” существенно упрощаются. Математический ана-
лиз, построенный при помощи этого подхода, называется нестандартным ана-
лизом.



8 Сравнение языков логики разных порядков

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


Вопрос 1 Cуществует ли множество формул языка логики первого (соответ-
ственно, второго) порядка, истинное во всех конечных моделях и только в них?
Напомним, что, говоря о мощности модели, мы имеем в виду мощность со-
ответствующего универсума. То есть модель называется конечной (счетной,
54 Сравнение языков логики разных порядков


не более чем счетной), если соответствующим свойством обладает универсум
модели.


Ответ на заданный выше вопрос для языков логики первого порядка, очевидно,
отрицательный вследствие теоремы 7.3: если множество формул верно во всех
конечных моделях, то оно будет иметь и бесконечную модель. В то же время в
языке логики второго порядка данный факт можно выразить всего лишь одним
предложением:


P?n := ?f (?x?y (f (x) = f (y) > x = y) > ?x?y (x = f (y)))

Здесь использован квантор всеобщности по “функциональной переменной”, а
именно, данная формула “говорит”, что во всех моделях, в которых она истин-
на, любая инъекция является сюръекцией. Это и означает, что в универсуме
модели данной формулы не может быть бесконечного числа элементов. Стоит
напомнить, что, строго говоря, согласно нашему определению, в алфавите языка
логики второго порядка нет специальных символов для функциональных пере-
менных, а есть только символы для предикатных переменных, поэтому формулу
P?n нужно понимать как сокращенную запись формулы

?F (f unc(F ) ? ?x?y?z(F (x, z) ? F (y, z) > x = y) > ?x?y(F (y, x))),

где
f unc(F ) := ?x?!y F (x, y),
(иначе говоря, формула f unc(F ) “говорит” о том, что отношение, записанное
символом предикатной переменной F , является графиком функции)
Вопрос, аналогичный вопросу 1, можно сформулировать и для других свойств
модели, например, для свойства модели быть не более чем счетной. А именно:

Вопрос 2 Cуществует ли множество формул языка логики первого (соответ-
ственно второго) порядка, истинное во всех не более чем счетных моделях и
только в них?

Опять-таки, ответ на этот вопрос для языков логики первого порядка отрица-
тельный в силу теоремы Левенгейма–Скулема–Тарского 7.5, а именно, если у
множества формул есть счетная модель, то у него есть и модель сколь угодно
большой мощности. В то же время, для языков логики второго порядка можно
55


охарактеризовать свойство модели быть не более чем счетной одним предложе-
нием, а именно, предложением

Pcount := ?z?f ?X (X (z) ? ?x (X (x) > X (f (x))) > ?x (X (x)))

Здесь f снова символ “функциональной переменной”, которая, строго говоря, в
силу нашего определения, в языке логики второго порядка отсутствует, так что
формулу Pcount нужно понимать как сокращенную запись другой формулы, в ко-
торой вместо символа f присутствует символ предикатной переменной. Запиши-
те соответствующую формулу самостоятельно, по аналогии с тем, как это было
сделано для формулы Pf in .
Можно предъявить сколь угодно много свойств моделей, которые не могут быть
охарактеризованы никакими формулами языков логики первого порядка, но мо-
гут быть легко охарактеризованы формулами языков логики второго порядка.
Например, формула Pcount ? ¬Pf in характеризует свойство модели быть счетной.
В то же время соответствующее свойство не может быть охарактеризовано фор-
мулами языка логики первого порядка.

Упражнение 8.1 Напишите предложение, которое характеризует свойство
модели иметь более чем счетный универсум, иначе говоря, предложение, кото-
рое было бы верно во всех более чем счетных моделях и только в них. Можно ли
охарактеризовать соответствующее свойство при помощи языка логики пер-
вого порядка с не более чем счетным алфавитом? С любым алфавитом?

Любопытно отметить, что, тем не менее, свойство модели иметь заданное конеч-
ное число элементов может быть охарактеризовано и при помощи языка логики
первого порядка. Например формула ?x?y(x = y) верна во всех моделях, уни-
версум которых содержит ровно один элемент, и только в них.

Упражнение 8.2 На языке логики первого порядка напишите предложения,
характеризующие свойства модели иметь не более чем k элементов (k – задан-
ное число), ровно k элементов, не менее чем k элементов.

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

Теорема 8.1 Для языков логики второго порядка теорема о компактности
неверна.
56 Сравнение языков логики разных порядков


Доказательство: Предположим противное и рассмотрим множество формул

? := P?n ? {P?k }? ,
k=1

где формулы P?k определены в (7.1). Пусть ? ? ? конечно, тогда

? ? P?n ? {P?k }m
k=1

для некоторого конечного m ? N. Однако последнее множество формул истинно
в любой модели, универсум которой имеет хотя бы m элементов, а значит, выпол-
нимо и множество формул ?. Тогда, в силу предположения о верности теоремы
о компактности и произвольности подмножества ? заключаем, что множество ?
также является выполнимым. Но тогда в модели ? должно быть не менее чем k
элементов для любого k ? N (так как в этой модели истинны все формулы P?k ).
И в то же время число элементов этой модели должно быть конечно, так как в
ней верна формула Pf in . Так как одновременно эти два условия невыполнимы,
то мы пришли к противоречию.


Теорема 8.2 Для языков логики второго порядка неверны теоремы Левенгей-
ма–Скулема о повышении мощности модели 7.4 и о понижении мощности мо-
дели 7.2.


Доказательство: Если бы для языков логики второго порядка была верна тео-
рема Левенгейма–Скулема о повышении мощности модели, то нельзя было бы на-
писать множество формул, выражающее счетность модели. Если бы для языков
логики второго порядка была верна теорема Левенгейма–Скулема о понижении
мощности модели, то нельзя было бы написать множество формул, выражающее
более чем счетность модели.
Завершим эту главу наиболее сильным, на наш взгляд, результатом.


Теорема 8.3 Для логики второго порядка не существует одновременно полной
и корректной формальной системы.


Доказательство: Предположение о существовании одновременно корректной
и полной формальной системы влечет справедливость теоремы о компактности
(в доказательстве теоремы о компактности для языков логики первого поряд-
ка использовался лишь факт существования одновременно корректной и полной
формальной системы), что противоречит теореме 8.1.
57


Требование корректности является необходимым для осмысленности формаль-
ной системы: формальная система строится для того, чтобы получать логиче-
ские, то есть семантические, истины, поэтому некорректная формальная система,
которая позволяет выводить в том числе формулы, не являющиеся истинными,
не имеет никакой практической ценности. Только что доказанная теорема утвер-
ждает, таким образом, что осмысленная (т.е. корректная) формальная система
для языка логики второго порядка не может быть полной. Иначе говоря, при
помощи такой формальной системы мы не можем вывести все семантические
истины. В то же время другого инструмента, пригодного для поиска на прак-
тике семантических следствий для заданного множества формул, кроме вывода
при помощи некоторой формальной системы, нет. Поэтому утверждение теоре-
мы 8.3 фактически является препятствием к широкому использованию языков
логики второго порядка. Языки логики второго порядка являются, таким обра-
зом, “чересчур” выразительными, настолько, что их чрезмерная выразительная
сила ограничивает возможность их применения. В этом смысле языки логики
первого порядка являются вполне подходящими, так как инструмент для их ис-
пользования (достаточно удобные формальные системы) существует, и в то же
время, как показывает опыт, при помощи языка логики первого порядка можно
записывать практически все важные естественнонаучные теории, хотя и нельзя
охарактеризовать какую-нибудь серьезную модель однозначно.



9 Формальная теория множеств

В качестве еще одного примера языка логики первого порядка, находящего самые
широкие применения в современной математике, рассмотрим язык теории мно-
жеств. Определим язык теории множеств как язык L? логики первого порядка с
равенством, с сигнатурой, содержащей лишь один символ, отличный от равенства
– символ предиката принадлежности ?. Иначе говоря, ?(L? ) := {=, ?}. Принято
писать x = y и x ? y вместо = (x, y) и ? (x, y) соответственно. Например, мы
будем считать формулы x = y, ?x ? y ? z ? q правильными формулами язы-
ка L? . Как и принято в математике, мы будем интерпретировать эти формулы
соответственно как “множества x и y совпадают” и “существует множество x, при-
надлежащее множеству y, и множество z принадлежит множеству q”. Несколько
необычным с точки зрения наивной теории множеств является утверждение о
том, что одно множество принадлежит другому. Привычнее говорить о том, что
элемент принадлежит множеству. Однако заметим, что во введенном языке име-
ются символы предметных переменных только одного cорта, а именно – только
для обозначения множеств (нет специального сорта переменных для обозначения
58 Формальная теория множеств


элементов множеств). Поэтому, имея дело с семантикой языка L? , мы будем ин-
терпретировать все предметные переменные как “множества”. Таким образом мы
будем иметь дело с миром, состоящим только из одного типа объектов – “мно-
жеств”. При этом нас не будет интересовать, насколько понятие “множества” как
элемента интерпретирующего универсума соответствует интуитивному понятию
множества как совокупности разных объектов. К этому вопросу мы еще вернемся
в дальнейшем.
Несмотря на то, что введенный в рассмотрение язык L? кажется весьма бедным,
на нем можно выразить все привычные факты о множествах (а также, и всю
математику – но об этом речь пойдет чуть позже). Например, “x подмножество
y” можно записать в виде правильной формулы языка L? , которую будем обо-
значать x ? y, следующим образом:

x ? y := ?z(z ? x > z ? y).

Здесь и далее подчеркивание указывает на то, что мы имеем дело с сокращенным
обозначением правильной формулы. Чуть позже мы еще займемся “кодировани-
ем” основных математических понятий в виде формул L? . А теперь покажем, что
к перенесению основных интуитивных понятий о множествах на формальный
язык L? нужно подходить с большой осторожностью. Рассмотрим следующий
пример.
Парадокс Рассела-Фреге. Мы привыкли формировать множества путем груп-
пирования элементов, обладающих заданным свойством (принято обозначать
{x : P (x)} множество элементов, обладающих свойством P ). Попробуем форма-
лизовать такой способ формирования множеств на языке L? . А именно, логично
предположить, что множество z := {x : P(x)} существует для любого “свойства”
(т. е. формулы L? с одной свободной переменной). Это легко записать в виде
формулы
?z?x(x ? z - P(x)),
где #free(P) = 1 (здесь и далее запись A - B понимается как сокращенная
запись формулы (A > B) ? (B > A). Каким бы заманчивым с интуитивной
точки зрения ни было это утверждение, оно ведет к абсурду. Действительно,
выберем в качестве P свойство множества не принадлежать самому себе, то есть
P(x) := ¬x ? x. Тогда для множества z := {x : ¬x ? x}, очевидно, выполняется
либо z ? z, либо z ? z, причем в силу определения множества z в первом случае
z ? z, а во втором z ? z. С более формальной точки зрения это означает, что
предложение
Q := ?z?x(x ? z - ¬x ? x)
противоречиво.
9.1 Аксиоматика Цермело-Френкеля. Основные аксиомы 59


Приведенный парадокс, который, несмотря на его название, был впервые об-
наружен Г. Кантором, показывает что далеко не все интуитивно осмысленные
предложения введенного формального языка теории множеств имеют право на
существование. Поэтому для построения содержательной и осмысленной фор-
мальной теории множеств явно недостаточно интуиции, основанной на наивных
представлениях о множествах. Традиционный способ выхода из такой ситуации –
ограничить формальную теорию множеств утверждениями, выводимыми из до-
статочно простого, понятного и непротиворечивого набора аксиом. В то же время
математика развивалась в течение по крайней мере последних двух с половиной
тысяч лет и накопила за это время огромный набор фактов, давно ставших досто-
янием как собственно математики, так и всех использующих ее наук. Теория же
множеств как основание математики появилась сравнительно недавно, начиная с
работ Г. Кантора в 70-х годах 19 века. Поэтому система аксиом для формальной
теории множеств кроме непротиворечивости должна обладать еще и следующим
важным с прикладной точки зрения свойством: она не должна существенным
образом обеднять создаваемую на ее основе формальную теорию множеств и ма-
тематику в целом. В связи с особой важностью теории множеств для построения
современной математики на протяжении 20 века было предпринято много по-
пыток предоставить такой набор аксиом. Ни одна из предложенных аксиоматик
не была абсолютно удачной, так что проблема формального обоснования совре-
менной математики до сих пор остается открытой. В то же время хотелось бы
предостеречь от немедленных попыток взяться за решение этой проблемы. Де-
ло в том, что, во-первых, существует несколько вполне удовлетворительных для
практических целей аксиоматик (наиболее популярные среди них – аксиоматики
Цермело-Френкеля и Геделя-Бернайса), а во-вторых, полное решение проблемы
формального обоснования вряд ли что-либо изменит в развитии современной ма-
тематики. Вскоре мы подробнее рассмотрим эти вопросы. А сейчас выпишем с
небольшими комментариями аксиомы наиболее простой и часто используемой ак-
сиоматики формальной теории множеств, предложенной Цермело и Френкелем.



9.1 Аксиоматика Цермело-Френкеля. Основные аксиомы

• Аксиома объемности.

?x?y(?z(z ? x - z ? y) - x = y) (ZF1 )

Эта аксиома говорит о том, что множество однозначно определяется своими
элементами. Очень часто она используется в доказательстве единственности
различных специальных множеств (например, пустого множества).
60 Формальная теория множеств


• Аксиома пары.

?x?y?z?v(v ? z - v = x ? v = y). (ZF2 )

Целесообразно записать ее в сокращенном виде, введя для множества z –
пары элементов x и y обозначение

z = {x, y} := ?v(v = x ? v = y - v ? z).

Таким образом, (ZF2 ) можно записать в виде

?x?y?z(z = {x, y}),

то есть утверждается, что из любых двух элементов можно построить мно-
жество-пару.

• Аксиома выделения.

?x?y (?z (z ? y - (z ? x) ? P (z))) , x, y ? free (P) , #free (P) = 1.
(ZF3 )
Эта аксиома представляет собой исправленный вариант обсуждавшегося
выше принципа, по которому можно формировать множества путем груп-
пирования элементов, обладающих заданным свойством. В исходном вари-
анте, как было показано, этот принцип ведет к противоречию. Способ слегка
подправить его с целью получить в действительности часто используемый
в математике факт, очень прост – достаточно заметить, что на практике
множества всегда формируются путем выделения элементов, обладающих
заданным свойством, из заданного множества, а не просто путем группиро-
вания “всех вообще” элементов с заданным свойством. Так например, мно-
жество {n : n2 ? 1 = 0} на самом деле получено выделением элементов из
N (то есть правильнее было бы писать {n ? N : n2 ? 1 = 0}). Такой способ
исправления основного принципа формирования множества по заданному
свойству его элементов был предложен Фреге и реализован в (ZF3 ).

• Аксиома множества подмножеств. Для сокращения записи введем об-
щепринятое обозначение для множества y всех подмножеств заданного мно-
жества x: y = 2x := ?z(z ? x - z ? y). Заметим, что в данном определении
использовано ранее введенное сокращение – формула z ? x. Рассматривае-
мая аксиома позволяет формировать новое множество как множество всех
подмножеств заданного множества и может быть с использованием введен-
ных обозначений записана в виде

?x?y(y = 2x ). (ZF4 )
9.1 Аксиоматика Цермело-Френкеля. Основные аксиомы 61


• Аксиома суммы говорит о существовании объединения произвольного
множества множеств. Для удобства записи введем обозначение для объ-
единения (иногда называемого также суммой) всех элементов множества x
(напомним, что все объекты, с которыми мы работаем – множества):

y = ?x := ?z(z ? y - ?v(v ? x ? z ? v)).

С учетом введенного обозначения аксиома суммы записывается в виде

?x?y(y = ?x). (ZF5 )


Прежде чем рассмотреть оставшиеся четыре аксиомы Цермело-Френкеля, по-
тренируемся в “кодировании” основных фактов о множествах на языке L? и в
их доказательстве с использованием уже введенных аксиом. Будем обозначать
систему аксиом Цермело-Френкеля (кроме аксиомы выбора) ZF .


Пример 9.1 Докажем существование и единственность пустого множества,
то есть множества, не содержащего ни одного элемента. Для этого введем
общепринятое обозначение:

x = ? := ?y(¬y ? x).

Требуется доказать ZF ?!x(x = ?). Напомним, что ?!x P(x) – общепринятое
сокращение формулы

?x P(x) ? ?y?x(P(y) ? P(x) > x = y).


Доказательство:
Существование. Аксиома (ZF3 ) записывается в виде

?x?y?z(z ? y - z ? x ? (¬z = z)).

Применяя правило (?e), получаем (ZF3 ) ?y R, где

R := ?z(z ? y - z ? x ? (¬z = z)).

Теперь докажем R ?z(¬z ? y). Это доказательство удобно представить в виде
62 Формальная теория множеств


дерева
?z(z ? y - z ? x ? (¬z = z)) (?e)
z ? y - z ? x ? (¬z = z) (?e)
z ? y > z ? x ? (¬z = z) [z ? y]1 (m.p.)
z ? x ? (¬z = z)
¬z = z
? 1, (¬i)
¬z ? y (?i)
?z(¬z ? y)
Осталось объединить две “ветви” для завершения доказательства:

(ZF3 ) [R]2
?y R ?z(¬z ? y)
2
?y?z(¬z ? y)

(здесь применено одновременно несколько правил; мы предоставляем читателям
возможность самим убедиться в корректности соответствующего перехода).
Единственность. Надо доказать

ZF ?x?y(?z(¬z ? y) ? ?z(¬z ? x) > (x = y)).

Представим доказательство в виде дерева

[?z(¬z ? x) ? ?z(¬z ? y)]1 [?z(¬z ? x) ? ?z(¬z ? y)]1
?z(¬z ? x) ?z(¬z ? y)
¬z ? x ¬z ? y
¬z ? x ? ¬z ? y
(ZF1 ) z?x-z?y
?z (z ? x - z ? y) > (x = y) ?z (z ? x - z ? y)
x=y 1
?z(¬z ? x) ? ?z(¬z ? y) > x = y
?x?y (?z(¬z ? x) ? ?z(¬z ? y) > x = y)

Предоставляем читателю определить, какие правила применены на каждом шаге
доказательства, а также заполнить недостающие фрагменты. После этого оста-
нется объединить доказательство существования с доказательством единствен-
ности при помощи правила (?i). .

Упражнение 9.1 Доказать
9.1 Аксиоматика Цермело-Френкеля. Основные аксиомы 63


(A) ZF ?x?y?!z(z = x ? y), где

z = x ? y := ?v(v ? z - v ? x ? v ? y)

(существование и единственность объединения множеств).

(B) ZF ?x?!y(y = {x}), где

y = {x} := y = {x, x}

(существование и единственность одноэлементного множества, содер-
жащего заданный элемент).


Указание:

(A) Для доказательства существования использовать аксиому суммы, приме-
ненную к множеству-паре {x, y}. Существование последнего гарантируется
аксиомой пары. Для доказательства единственности использовать аксиому
объемности.

(B) Использовать аксиому пары и аксиому объемности.


Упражнение 9.2 Введем упорядоченную пару как пару с выделенным первым
элементом:
x = (y, z) := x = {{y}, {y, z}}.
Доказать
ZF ?y?z?x(x = (y, z)).


Указание: Для доказательства существования упорядоченной пары (y, z) ис-
пользовать уже доказанные факты существования одноэлементного множества
{y} и пары {y, z}, затем еще раз сослаться на существования пары, элементами
которой будут только что построенные множества. Для доказательства един-
ственности использовать аксиому объемности.
64 Формальная теория множеств


Упражнение 9.3


(C) Введем следующее обозначение для векторов, обобщающее понятие упоря-
доченной пары:
x = (x1 , ..., xn ) := x = (x1 , (x2 , ..., xn )).
Докажите ZF ?x1 ?x2 ?!y(y = x1 ? x2 ), где
y = x1 ? . . . ? xn := ?u(u ? y - ?z1 ...?zn (z1 ? x1 ? . . . ? zn ? xn ? u = (z1 , . . . , zn )))
(существование и единственность декартова произведения множеств).
(D) Доказать ZF ?x(¬x = ?)?!y(y = ?x), где
y = ?x := ?z(z ? y - ?v(v ? x > z ? v))
(существование и единственность пересечения произвольного числа мно-
жеств).
(E) Доказать ZF ?x?y?!z(z = x ? y), где
z = x ? y := ?v(v ? z - (v ? x ? v ? y)).

Указание:


(F) Рассмотрим случай только элементов в произведении, поскольку техни-
ка доказательства в других случаях аналогична. Единственность следует
из аксиомы объемности, а существование из аксиомы выделения, приме-
x ?x
ненной к множеству x := 22 1 2 , и свойству P := ?z1 ?z2 (z1 ? x1 ? z2 ?
x2 ? z = (z1 , z2 )).
(G) Для доказательства существования применить аксиому выделения к
множеству ?x и свойству P := ?v(v ? x > z ? v) Единственность
следует из аксиомы объемности.
(H) Применить (E) к паре (x, y).

• Аксиома замены. Можно создавать новое множество как множество зна-
чений некоторой функции.
?x(?y?z?w((y ? x ? P (y, z) ? P (y, w)) > z = w) >
?r?s(s ? r - ?t(t ? x ? P (t, s)))). (ZF6 )
9.2 Отношение порядка 65


9.2 Отношение порядка

Перед обсуждением остальных аксиом Цермело-Френкеля рассмотрим понятие
порядка. Введем следующее определение:

Определение 9.1 Частичным порядком называется пара (A, <), где A – мно-
жество, а < – двуместное отношение на A (напомним, что n-местное от-
ношение на A это просто подмножество An , то есть < это подмножество
A ? A), обладающее следующими свойствами:

(i) y < y для всех y ? A,

(ii) Из x < y и y < z следует x < z для всех x, y, z ? A.

В этом случае говорят также, что отношение < частично упорядочивает
множество A либо что A частично упорядоченно отношением <.

Следуя традиции, мы используем значок < (а не букву) как знак отношения
частичного порядка и называем это отношение “меньше”.

Определение 9.2 Частичный порядок (A, <) называется линейным, если все
элементы множества A сравнимы отношением <, иначе говоря, если для всех
a ? A , b ? A выполнено либо a < b, либо b < a, либо a = b. В этом случае
говорят также, что отношение < является отношением линейного порядка
на A, или что A является множеством, линейно упорядоченным отношением
<.

Пусть (A, <) – частичный порядок. Очевидно, что любое B ? A также частично
упорядоченно отношением <. Элемент x ? B называется минимальным элемен-
том множества B, если не существует никакого меньшего его элемента этого
множества. Элемент x ? B называется наименьшим элементом множества B,
если он меньше всех элементов этого множества. Заметим, что наименьший эле-
мент множества автоматически является и его минимальным элементом, однако
обратное, вообще говоря, неверно. Например, во множестве коробок определим
отношение порядка таким образом, что коробка A меньше коробки B, если ее
можно поместить внутрь коробки B. Ясно, что при таком определении необя-
зательно все коробки являются соизмеримыми, то есть полученный порядок не
обязательно является линейным, (например, если в рассматриваемом множестве
коробок найдутся такие две, что ни одна из них не помещается внутрь другой).
66 Формальная теория множеств


При этом наименьшей коробкой является та, которая помещается во все осталь-
ные, а минимальной та, в которую не помещается ни одна коробка.

Определение 9.3 Порядок (A, <) называется фундированным, если любое под-
множество B ? A содержит минимальный элемент. В этом случае говорят
также, что частично упорядоченное множество A является фундированным.
Фундированный линейный порядок называется полным. В этом случае говорят
также, что множество A вполне упорядочено отношением <.

Вот некоторые примеры частичных порядков:

Пример 9.2


(A) Множество натуральных чисел N со стандартным отношением < – пол-
ный порядок.

(B) Множество Z (целых чисел), также со стандартным отношением < –
не является полным порядком, хотя и является линейным порядком.

(C) Множество комплексных чисел C со следующим отношением порядка
(z1 < z2 - Re(z1 ) < Re(z2 )) является частичным, но не является даже
линейным порядком.

(D) Множество целых положительных чисел Z+ с отношением <, введен-
ным следующим образом: x < y если x делит y. Такой порядок является
частичным, но не является линейным порядком.

(E) Для некоторого множества X, рассмотрим множество всех его подмно-
жеств 2X , упорядочим его отношением включения, а именно x < y если
x ? y и x = y. Такой порядок в общем случае не является линейным.

(F) Над множеством A? слов над алфавитом A, где алфавит частично упоря-
дочен отношением <A , определим лексикографический порядок следующим
образом: x < y если либо длина (число символов) слова x меньше длины
слова y, либо, если их длины одинаковы и x <A y , где x и y – первые
различающиеся буквы. Например, если A – латинский алфавит, <A – по-
рядок следования букв в алфавите, то лексикографический порядок будет
полным, причем для множества слов A? верно, например, что z <A? f ish
и home <A? last. Но если A – вещественные числа, то лексикографический
порядок будет линейным, но не будет полным.
9.2 Отношение порядка 67


Справедливо следующее утверждение:

Теорема 9.1 В любой модели системы аксиом Цермело-Френкеля следующие
три свойства частичных порядков (A, <) эквивалентны:

(i) Порядок (A, <) является фундированным.

(ii) Не существует бесконечной строго убывающей последовательности x0 >
x1 > x2 > . . . > xk > . . . элементов множества A.

(iii) Для множества X верен принцип математической индукции в следующей
форме: если (при каждом x ? X) из истинности для всех y < x следует
истинность P(x), то свойство P верно при всех x.

Доказательство: Теорему будем доказывать по частям. Перейдем к доказа-
тельству эквивалентности первых двух свойств. Рассмотрим бесконечную убы-
вающую последовательность x0 > x1 > x2 > . . .. Очевидно, что множество ее
значений не имеет минимального элемента (следующий элемент найдется для
любого элемента, так как последовательность бесконечная, и он еще меньше, так
как она убывающая). Поэтому (i) влечет (ii). И обратно, если X непустое мно-
жество, не имеющее минимального элемента, то бесконечную убывающую после-
довательность можно строить следующим образом. Зафиксируем некий элемент
x ? X, он не минимальный по предположению, тогда берем меньший элемент
x1 < x, x1 ? X, таким образом получаем бесконечную убывающую последова-
тельность {xi }? .
i=1

Теперь выведем принцип математической индукции из существования минималь-
ного элемента в любом подмножестве. Пусть P(x) – свойство элементов множе-
ства X, верное не для всех элементов x ? X. Рассмотрим множество тех элемен-
тов, для которых свойство P неверно. Множество B непусто по предположению.
Пусть x0 - минимальный элемент множества B. Тогда для всех x < x0 свойство
P(x) выполнено, так как элементов меньших x0 в множестве B нет. Но тогда по
предположению должно быть выполнено и P(x0 ), таким образом мы пришли к
противоречию.
И последнее: из принципа математической индукции следует существование ми-
нимального элемента в любом непустом множестве. Пусть B - множество, в кото-
ром нет минимальных элементов. Докажем что B пусто: в качестве P(x) возьмем
свойство x ? B. Тогда, если P(x) верно для всех x < x0 , то никакой элемент,
меньший x0 , не лежит в B. Значит, если бы x0 лежал в B, то он был бы там
минимальным, таким образом, мы пришли к противоречию.
68 Формальная теория множеств


9.3 Аксиома регулярности

Теперь мы можем сформулировать еще одну, весьма важную аксиому системы
аксиом Цермело-Френкеля, называемую аксиомой регулярности, или фундиро-
вания (the foundation axiom). Эта аксиома записывается следующим образом:

?x ¬x = ? > ?y y ? x ? y ? x = ? , (ZF7 )

где y ? x = ? – сокращенное написание формулы

z ? y = ? := ?r r = z ? y ? r = ? .

Эта аксиома является несколько искусственной и никогда явным образном не
используется в привычной нам математике. Она утверждает, что каждое непу-
стое множество X содержит элементы, минимальные по отношению к отношению
принадлежности ? (а не включения ?). С интуитивной точки зрения мы бы хо-
тели, чтобы все наши множества строились из пустого множества ?. Поэтому мы
хотим избавиться от бесконечных последовательностей множеств, убывающих по
отношению к порядку, определенному отношением принадлежности ?. Аксиома
регулярности (ZF7 ) утверждает таким образом, что никакое множество, в этом
смысле, не может иметь бесконечной “глубины”. В привычной нам математике мы
имеем дело с натуральными, рациональными, действительными числами, функ-
циями и т.п. В дальнейшем мы покажем, что все эти объекты явным образом
строятся из пустого множества ?.
Условие, налагаемое аксиомой регулярности на отношение принадлежности ?,
очень похоже на понятие фундированного порядка. Правда, стоит иметь в виду,
что отношение принадлежности не упорядочивает все множество, например, хотя
бы потому, что из x = y не следует, что x ? y либо y ? x.
/ /
Требование справедливости данной аксиомы является весьма сильным, и, в част-
ности, исключает из возможных моделей аксиоматики Цермело-Френкеля все-
возможные экзотические объекты, такие как множество всех множеств или мно-
жество всех множеств не содержащих себя в качестве элемента. Действительно,
если бы существовало множество A всех множеств, не содержащих самого се-
бя, то есть x ? A, если и только если x ? x, то оно содержало бы бесконечную
/
(“бездонную”) последовательность множеств, включающихся друг в друга. Вот
строгая формулировка и доказательство этого утверждения.
9.4 Аксиома бесконечности 69


Предложение 9.1. ZF ?x(¬x ? x)

Доказательство: Докажем теперь, что никакое множество не принадлежит
самому себе. Воспользуемся аксиомой регулярности и уже доказанным фактом
существования одноэлементного множества {x}, а также тем, что
ZF ?x(x ? {x}), где

x ? {x} := ?y(x ? y ? y = {x})

(докажите этот факт самостоятельно). Дерево доказательства формулы ?x(¬x ?
x) выглядит следующим образом.
[y ? {x} ? ?z(z ? {x} > ¬z ? x)]1 (?e)
?z(z ? {x} > ¬z ? x)(?e)
z ? {x} > ¬z ? x z=x
x ? {x} x ? {x} > ¬x ? x(>e) ?v(?y(y ? v) > ?y(y ? v ? ?z(z ? v > ¬z ? y)))?e,v={x}
¬x ? x?i ?y(y ? {x}) ?y(y ? {x}) > ?y(y ? {x} ? ?z(z ? {x} > ¬z ? y))(>e)
?x(¬x ? x) (?y)(y ? {x} ? ?z(z ? {x} > ¬z ? y))1,(?e)
?x(¬x ? x)




Упражнение 9.4 Докажите, что в модели аксиоматики Цермело-Френкеля
не существует множества всех множеств. Иначе говоря,

ZF ¬?x?y(y ? x).

Указание: Если бы такое множество существовало, то оно содержало бы

<<

стр. 2
(всего 3)

СОДЕРЖАНИЕ

>>