Непейвода Н.Н. Прикладная логика

Подождите немного. Документ загружается.

9.8. ТЕОРЕМА ПОЛНОТЫ

251

Следствие. На любом бесконечном пути в таблице, построенной

согласно стратегии корректных разбиений, имеется бесконечно много

условно финальных секвенций.

Докажем теперь, что для каждой МИ-формулы

A, встретившейся в

секвенции Γ на незамкнутом пути ω, на этом пути встречаются резуль-

таты ее разбиения по каждой константе c

, встречающейся на ω. Если ω

завершается финальной секвенцией, то любое разбиение A избыточно

и, соответственно, любое разбиение по любой константе c

пройдено

в финальной секвенции. Если же путь ω бесконечен, то в промежутке

между i-той и (i + 1)-ой условно финальными секвенциями, встретив-

шимися на ω после появления A и c

, A будет разбито по c

Для любой обычной формулы результаты ее разбиения встретятся

на

ω до следующей условно финальной секвенции после того, как она

появилась либо стала разрешена (если формула является аксиомой).

Итак, любая таблица, построенная в соответствии со стратегией кор-

ректных разбиений, полна

Таким образом, если полная таблица не является выводом в исчисле-

нии секвенций, то она дает модель, в которой все аксиомы

истинны,

а проверяемая формула A ложна. Комбинируя доказанное утверждение

с теоремой корректности, получаем:

Теорема 9.2. (Теорема полноты классической логики)

Th ` A тогда

и только тогда, когда существует вывод секвенции |= Th ⊕{=| A}.

Таким образом, синтаксическая доказуемость при помощи семан-

тических таблиц совпадает с семантическим отношением логическо-

го следования. Теорема полноты (в формулировке, связанной с другой

формализацией логики)была первым фундаментальным результатом ма-

тематической логики, доказанным в 1930 г. великим логиком XX ве-

ка К. Г

eделем (K. G

odel)

. Теорема полноты влечет несколько важных

следствий.

Определение 9.8.3.

Th синтаксически непротиворечива

, если не замы-

кается семантическая таблица ни для какой формулы вида

A&¬A

На самом деле теорему полноты (в форме теоремы существования модели) предвос-

хитил, но не сумел понятно сформулировать и доказать Лёвенгейм (L. L

owenheim) еще

в 1915 г. Его работа осталась незамеченной и была заново открыта лишь после доказа-

тельства Гёделя.

252

ГЛАВА 9. КЛАССИЧЕСКИЕ СТ

Следствие 1. (Теорема существования модели) Если Th синтакси-

чески непротиворечива, то она имеет модель.

Незапертый путь в полной таблице для |= Th ⊕ {=| A&¬A} дает

искомую модель.

Следствие 2. (Теорема компактности) Если

Th ` A

, то найдется

конечная подтеория

⊆ Th, такая, что Th

