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

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

9.6. СЕКВЕНЦИИ

241

то все формулы из Γ специфицированы правильно, и истинно A ⇒ B.

По таблице истинности, тогда ложно A или истинно B. Значит, хотя

бы одна из посылок истинна. Наоборот, если ложен один из аргумен-

тов правила, то все формулы из Γ специфицированы правильно, и лож-

на посылка импликации либо истинно ее заключение. В любом из этих

случаев

A ⇒ B истинна. Теперь рассмотрим правило |= ∀. Если ложен

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

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

то он полностью входит в аргумент, а A(c

) истинно, поскольку истинно

∀x A(x).

И наконец, рассмотрим

=| ∀. Здесь уже не выполнена эквивалент-

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

A(c

n+1

) может быть истинно в интерпретации M, хотя ∀xA(x) ложно в

M. Но:

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

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

В самом деле, возьмем произвольную интерпретацию

M сигнатуры се-

квенции Γ ⊕ {=| ∀xA(x)}. В ней нет интерпретации для c

n+1

, поэтому

ей соответствует целое семейство (M

)

a∈U

интерпретаций аргумента,

отличающихся от M лишь тем, что c

n+1

имеет значение a ∈ U. В ка-

ждой из M

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

некоторого a ∈ U противоречит своей спецификации одна из формул Γ,

то поскольку она не содержит c

n+1

, она сохранит то же значение и в M,

и результат будет истинен. Если же ни для какого a ∈ U ни одной такой

формулы из Γ не найдется, то в любой M

=| A(c

n+1

) противоречит

своей спецификации, и, значит, A(c

n+1

) истинна при любом значении

n+1

из

. По определению истинности, тогда в M истинна ∀xA(x), эта

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

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

зывает тождественную истинность проверяемой формулы. Более того,

Таким образом, данное утверждение имеет логическую форму

∀m A(m) ⇒ ∀m B(m).

242

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

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

ских таблиц оказываются эквивалентными.

9.7. С РАВЕНСТВОМ

243

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

9.6.1. Определить правила исчисления секвенций для всех остальных

связок классической логики.

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

дыдущих параграфов.

9.6.3. Сравните число символов в таблице и в дереве секвенций. А чи-

сло формул?

§ 9.7. СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ С РАВЕНСТВОМ

И ДЛЯ ТЕОРИЙ

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

ленного двуместного предиката =, всегда интерпретируемого как совпа-

дение,т.е. ζ(a = a) = 1; ζ(a = b) = 0 для различающихся a, b. Совпаде-

ние интерпретаций равных объектов гарантирует эквивалентность всех

их свойств, согласно определению равенства, данному Лейбницем. Со-

гласно теореме о замене эквивалентных, это означает, что Subst(A, x, t)

может быть заменено на Subst(A, x, r), если |= t = r. Анализируя,

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

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

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

что t = t всегда истинно. Это выражается следующими дополнитель-

ными правилами закрытия таблиц: если |= t = r либо |= r = t, то

|= Subst(A, x, t) и =| Subst(A, x, r) составляют противоречие. =| t = t

есть противоречие само по себе.

Пример 9.7.1.

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

∀x∀y(x = y ⇒ y = x)

=| ∀x∀y(x = y ⇒ y = x)

=| ∀y(c = y ⇒ y = c)

=| c = d ⇒ d = c

|= c = d =| d = c

=| d = d

Семантические таблицы для равенства являются частным случаем

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

ся ли A теоремой Th. Тогда построим вывод секвенции |= Th ⊕{=| A}.

244

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

Здесь |= Th означает совокупность всех аксиом Th, специфицирован-

ных как истинные. В семантической таблице это означает возможность

в любой момент выписать формулу |= B,где B ∈ Th. Поскольку аксиом

может быть бесконечно много, нецелесообразно требовать обязательно

выписывать их все в самом начале.

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

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

∀xx =

x и две схемы аксиом

∀x∀y(y = x&Subst(A, z, x) ⇒ Subst(A, z, y));

∀x∀y(x = y&Subst(A, z, x) ⇒ Subst(A, z, y));

