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

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

11.4. СОГЛАСОВАННОСТЬ С ИСТИННОСТЬЮ

311

и вывод A & ¬B ⇒ ¬(A ⇒ B).

∗ A & ¬B



A ¬B

∗ A ⇒ B



⊥

¬(A ⇒ B)

A & ¬B ⇒ ¬(A ⇒ B)

А теперь докажем правила формулировки отрицаний.Каждое из них

является эквивалентностью и требует доказательства и в ту, и в другую

сторону. В одну сторону — от отрицаний частей к отрицанию целого —

они по сути дела уже доказаны для пропозициональных связок. (¬A ∨

¬B) ⇒ ¬(A & B) легко доказать самим, базируясь на уже доказанных

фактах); докажем их для кванторов.

∗ ∃x ¬A(x) ∗ ∀x ¬A(x)



¬A(c

)

∗ ∀x A(x)



A(c

)

⊥

¬∀x A(x)



∗ ∃x A(x)



A(c

)

¬A(c

)

⊥

¬∃x A(x)

∃x ¬A(x) ⇒ ¬∀x A(x) ∀x ¬A(x) ⇒ ¬∃x A(x)

В обоих этих примерах правило передачи информации применяет-

ся корректно: вспомогательная константа может быть использована во

внутреннем подвыводе; во внутренний подвывод может быть пронесена

замкнутая формула. Импликации в обратном направлении порою тре-

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

выделить прямые и косвенные. Но, конечно же, приемы, которые в этих

выводах применяются, хорошим стилем оформления не назовешь. Они

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

нейшем пользоваться уже ими.

312

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

∗ ¬(A ∨ B)



∗ A



A ∨ B

⊥

¬A

∗ B



A ∨ B

⊥

¬B

¬A & ¬B

¬(A ∨ B) ⇒ ¬A & ¬B

∗ ¬(A ⇒ B)



∗ ¬A



A ⇒ B

⊥

¬¬A

∗ B



A ⇒ B

⊥

¬B

A & ¬B

¬(A ⇒ B) ⇒ A & ¬B

Во втором выводе косвенным является вывод A. А следующий ниже

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

зование A ∨ ¬A:

∗ ¬(A & B)



A ∨ ¬A

∗ A ∗ ¬A



B ∨ ¬B

∗ B ∗ ¬B



A & B

⊥

¬A ∨ ¬B

| ¬A ∨ ¬B

¬A ∨ ¬B

| ¬A ∨ ¬B

¬(A & B) ⇒ ¬A ∨ ¬B

11.4. СОГЛАСОВАННОСТЬ С ИСТИННОСТЬЮ

313

Осталось рассмотреть кванторы.

∗ ¬∃x A(x)



∗ x

произвольно



∗ A(x)



∃x A(x)

⊥

¬A(x)

∀x ¬A(x)

¬∃x A(x) ⇒ ∀x ¬A(x)

∗ ¬∀x A(x)



∗ ¬∃x ¬A(x)



∗ x

произвольно



∗ ¬A(x)



∃x ¬A(x)

⊥

¬¬A(x)

A(x)

∀x A(x)

⊥

¬¬∃x ¬A(x)

∃x ¬A(x)

¬∀x A(x) ⇒ ∃x ¬A(x)

Второй из этих выводов является неподражаемо косвенным. Теперь

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

ценно в сочетании с A ∨ ¬A.

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

11.4.1. Докажите следующие формулы:

∀x(A(x) ∨ B) ⇒ ∀x A(x) ∨ B

2. ∀x(A(x) ∨ B(x)) ⇒ ∀x A(x) ∨ ∃x B(x)

3. ∀x ∃y A(x, y) & ∃x ∀y B(x, y) ⇒ ∃x ∃y(A(x, y) & B(x, y))

4. (∀x A(x) ⇒ B) ⇒ ∃x(A(x) ⇒ B)

5. (B ⇒ ∃x A(x)) ⇒ ∃x(B ⇒ A(x))

6. (∃x A(x) ⇒ B) & (∀x ¬A(x) ⇒ B) ⇒ B

7. ∃x(A(x) ⇒ ∀x A(x))

8. ∀x ∃y A(y, x) & ∀x ∀y ∀z(A(x, y) & A(x, z) ⇒ A(y, z)) ⇒

∀x A(x, x)

9. ∀x ∃y A(y, x) & ∀x ∀y ∀z(A(x, y) & A(x, z) ⇒ A(y, z)) ⇒

∀x ∀y(A(x, y) ⇒ A(y, x))

10. ∀x ∀y(A(x) ∨ B(y)) ⇒ ∀x A(x) ∨ ∀x B(x)

11. ∃x ∀y B(x, y) ⇒ ∃x B(x, x)

12. ∃x ∀y(A(x) ⇒ B(x, y)) ⇒ ∃x(A(x) ⇒ B(x, x))

