<< Пред. стр.

стр. 5
(общее количество: 9)

ОГЛАВЛЕНИЕ

След. стр. >>

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? )/ ? (т.е. множество классов

<< Пред. стр.

стр. 5
(общее количество: 9)

ОГЛАВЛЕНИЕ

След. стр. >>