где A — произвольная формула, не содержащая других свободных пе-

ременных, кроме z.

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

ствуют функции. Здесь действует очень простой закон. Выражения

f(c), f (f (c)), ... считаются различными, если в таблице не установле-

но равенство каких-либо из них, но ни одно из них не годится как новое,

даже если оно еще никуда не подставлялось. Новой может быть лишь

вспомогательная константа c

. Когда появляется одна такая константа,

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

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

использует старые объекты.

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

Проверить истинность следующих формул и рассуждений в логи-

ке с равенством и/или функциональными символами.

9.7.1.

∀x A(x, f(x)) ⇒ ∃x A(x, x)

9.7.2. ∀x A(x, f(x))& ∀x ∀y(x = y) ⇒ ∃x A(x, x)

9.7.3. ∃x ∀y x = y& ∃x(A(x)&¬B(x))& ∃x ¬A(x) ⇒ ∃x B(x)

9.7.4. ∀x A(x) ∨ ∀x ¬A(x) ⇒ ∃x ∀y(x = y)

9.7.5. ∃x ∃y ∀z(x = z ∨ y = z)& ∃x(B(x)&A(x))& ∃x(B(x)&¬A(x)) ⇒

∀x B(x)

9.7.6. ∀x ∃y(x = f (y))& ∀x ∀y ∀z(x = y ∨ x = z ∨ y = z) ⇒

∀x f(f(x)) = x

9.7. С РАВЕНСТВОМ

245

9.7.7. ∀x ∃y(x = f (y))& ∀x f (f(x)) = x ⇒

∀x ∀y ∀z(x = y ∨ x = z ∨ y = z)

9.7.8. ∀x f(f(x)) = x ⇒ ∀x ∃y(x = f(y))

9.7.9. ∀x ∀y(A(x)&A(y) ⇒ x = y)&¬(a = b) ⇒ ∃x ¬A(x)

9.7.10. ∀x ∀y(¬x = y ⇒ A(x) ∨ A(y))& ∃x(B(x)&A(x))& ∀x(C(x) ⇒

¬A(x))& ∀x(C(x) ⇒ B(x)) ⇒ ∀x B(x)

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

кая “очевидные из контекста” аксиомы либо факты, использован-

ные в них. Такие рассуждения называются энтимемами. Проана-

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

полнения установить при помощи семантических таблиц.

9.7.11. Лисы умнее кур. Значит, ни одна курица не умнее лисицы.

9.7.12. Все тутси выше пигмеев. Значит, ни один пигмей не тутси.

9.7.13. Я боюсь зубных врачей. Я не желаю быть в одной компании с

тем, кого боюсь. Значит, я не хочу быть в одной компании с вами.

9.7.14. Народы, у которых некоторые национальные герои — злодеи,

воинственны. Народы, у которых некоторые национальные герои

являются учеными, образованны. Аттила и фон Нейман — нацио-

нальные герои Венгрии. Значит, венгры воинственны, но образо-

ванны.

Сделать выводы из посылок. Проверить их на таблицах.

9.7.15. Все курицы любят клевать пшено. Не все кошки жирные. Те, кто

ест пшено, жиреет. Жирные не могут петь по ночам ...

9.7.16. Все козлята прыгают. Только здоровые молодые животные пры-

гают. Некоторые поросята не прыгают. На свете не более одного

молодого существа, не являющегося козленком ...

9.7.17. Все павлины гордятся своим хвостом.Если кто-то гордится чем-

то, не представляющим ценности, то он не может сделать ничего

путного. Этот мост сделан павлинами. Все мосты в данной мест-

ности, кроме одного, — хорошего качества...

246

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

9.7.18. Те, кто любит учиться, не нуждаются в поощрениях. Для тех,

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

9.7.19. Армия — школа жизни. Если жизнь бестолковая, то такова же и

школа. Российская жизнь в данную пору — бестолковая. Только

толковая армия может выиграть войну. Значит, ...

9.7.20. Чтобы проиграть войну, нужно проиграть хотя бы одно сраже-