314

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

13. ∃x(A(x) ⇒ B(x)) & ∀x(¬A(x) ⇒ B(x)) & ∀x(¬B(x) ∨

C(x)) ⇒ ∃x C(x)

14. ∀x ∀y(A(f(x), y) ∨ B(x, y)) & ∀x ∀y(¬A(x, g(y)) ∨ B(x, y))

⇒ ∃x∃yB(x, y)

§ 11.5. ТЕОРЕМА ПОЛНОТЫ ЕСТЕСТВЕННОГО

ВЫВОДА

Доказательство эквивалентности выводимости и логической истинно-

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

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

дель для невыводимой формулы построим столь неэффективно,что вос-

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

лей практически невозможно. Это связано с “асимметричностью” есте-

ственного вывода:он хорош как средство доказательства, но то, что вы-

вод не удалось завершить, не всегда дает информацию для опровер-

жения.

Утверждение о полноте состоит из двух частей. Нужно доказать кор-

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

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

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

ется достаточно тривиальной индукцией, но с достаточно нетривиаль-

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

Теорема 11.1. (Теорема корректности) Если

A выводима в Th, то A

является семантическим следствием Th.

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

ного вывода. Незаконченный вывод — граф, удовлетворяющий услови-

ям, наложенным на вывод, кроме того, что каждый подвывод должен

иметь результат и использоваться в дальнейшем. Естественно, подвыво-

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

ный вывод может рассматриваться как промежуточная стадия постро-

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

там и теореме. Многие преобразования выводов являются общими для

завершенных и незавершенных выводов. В данном доказательстве нам

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

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

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

11.5. ТЕОРЕМА ПОЛНОТЫ ЕСТЕСТВЕННОГО ВЫВОДА

315

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

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

сделаны различными. Индукция ведется по числу вершин-формул в не-

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

Если

Σ — незаконченный вывод, A — встречающаяся в нем

формула, A

, ..., A

— допущения всех подвыводов, в кото-

рые входит формула A, c

, ..., c

— входящие в нее вспомо-

гательные константы, причем c

вводится в формуле B

, ..., z

— произвольные переменные, входящие свобод-

но в A, E

, ..., E

— аксиомы Th, использованные в нашем

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

торой истинны все E

, . . . , E

, при любых значениях z

, ...,

, c

, ..., c

, таких, что истинны все A

, ..., A

, B

), ис-

тинна и наша формула A. Итак, формула, встретившаяся в

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

тинны все предположения, явные и неявные, от которых она

зависит. Далее, второй частью индукционного утверждения,

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

утверждение: если вспомогательная константа c

вводится

посредством формулы B

) и A

, ..., A

— допущения, а

, ..., E

— аксиомы Th, использованные в незаконченном

выводе B

), z

, ..., z

— входящие в них свободные пере-

менные, то в любой интерпретации, в которой истинны A

..., A

, E

, ..., E

, при любых значениях z

, ..., z

можно

подобрать такое значение c

, при котором B

) истинно.

Базис индукции. Если в незаконченном выводе одна формула, то

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

нен тривиально.

Шаг индукции. Пусть инвариант доказан для всех незаконченных

выводов длины

6 n. Докажем его для незаконченных выводов длины

n + 1. Пусть Σ содержит n + 1 формулу. Возьмем произвольную фор-

мулу A, не используемую никаким правилом. Удалив ее, а также (если

она не является аксиомой либо допущением) породившее ее правило

из вывода, получим незаконченный вывод Σ

, содержащий n формул.

Все встречающиеся в нем формулы, по предположению индукции, ис-

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

которых они зависят. Для вспомогательных констант можно подобрать

316

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

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

вольных переменных. Теперь рассмотрим всевозможные случаи, соот-

ветствующие получению A.

Если

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

так же, как и в базисе индукции.

Пусть

A получена по правилу

modus ponens

. Тогда посылками это-

го правила являются формулы вида B и B ⇒ A, подчиненные тому

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

формулу A и

породившее ее правило modus ponens, получаем незаконченный вывод

длины n, в котором встречаются B и B ⇒ A. По предположению индук-

ции,они истинны в соответствующих контекстах,а по структуре вывода

контекст у них тот же, что и у A. А если в некоторой интерпретации ис-

тинны B и B ⇒ A, то в ней истинно A. Все остальные правила прямого

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

столь же тривиально.

Пусть

A ⇒ B получено по правилу дедукции. Тогда в Σ

имеется

подвывод, допущением которого является A,а результатом — B. Опять-

таки, отбрасывая из Σ

формулу A и породившее ее правило, получаем,

что B истинно в любой интерпретации, где истинны формулы, принад-

лежащие контексту A ⇒ B, и формула A. Значит, по теореме дедукции,