` A.

В самом деле, найдется замкнутая семантическая таблица для A.

Она использует лишь конечное число аксиом Th.

Следствие 3. (Теорема компактности, форма 2) Если любая ко-

нечная подтеория Th непротиворечива, то Th непротиворечива.

Доказательство. Действуем от противного.Если семантическая табли-

ца для |= T h ∪ {=| A&¬A} замкнута, то найдется конечная Th

⊂ Th,

такая, что Th

противоречива. Значит, если теория противоречива, то

противоречива некоторая ее конечная подтеория.По контрапозиции,по-

лучаем отсюда искомую форму теоремы компактности.

Следствие 4. (Теорема компактности, форма 3) Если любая ко-

нечная подтеория Th имеет модель, то и

имеет модель.

Комбинация следствия 3 и теоремы существования модели.

Следствие 5. (Теорема о взаимной противоречивости) Если те-

ории Th

и Th

непротиворечивы, а теория Th

∪ Th

противоречива,

то найдется конечное число аксиом Th

и конечное число аксиом Th

которые противоречат друг другу.

Следствие 6. (Теорема о взаимной непротиворечивости)

Если теории Th

и Th

непротиворечивы и любое конечное число акси-

ом Th

не противоречит Th

, то теория Th

∪ Th

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

Доказательства этих следствий являются экзаменационными допол-

нительными вопросами на оценки 4–5.

Вы видите, сколько разнообразных форм, внешне совершенно не по-

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

ствия фундаментальной теоремы. Таким свойством обладают все прин-

ципиальные математические результаты. Но отнюдь не всегда их след-

ствия становятся ясны сразу после их открытия. На первый взгляд (ска-

жем) теорема компактности выглядит как тривиальное следствие теоре-

мы полноты. Но потребовалось около двух десятилетий для формули-

ровки теоремы компактности после того, как была полностью осознана

формулировка теоремы полноты, да и первые ее доказательства были

не такими простыми. Более совершенный аппарат позволяет ярче выде-

лить взаимосвязи. Интересна и ее история. Она была доказана русским

9.8. ТЕОРЕМА ПОЛНОТЫ

253

логиком А. И. Мальцевым во время II мировой войны и опубликована

в Вестнике Ивановского педагогического института. Естественно, что

публикация осталась незамеченной, и десятью годами позже она бы-

ла “переоткрыта” Л. Хенкиным. Правда, историческую справедливость

удалось восстановить, но теперь кое-кто утверждает, что она практиче-

ски содержалась в уже упомянутой работе Лёвенгейма.

Упражнения к § 9.8

9.8.1. Доказать, что любая модель теории

Th с равенством может быть

преобразована в такую, в которой равенство определяется как со-

впадение.

9.8.2. Доказать, что теория без равенства, имеющая модель с

n элемен-

тами, имеет и модель с n + 1 элементом.

9.8.3. Доказать,что теория с равенством, у которой есть модели со сколь

угодно большим числом элементов, имеет модель с бесконечным

числом элементов.

9.8.4. Студент Гениалькис доказал, что все счетные модели теории с

равенством

, описывающей порядок и его взаимоотношения со

сложением и вычитанием на множестве рациональных чисел и

имеющей перечисленные ниже аксиомы, изоморфны:

∀x ¬x < x ∀x ∀y ∀z(x < y&y < z ⇒ x < z)

∀x 0 + x = x ∀x ∃y ∃z(y < x&x < z)

∀x x + 0 = x ∀x ∀y(x < y ⇒ ∃z(x < z&z < y))

∀x x + (−x) = 0 ∀x ∀y ∀z x + (y + z) = (x + y) + z

1 > 0 ∀x ∀y x + y = y + x

∀x ∀y ∀z(x + y = x + z ⇒ y = z)

∀x ∀y(x > 0 ⇒ x + y > x)

Доказательство занимает 121 страницу. Будете ли Вы его читать;

если нет, то почему?

9.8.5. Известно, что если из предыдущей теории выбросить сложение,

то все ее счетные модели действительно будут изоморфны. Как же

согласовать это с существованием нестандартных моделей?

9.8.6. Какая аксиома теории

лишняя (следует из остальных)?

254

ГЛАВА 9. КЛАССИЧЕСКИЕ СТ

§ 9.9. СЕЧЕНИЯ

Еще одним важным следствием теоремы полноты для семантических

таблиц является теорема об устранении сечений.

Теорема об устранении сечений. Если семантические таблицы для

Γ ⊕{=| A} и Γ ⊕{|= A} закрываются, то закрывается и семантическая

таблица для Γ.

Доказательство. Поскольку в любой интерпретации

A либо истинно,

либо ложно, в соответствующей секвенции противоречит (по теореме

корректности) своей спецификации одна из формул Γ. Значит, Γ тожде-

ственно истинна и по теореме полноты имеет замкнутую семантиче-

скую таблицу.

Правило сечения

Γ ⊕ {=| A} Γ ⊕ {|= A}

присутствовало в исходной генценовской формулировке исчисления се-

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

ным результатом его работ. Формула A называется формулой сечения

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

Заметим, что наше доказательство, хотя и краткое, обладает одним

существенным недостатком, которого лишено гораздо более длинное

доказательство Генцена. Оно полностью неконструктивно, не дает ни-

какого способа преобразования замкнутых таблиц для его посылок в та-

блицу для заключения, кроме тривиального указания “ищите и обряще-

те”. Логический статус приведенного доказательства полностью анало-

гичен логическому статусу следующего доказательства того, что в шах-

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

рона делает два хода подряд, белые проиграть не могут.

В детерминированной конечной игре обязательно име-

ется либо стратегия, ведущая к выигрышу одной из сторон,

либо стратегия, ведущая к ничьей

Кажется, что оговорка о конечности здесь перестраховка, но предположение о суще-

ствовании выигрышной стратегии у одного из игроков для бесконечных игр оказалось

новой аксиомой теории множеств,альтернативной аксиоме выбора (т. е.несовместимой

с ней, но вроде бы не противоречащей всем остальным аксиомам)!

9.9. СЕЧЕНИЯ

255

Рассмотрим три возможных случая. Если стратегия ведет к

выигрышу белых либо к ничьей, то все доказано. Пусть она

ведет к выигрышу черных.Тогда,воспользовавшись тем,что

есть фигура, которая может ходить в начальной позиции (а

именно,прыгающий через другие фигуры конь), сделаем ею

ход, а затем вернем ее на исходную позицию (например,

1. Kg1–f3, Kf3–g1). Тогда мы передадим ход черным, и по

предположению они теперь должны проиграть, что абсурд-

но. Итак, третий случай исключается.

Тот, кто попытается в реальной игре походить два раза конем туда-

обратно, скорее всего проиграет, так что никакого способа достичь хотя

бы ничьей это доказательство не дает.

Устранение сечений внешне похоже на разбор случаев

A ∨ ¬A, но

отнюдь не сводится к нему. Оно имеет место и для многих некласси-

ческих логик, в которых закон исключенного третьего отсутствует. Оно

проваливается в ряде систем, в которых закон исключенного третьего

есть.

Ввиду исключительной важности данного правила мы рассмотрим и

синтаксическое доказательство устранимости сечений, дающее способ

перестройки таблицы без сечений в таблицу с сечениями.Более того, мы

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

устраняющая из них сечения, и такая, что процесс устранения закан-

чивается независимо от порядка применения данных преобразований.

Эти преобразования называются шагами нормализации таблицы. Шаги

нормализации определяются в соответствии с главной связкой формулы

сечения и с тем, созданы ли обе формулы сечения в посылках непосред-

ственно на предыдущем шагу или же хоть одна из них передается от

предыдущих секвенций без изменения.

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

образований выводов в исчислении секвенций,а именно: ослабления се-

квенций путем дописывания новых членов, подстановки конкретного

значения вместо вспомогательной константы в заключении, т. н. обра-

щения всех правил исчисления секвенций

и сокращения нескольких

экземпляров одинаковых формул в заключении вывода. Далее покажем,

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

На самом деле мы уже указали на возможность обращения правил, разрешив поль-

зоваться для сокращения семантической таблицы обратными преобразованиями.

256

ГЛАВА 9. КЛАССИЧЕСКИЕ СТ

модифицируем понятие вывода. Аксиомами теперь будут лишь проти-

воречия из элементарных формул. Очевидно, что любое противоречие

из пары сложных формул разбивается на элементарные, так что с тео-

ретической точки зрения понятие выводимости не изменяется

Предложение 9.9.1. (Подстановка) Вывод секвенции

Γ ⊕ {A(c

n+1

)},

где c

n+1

не входит в Γ, без увеличения числа применений правил и слож-

ности встречающихся формул перестраивается в вывод Γ ⊕{A(x | t)}

для произвольного терма t.

Доказательство. Начнем с частного случая подстановки — переиме-

нования вспомогательной константы. Докажем, что если

не входит

в формулы из Γ, то вывод Γ[x | c

n+1

] можно преобразовать в вывод

Γ[x | c

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

противоречиями, и мы получаем базис индукции по длине вывода. Да-

лее, все применения правил после такой замены остаются корректны-

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

щих

вспомогательную константу, да и то в случае, когда эта константа

совпадает с c

. Рассмотрим одно из них, например,

⊕ {|= A(c

)}

⊕ {|= ∃y A(y)}

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

ящей ниже его секвенции. В Σ меньше применений правил,чем в исход-

ном выводе, Γ

не содержит c

. Поэтому по предположению индукции

можно переименовать везде внутри Σ, например, заменив ее на

, не

входящее в Σ и не совпадающее с c

n+1

. После чего x можно повсюду

заменять на c

Теперь проведем подстановку терма. Все константы, входящие в

t и

не входящие в Γ, переименуем. После такого переименования все при-

менения правил после подстановки останутся корректными.

Результат применения преобразования подстановки к выводу

Σ обо-

значаем, аналогично подстановке в формулу, Σ[c

n+1

| t]. Проведенное

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

ментарных компонент уже встретившееся противоречие.

В терминах таблиц: вводящих.

9.9. СЕЧЕНИЯ

257

доказательство подчеркивает аналогию связанных переменных в фор-

муле и вспомогательных констант в выводе: на самом деле мы занима-

лись именно устранением коллизий.

Предложение 9.9.2. (Ослабление) Вывод секвенции

Γ перестраивает-

ся без увеличения числа применяемых правил и сложности формул в вы-

вод секвенции Γ ⊕ Δ.

Доказательство. Сначала при помощи подстановки переименуем вну-

три вывода

Γ все вспомогательные константы, входящие в Δ и не встре-

чающиеся в Γ. Затем просто дописываем Δ ко всем секвенциям в исход-

ном выводе.

Предложение 9.9.3. Вывод заключения любого из правил исчисления се-

квенций перестраивается в вывод любой из своих посылок без увеличе-

ния числа применяемых правил и сложности формул.

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

выводе исходной секвенции.

Если примененных правил вообще нет, то исходная секвенция — ак-

сиома, а поскольку противоречие состоит из элементарных формул, оно

находится в

Γ, и результирующая секвенция также является аксиомой.

Пусть теперь обратимость доказана для всех выводов с числом пра-

вил не более

n. Докажем для выводов с n + 1 правилом.

Проанализируем правила обращения для конъюнкции и всеобщно-

сти (остальные правила рассматриваются совершенно аналогично).

Докажем, что вывод

Γ⊕{|= A & B}без усложнения перестраивает-

ся в вывод Γ ⊕ {|= A, |= B}. Проанализируем последнее из применен-

ных в выводе правил. Если это правило создало |= A & B, то просто

отбрасываем его, если же оно его не затрагивало, то обращаем по пред-

положению индукции выводы-посылки данного правила. Так же посту-

паем в случае =| A & B,но здесь в случае,если последним применялось

правило =| &, отбрасываем целое поддерево вывода, поскольку нас ин-

тересует лишь одна из его посылок.

Рассмотрим перестройку вывода секвенции

Γ ⊕{=| ∀x A(x)} в вы-

вод секвенции Γ ⊕ {=| A(c

n+1

)}. Опять-таки если последнее правило

создало =| ∀x A(x), то отбрасываем его, иначе обращаем вывод посыл-

ки. Для истинности рассуждение совершенно аналогично.

258

ГЛАВА 9. КЛАССИЧЕСКИЕ СТ

Предложение 9.9.4. Вывод секвенции Γ ⊕ {|= A, |= A} без увеличения

числа применений правил и сложности встречающихся формул пере-

страивается в вывод Γ ⊕{|= A}. Аналогично для =| A.

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

выводе исходной секвенции.

Если она является аксиомой, то после устранения отдублированной

формулы она аксиомой и останется.

Если последним применялось правило, не затрагивающее ни одного

из экземпляров сокращаемой формулы, то по предположению индукции

можно применить сокращение к выводам посылок и по тому же правилу

получить вывод сокращенного заключения.

Если последним применялось правило к сокращаемой формуле, то

рассмотрим ее вид. Пусть она имеет вид

B & C. Тогда вывод выглядит

следующим образом

Γ ⊕ {|= B & C, |= B, |= C}

Γ ⊕ {|= B & C, |= B & C}

Тогда по обратимости можно перестроить вывод Σ без увеличения дли-

ны в вывод Σ

, дающий секвенцию

Γ ⊕ {|= B, |= C, |= B, |= C}.

А теперь, применив сокращение, получаем из него вывод

Γ ⊕ {|= B, |= C, |= C}

Длина Σ

не больше длины Σ,и опять можно применить предположение

индукции, сократив еще раз:

000

Γ ⊕ {|= B, |= C}

А теперь возвращаем на место последнее правило:

000

Γ ⊕ {|= B, |= C}

Γ ⊕ {|= B & C}

9.9. СЕЧЕНИЯ

259

Рассмотрим случай B ∨ C. Тогда вывод имеет форму

Γ ⊕ {|= B ∨ C, |= B}

Γ ⊕ {|= B ∨ C, |= C}

Γ ⊕ {|= B ∨ C, |= B ∨ C}

Отсюда обращениями получаем

Γ ⊕ {|= B, |= B}

Γ ⊕ {|= C, |= C}

Применяем имеющиеся по предположению индукции сокращения и воз-

вращаем на место исходное правило:

Γ ⊕ {|= B}

Γ ⊕ {|= C}

Γ ⊕ {|= B ∨ C

}

Есть еще одно место в исчислении секвенций, где возникают труд-

ности при нормализации.Кванторы =| ∃и |= ∀“бессмертны”:они не ис-

чезают и дотягиваются из результата до всех аксиом-противоречий. Как

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

но не бесконечное же число раз!

Поэтому желательно было бы кое-

когда от них избавляться.

Предложение 9.9.5. (Удаление последнего квантора) Если вывод име-

ет вид

Γ ⊕ {=| A[x | t], =| ∃x A(x)

}

Γ ⊕ {=| ∃x A(x)}

и внутри Σ формула =| ∃x A(x) более нигде не разбивается, то без уве-

личения длины вывода и сложности формул можно преобразовать Σ в

вывод Γ ⊕ {=| A[x | t]}. Аналогично для |= ∀.

Определим шаги нормализации.

Шаг 0. Если главная связка формулы сечения является пропозици-

ональной и она не разбивается хотя бы в одной из его посылок, либо ее

Это нужно лишь для опровержения, но не для доказательства.

260

ГЛАВА 9. КЛАССИЧЕСКИЕ СТ

главная связка — квантор и ни в одной из посылок для него не вво-

дится вспомогательная константа, то выполняем одно из следующих

преобразований подъема сечения в зависимости от того, какое прави-

ло применялось к одной из секвенций-посылок (эта секвенция для фор-

мул с пропозициональной связкой может выбираться произвольно,а для

кванторных — соответствует посылке вида

Γ ⊕ {|= ∃x A(x)} либо Γ ⊕

{=| ∀x A(x)}).

Γ ⊕ {|= A, =| B, =| C}

Γ ⊕ {=| A ⇒ B, |= C}

Γ ⊕ {=| A ⇒ B, =| C}

Γ ⊕ {=| A ⇒ B}

=⇒

Γ ⊕ {|= A, =| B, =| C}

Γ ⊕ {|= A, =| B, |= C}

Γ ⊕ {|= A, =| B

}

Γ ⊕ {=| A ⇒ B}

Для двухпосылочного правила:

Γ ⊕ {=| A, |= C}

Γ ⊕ {|= B, |= C}

Γ ⊕ {|= A ⇒ B, |= C}

Γ ⊕ {|= A ⇒ B, =| C}

Γ ⊕ {|= A ⇒ B}

=⇒

Γ ⊕ {=| A, |= C}

Γ ⊕ {=| A, =| C}

Γ ⊕ {=| A}

Γ ⊕ {|= B, |= C}

Γ ⊕ {|= B, =| C}

Γ ⊕ {|= B}

Γ ⊕ {|= A ⇒ B}

получается обращением Σ

, Σ

— два обращения Σ

Для остальных пропозициональных связок преобразование произ-

водится аналогично.