ние. Наполеон в кампании 1812 г. выиграл все сражения. Эту кам-

панию он вел с Россией. Значит, ...

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

строил все планы противника. Если нет предательства,то расстро-

ить планы противника достаточно для того, чтобы выигрыш бит-

вы гарантировал победу в войне. Суворов проиграл Итальянскую

кампанию. Значит, ...

9.7.22. (Н. Макиавелли)

Чтобы добиться успеха, политику необхо-

димо выглядеть добродетельным. Кроме добродетельных и амо-

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

бивались успеха лишь аморальные политики, то никто не был бы

добродетельным. Некоторые люди добродетельны...

Сделанный вывод явно софистичен. В чем обман?

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

мнительной?

Никколо Макиавелли — флорентийский общественный деятель и писатель. Он про-

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

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

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

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

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

Поскольку такой показ воспринимался как оправдание существующих гадостей, Ма-

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

литиков до сих пор называют ‘макиавеллизм’. Сам Макиавелли в жизни был прилич-

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

корнем неисчислимых бед в истории.

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

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

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

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

247

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

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

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

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

ем семантических таблиц. Нам необходимо установить, что для каждой

теоремы A теории Th найдется замкнутая семантическая таблица. Но

здесь нужно было бы установить общий метод доказательства любой

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

щенном теории алгоритмов. Поэтому придется действовать от против-

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

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

A, т. е. модель Th, в которой ложно A. Далее установим, что начатую

семантическую таблицу можно продолжить до полной. По контрапози-

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

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

введения ряда важных вспомогательных понятий: полная таблица, не-

завершенная таблица...

Определение 9.8.1. Незавершенная семантическая таблица

— дерево,

каждой вершине которого сопоставлена секвенция, и секвенция в ка-

ждой вершине, не являющейся листом, получается из непосредственно

следующих за ней по одному из правил вывода исчисления секвенций.

Таким образом,в незавершенной таблице снимаются требования ко-

нечности путей и того, что листьями могут быть лишь аксиомы. Содер-

жательно говоря, незавершенная таблица является результатом несколь-

ких разбиений, проделанных над интересующей нас формулой. Неза-

вершенная таблица является одним из простейших примеров важного

и для теории, и для приложений семейства понятий — незавершенных

выводов.

Пример 9.8.1.

Незавершенная таблица.

` A, ` B, a A&B

↑