A ⇒ B истинна в любой интерпретации, где истинны все формулы из

ее контекста.

Пусть

C получено по правилу разбора случаев. Тогда в Σ

имеются

формула A ∨ B и подвыводы, допущениями которых являются A и B

соответственно, а результатом — C. По предположению индукции, в

любой интерпретации, где истинны формулы из контекста, истинно A ∨

B, значит, в ней истинно либо A, либо B, и опять-таки, по структуре

вывода и предположению индукции, истинно C.

Пусть

¬C получено по правилу

reductio ad absurdum

. Тогда в любой

интерпретации, где истинен контекст и вдобавок C, истинны некоторые

B и ¬B. Но этого быть не может, значит, C не истинно ни в одной из

моделей контекста и во всех таких моделях истинно ¬C.

Перейдем к кванторным правилам. Правило перехода от общего к

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

ной константы. Оно вводит новую константу

посредством формулы

). Для нее нетривиальна лишь вторая часть инварианта. Но по-

скольку в любой модели нашего контекста истинно ∃x B

(x), мы полу-

чаем возможность найти подходящее значение c

11.5. ТЕОРЕМА ПОЛНОТЫ ЕСТЕСТВЕННОГО ВЫВОДА

317

При обосновании правила доказательства на примере, т. е. перехода

от A(t) к ∃x A(x) необходимо опять-таки вспомнить вторую часть ин-

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

стант, входящих в терм t. В правиле обобщения A(z) верно при любом

значении произвольной переменной

Доказательство корректности завершено

Теперь рассмотрим обратную импликацию.Чтобы доказать ее,опять-

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

метим, что она эквивалентна следующему утверждению. Теория

Th не-

противоречива, если в ней невыводима никакая пара формул B и ¬B.

Она противоречива, если в ней выводимо такое противоречие. Очевид-

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

ному нами правилу

ex falso quodlibet

), и она моделей не имеет. Отсюда,

если всякое семантическое следствие выводимо, то всякая семантиче-

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

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

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

о существовании модели.

Теорема 11.2. Всякая непротиворечивая теория имеет модель.

Прежде всего заметим, что по определению непротиворечивости,

если

Th непротиворечива и A — замкнутая формула ее словаря, то не-

противоречива по крайней мере одна из теорий Th ∪ {A}, Th ∪ {¬A}.

В самом деле, теория Th ∪ {A} противоречива тогда и только тогда, ко-

гда ¬A выводима в Th (почему?). Значит, поскольку по крайней мере

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

к Th противоположную ей. Очевидно, что пополняя теорию, мы можем

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

любых двух замкнутых формул ¬A, A выводима одна и только одна.

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

замкнутых формул, истинных на некоторой интерпретации данной сиг-

натуры. Но прямо построить такую интерпретацию, исходя из полной

теории, не всегда удается. Мешает этому некорректность: в полной те-

ории может оказаться теорема вида

∃x A(x), такая, что ни для какого

терма t A(t) не является теоремой. Таким образом, может доказываться

существование предметов, которые назвать нельзя. В связи с этим опре-

делим

318

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

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

Теория

∃

корректна

, если для каждой теоремы ви-

да

∃x A(x)

найдется такой терм

, для которого

A(t)

является теоремой.

Теория

∨

корректна

, если для каждой теоремы вида

A ∨ B

либо

, ли-

бо

является теоремой. Теория

корректна

, если она и

∃

-корректна, и

∨

-корректна.

Интерпретацией, порождаемой теорией Th, называется следующая:

Универс состоит из замкнутых термов. Элементарная формула

P (t

, . . . , t

)

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

Лемма 11.5.1. Если

Th полна и корректна, то порождаемая ею интер-

претация является моделью Th.

Доказательство. Индукцией по построению формул докажем, что лю-

бая теорема

Th истинна в данной интерпретации. Базис индукции, ка-

сающийся элементарных формул, выполнен по определению интерпре-

тации. Теперь пусть истинность доказана для всех теорем с числом ло-

гических связок 6 n. Докажем ее для формул с n + 1 связкой.

Пусть формула имеет вид A & B. Тогда она является теоремой в

том и только в том случае, если как A, так и B являются теоремами,

а значит, истинны. Если она имеет вид A ∨ B, то она истинна по ∨-

корректности и предположению индукции. Если она имеет вид A ⇒ B,

то она эквивалентна ¬A ∨ B и истинна по ∨-корректности.

Теперь рассмотрим кванторы. Теорема ∀x A(x) влечет A(t) для лю-

бого терма t. Но, по определению интерпретации, ее универс состоит из

всех таких термов. По предположению индукции, A(t) истинно для лю-

бого терма t. Значит, по определению истинности, ∀x A(x) истинно. По

∃-корректности, если ∃x A(x) является теоремой, то A(t) при некото-

ром терме t является теоремой. Но тогда по предположению индукции

A(t) истинно, и по определению истинности ∃x A(x) истинно.

Легко видеть, что и, наоборот, любая истинная в порождаемой тео-

рией Th интерпретации формула является теоремой Th в случае, если

Th полна и корректна. Итак, полная и корректная теория имеет точ-

ную модель, в которой истинны теоремы и только они. Построить точ-

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

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

рия из двух аксиом {A ⇒ B, B ⇒ C} не имеет точной двузначной мо-

дели.

11.5. ТЕОРЕМА ПОЛНОТЫ ЕСТЕСТВЕННОГО ВЫВОДА

319

Осталось сделать самую малость: построить полную и корректную

теорию.

Первый шаг в этом построении следующий. Перенумеруем все за-

мкнутые формулы нашей теории, не начинающиеся с отрицания

. В ка-

честве исходной теории Th

возьмем саму Th. На i + 1-ом шаге рассма-

триваем формулу A

. Если она не противоречит построенной на преды-

дущем шагу теории Th

, то добавляем ее, если же она противоречит, то

добавляем ¬A

На шагу

ω берем объединение всех ранее построенных теорий. По-

лучившаяся теория полна,но не обязательно корректна.Поэтому на этом

же шагу добавляем для всех аксиом вида ∃x A(x),для которых в Th

нет

аксиом

вида A(x | t), новые константы c

и новые аксиомы A(x | c

После этого теория опять может стать неполной, поэтому перенуме-

руем все формулы новой теории и на шагах

ω + n + 1 поступаем так же,

как на шагах n + 1. На шаге 2ω опять-таки объединяем все Th

ω+n

и до-

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

ваний. Этот процесс продолжаем по всем ординалам вида n ∙ω + k, т. е.

по всем ординалам, меньшим ω

. На шаге ω

объединяем все теории,

полученные на шагах n ∙ ω. Полученная теория будет полной (посколь-

ку любая замкнутая формула A либо ее отрицание будет присутствовать

уже в теории (n + 1) ∙ ω, где Th

n∙ω

— теория, в которой появились все

вспомогательные константы из A). Аналогично, если на шаге n ∙ω име-

ются все вспомогательные константы из ∃x A(x), то на шаге (n + 1) ∙ω

будем иметь A(t).

Конец доказательства теоремы о существовании модели.

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

11.5.1. Мы добавляем вспомогательные константы для существований

все разом, “оптом”, на шаге

n∙ω. А почему это ничему не мешает?

Почему они не путаются между собой?

Если сигнатура несчетна, то в качестве номеров воспользуемся ординалами. Здесь

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

ноты для более чем счетных теорий.

А почему мы не сказали осторожнее: теорем?

320

ГЛАВА 11. ЕСТЕСТВЕННЫЙ ВЫВОД

§ 11.6. ЛОГИКА С РАВЕНСТВОМ И ЕЕ ПОЛНОТА

Работа с равенством для естественного вывода, так же, как и для семан-

тических таблиц, базируется на его определении по Лейбницу. Зададим

два правила работы с равенством, выражающие один и тот же факт —

равные объекты можно без ограничений заменять друг на друга:

t = u A(x|t)

A(x|u)

t = u A(x|u)

A(x|t)

(11.3)

и одну аксиому равенства

∀x(x = x). Корректность этих правил и акси-

омы очевидна.

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

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

и корректной интерпретации, в которой истинны все аксиомы, но ра-

венство интерпретируется как некоторое отношение эквивалентности.

Такую интерпретацию будем называть нестрогой моделью равенства.

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

достаточно перестроить любую нестрогую модель в обычную. Для это-

го установим следующее свойство нестрогой модели.

Предложение 11.6.1. В нестрогой модели

M теории с равенством,если

M |= a

= b

, ..., M |= a

= b

, то для любого n-арного предиката P

M |= P (a

, . . . , a

) ⇔ P (b

, . . . , b

Доказательство. По правилам замены равных, из

= y

, ..., x

= y

при произвольных x

, y

выводимы обе импликации: от P (x

, . . . , x

) к

P (y

, . . . , y

) и наоборот. Значит, выводима формула

∀x

, y

. . . ∀x

, y



= y

& ∙∙∙ & x

= y

⇒

(P (x

, . . . , x

) ⇔ P (y

, . . . y

))



Тогда можно вывести и исходную эквивалентность, применяя правило

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

Предложение 11.6.2. Каждую нестрогую модель теории с равенством

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

всех замкнутых формул.

Доказательство. Рассмотрим фактор-множество универса

M по отно-

шению M |= a = b. По предыдущему предложению все предикаты со-

гласованы с этим отношением эквивалентности, значит, они переносят-

ся на фактор-множество. Получившаяся фактор-интерпретация и явля-

ется искомой моделью.