` A, a (B ⇒ A&B)

↑

a A ⇒ (B ⇒ A&B)

(9.17)

Определение 9.8.2. Шаг разбиения

— добавление правила

и вершин

над листом

незавершенной таблицы,не являющимся аксиомой,таким

образом, чтобы

был получен по правилу

из добавленных вершин.

248

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

Формула

A пройдена

в секвенции

, если она присутствует либо в

самой

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

ной семантической таблицы в

. Шаг разбиения

избыточен

, если хотя

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

таты разбиения пройдены в

. Секвенция

финальна

, если она аксиома

либо каждый шаг разбиения, применимый к ней, избыточен. Путь

ω не-

заперт

,если он бесконечен либо заканчивается в финальной секвенции,

не являющейся аксиомой.

Семантическая таблица

полна

, если все листья являются финальны-

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

в ней выполнены сле-

дующие три (для таблиц в теории — четыре) условия:

1. Если формула является конъюнкцией, импликацией, дизъюнкци-

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

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

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

2. Для любой встречающейся в некоторой секвенции пути

форму-

лы вида

=| ∀x A(x)

(

|= ∃x A(x)

) на

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

=| A(c

) (|= A(c

))

3. Для любой константы

, входящей в некоторую формулу на

и для любой встречающейся в некоторой секвенции

формулы

вида

|= ∀xA(x)

(

=| ∃xA(x)

) на

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

|= A(c

)

(

=| A(c

)

4. (Для таблиц в теории

) На

встречается

|= A

для любой

A ∈

Лемма 9.8.1. (О построении контрпримера) В полной таблице по лю-

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

которой истинны все встречающиеся на нем секвенции.

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

строение контрпримера и его верификация

Построение контрпримера. В качестве универса контрмодели M

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

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

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

здесь это означает истинность всех секвенций.

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

249

ω. Каждая константа означает саму себя. ζ(P (c

, . . . , c

)) есть ⊥, если

=| P (c

, . . . , c

) встречается в какой-то секвенции на ω; >, если встре-

чается |= P (c

, . . . , c

). В остальных случаях оно определяется произ-

вольным образом.

Верификация построения. То, что все секвенции пути

истинны,

означает, что все встречающиеся в них формулы удовлетворяют своим

спецификациям. Это утверждение доказывается индукцией по постро-

ению формулы.

Прежде всего элементарная формула,встретившаяся в некоторой се-

квенции

на пути ω, будет присутствовать и во всех последующих се-

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

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

тарных формул, и модель M определена корректно. Далее, по постро-

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

Базис индукции установлен.

Шаг индукции. Пусть соответствие спецификации уже доказано

для всех формул с числом логических связок меньше n. Пусть A имеет

n логических связок. Разберем случаи, соответствующие построению и

спецификации A.

Если рассматриваемая формула есть |= (B ⇒ C), то, по определе-

нию полноты, на пути ω найдется либо |= C, либо =| B. По предполо-

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

В каждом из этих случаев истинно (B ⇒ C). Если она есть =| (B ⇒ C),

то по полноте на пути ω встретятся и |= B, и =| C. Поскольку они удо-

влетворяют своим спецификациям, (B ⇒ C) ложно.

Если формула имеет вид =| ∀x A(x), то по условию полноты табли-

цы на пути ω встретится =| A(c

) для какого-то c

, и ∀x A(x) ложно.

Если формула есть |= ∀x A(x), то по полноте на ω встретится |=

A(c

) для любой константы c

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

M. По предположению индукции, любая из =| A(c

) удовлетворяет сво-

ей спецификации и, значит, истинна. Но тогда по определению истин-

ности истинно и ∀x A(x).

Остальные связки разбираются аналогично.

Осталось убедиться, что полную таблицу всегда можно построить.

Для этой цели сформулируем стратегию корректного разбиения формул,

приводящую к такой таблице. Стратегия не будет определять однознач-

но, какая формула должна быть разбита в данный момент. Она лишь

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

250

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

Занумеруем все константы из сигнатуры теории нечетными нату-

ральными числами. Все вспомогательные константы занумеруем чет-

ными. Занумеруем все аксиомы теории. Введем дополнительные специ-

фикации для аксиом теории и многократно используемых (МИ) формул

вида

|= ∀x A(x)

=| ∃x A(x)

. Аксиома может быть разрешена или за-

держана. Каждой МИ-формуле сопоставим множество

α констант, по

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

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

ение. Корректное разбиение МИ-формулы может производиться лишь

по константе c

∈ α, при этом c

добавляется к α. Корректное разбие-

ние не может производиться по временно запрещенной или задержан-

ной формуле. Секвенция условно финальна, если в ней не может быть

произведено ни одного неизбыточного корректного разбиения.

Стратегия корректного разбиения. Вначале задерживаем все ак-

сиомы,кроме первой,и не запрещаем ни одной МИ-формулы. Пока фор-

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

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

, имеющей минимальный номер среди всех таких констант, встреча-

ющихся в незадержанных формулах секвенции. Когда секвенция оказа-

лась условно финальной, разрешаем первую из задержанных аксиом и

снимаем все временные запрещения.

Лемма 9.8.2. В незавершенной семантической таблице для теории в

любой секвенции число формул,не являющихся результатами разбиения

аксиом, конечно.

Доказательство. В корне дерева такая формула всего одна. Каждый

шаг разбиения увеличивает их количество не более чем на

Лемма 9.8.3. (Лемма о корректных разбиениях) Любая последова-

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

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

условно финальной.

Доказательство. Определим ранг секвенции как количество логиче-

ских связок в формулах, не являющихся задержанными либо временно

запрещенными.В условиях леммы ранг конечен, поскольку число таких

формул конечно. При каждом разбиении ранг уменьшается на 1.