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

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

9.5. ИСЧИСЛЕНИЯ ТРАДИЦИОННОГО ТИПА

231

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

ние. Правила вывода обычно записываются в следующей форме:

, ∙∙∙ , Ξ

Zυς

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

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

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

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

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

. Рядом с правилом

написано его имя (например, Zυς). В соответствии с этим возникает

следующее индуктивное определение выводимых (или порождаемых)

объектов.

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

Если

— аксиома, то

— выводимый объект.

Если

, ∙∙∙ , Ξ

— выводимые объекты,

получается из них при-

менением правила вывода, то

— выводимый объект.

Процесс порождения объекта согласно данному индуктивному опре-

делению представляется деревом, как доказано в § 6.1.

Определение 9.5.2. Вывод

в исчислении

традиционного типа — ко-

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

ребрам — положительные натуральные числа, остальным вершинам —

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

правила к объектам, сопоставленным вершинам, непосредственно сле-

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

санным ребрам, ведущим в эти вершины, причем количество вершин,

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

соответствующем правиле (обозначим его

), а ребра, в них ведущие,

взаимно-однозначно занумерованы числами от 1 до

Таким образом, правила в исчислении, в отличие от правил в алго-

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

шить какие-то преобразования, но не обязывают нас сделать это. Как

говорят, исчисление порождает объекты.

Пример 9.5.2.

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

или перевертышей (слов типа ‘кабак’), в алфавите

. Пусть

— пере-

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

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

путаницы при рассмотрении правил, относящихся, например, к импликации.

232

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

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

. Аксиомами

являются пустое слово, обозначаемое (для того, чтобы его увидеть)

и любая буква

. Правило вывода единственное и с одной посылкой.

ξΞξ

Вывод перевертыша ‘потоп’имеет вид (здесь последовательные при-

менения правил мы не станем полностью разворачивать в дерево):

ото

потоп

Предложение 9.5.1. Объект Ξ выводим в исчислении I тогда и только

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

Следствие теоремы 6.1.

На самом деле выводимым оказывается любой объект, встречаю-

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

типа позволяют порождать и использовать лишь абсолютно правильные

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

применять никаких гипотез, допущений и т.п. С точки зрения современ-

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

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

кроме того, что он считает истинным. Но с чисто математической точ-

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

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

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

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

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

тождественную истинность всех доказуемых объектов). Корректность,

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

возможность вывести любой семантически правильный объект в нашем

исчислении. Полнота не является столь обязательным свойством, а за-

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

иметь ее стоит.

Пример 9.5.3.

Рассмотрим исчисление

равенств натуральных чисел,

представленных в следующей форме:

как

раз

z }| {

SS ∙∙∙S 0 .

9.5. ИСЧИСЛЕНИЯ ТРАДИЦИОННОГО ТИПА

233

Язык

состоит из равенств

n = m

Аксиома единственная:

0 = 0

. Правило вывода также одно:

n = m

Sn = Sm

Легко видеть, что это исчисление полно и корректно относительно

обычной интерпретации равенств.

Пример 9.5.4.

Немного изменим определение натурального числа из про-

шлого примера, отбросив

. После этого, наряду с исчислением, полу-

чающимся из предыдущего заменой аксиомы на

‘=’

, можно сформулиро-

вать исчисление

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

вило

n = m l = k

nl = mk

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

умножение. Тем не менее можно доказать, что ни одно дерево вывода в

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

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

влением данных. Вывод представлен как дерево. Но дерево плохо тем,

что его ветви абсолютно независимы, и получив однажды n = n, мы

должны на другой ветви получать его вновь. Нельзя ли перейти к бо-

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

жество раз одни и те же куски вывода?

Таким представлением является сеть вывода. Ниже дана сеть выво-

да формулы

8 = 8, более короткая, чем соответствующее дерево.

SSSSSSSS = SSSSSSSS

↓ ↓

SSSS = SSSS

↓ ↓

SS = SS

↓

S = S

↓

(9.14)

234

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

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

вания в математическом тексте. Это последовательность объектов. Ка-

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

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

Известно, что при преобразовании сети в дерево количество объектов в

выводе порою растет экспоненциально, т. е. пропорционально

c ∙a

, где

a > 1, n — количество объектов в выводе, c — константа.

Если исчисление содержит правила вывода, то возникает еще одно

важное понятие.

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

Правило

допустимо в исчислении

, если множе-

ство выводимых объектов не изменяется после добавления

Например, правило Π

допустимо в исчислении E из примера 9.5.3.

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

9.5.1. Что получится, если опустить требование конечности дерева в

определении вывода?

9.5.2. Верно ли, что в рассмотренном выше исчислении для подстано-

вок порядка k любая подстановка, встретившаяся в выводе, явля-

ется выводимой?

9.5.3. Докажите, что в расширенном исчислении из примера 9.5.4

n=n

выводится не менее чем за n применений правил.

9.5.4. Пусть задано исчисление традиционного типа, в котором языком

является множество всех слов в алфавите

{abc}, аксиомой — a,

правилами вывода

XaY

XabY

XaY

XcY

XcbbY

XbbaY

Здесь

X, Y

— произвольные слова.

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

bbcb.

2. Построить граф выводимых слов не более чем из пяти букв;

слова

связаны ребром, если

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

3. Привести пример слова, имеющего два существенно различ-

ных вывода.

4. Привести пример невыводимого слова.

9.5. ИСЧИСЛЕНИЯ ТРАДИЦИОННОГО ТИПА

235

9.5.5. Пусть задано исчисление Ξ традиционного типа, в котором язы-

ком является множество всех слов в алфавите {ab}, аксиомой —

b, правилами вывода

aXa

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

2. Дать семантику, относительно которой данное исчисление

было бы полным.

3. Показать, что правило

XbY YbZ

XbZ

допустимо в исчислении Ξ.

9.5.6. Рассмотрим теорию AA над языком слов в алфавите

{S+=}

c ак-

сиомой += и правилами вывода

X + Y = Z

XS + Y = ZS

X + Y = Z

X + Y S = ZS

1. Вывести

SS+SSS=SSSSS

2. Доказать, что правило

X + Y = Z

Y + X = Z

допустимо в исчислении AA.

3. Доказать, что AA полно и корректно для сложения натураль-

ных чисел.

9.5.7. Рассмотрим исчисление в алфавите {()}. Аксиома:

Λ. Правила

вывода:

(Ξ)

Ξ Ψ

ΞΨ

1. Охарактеризовать выводимые объекты.

2. Доказать полноту исчисления.

236

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

9.5.8. Видоизменим второе правило предыдущего исчисления на

Ξ Ψ

(ΞΨ)

Чем это исчисление отличается от предыдущего?

9.5.9. Рассмотрим исчисление в языке выражений в алфавите

()irbctˆ.

Аксиомы его —

{i, r, b, c}.

Правила вывода:

. . . ξ

(ξ

. . . ξ

)

ˆξ

ξ ξ

Здесь ξ — произвольное слово, T — слово из букв t. Вывод —

конечный граф, начальными вершинами которого являются акси-

омы,

в каждом применении правила I отлично от использован-

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

меняется хотя бы одно правило P. Выводимые объекты — встре-

чающиеся в выводе.

определено в выводе Σ, если оно является

заключением правила I.

1. Показать, что все

, встречающиеся в любом выводе, опре-

делены.

2. Показать,что если сопоставить нашим выражениям типы Па-

скаля по принципу:

i → integer; r → real; b → boolean;

c → char; (ξ

. . . ξ

) → record a1 : x

; . . . an : x

end;

ˆξ → ˆx; (здесь

— идентификатор a, определенный опи-

санием type a=x; x — тип, сопоставленный выражению ξ,

— произвольные неповторяющиеся идентификаторы), то

наше исчисление может рассматриваться как способ вывода

корректных описаний типов языка Паскаль.

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

кле было правило P, наше исчисление становится некоррект-

ным.

9.6. СЕКВЕНЦИИ

237

9.5.10. Сформулировать полное и корректное исчисление для равенств

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

помощи операций сложения.

9.5.11. Сформулировать полное и корректное исчисление для равенств

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

помощи операций сложения и умножения.

§ 9.6. СЕКВЕНЦИИ И ФОРМАЛИЗАЦИЯ

СЕМАНТИЧЕСКИХ ТАБЛИЦ

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

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

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

структуру.

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

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

ными” словами в нестрогом описании. Важнейшее из них — секвенция.

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

Секвенция отображает некоторую стадию построения подтаблицы

и состоит из всех результатов, полученных в ней в данный момент. Эти

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

полнительными спецификациями.Далее,при интерпретации секвенции

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

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

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

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

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

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

Данные соображения лежат в основе “парадоксального” определения

истинности секвенции ниже.

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

Если задано множество спецификаций

, и

α ∈ S

— формула, то

αA

— специфицированная формула.

Секвенция

—

набор специфицированных формул.

Классическая секвенция

— секвен-

ция, где

есть

{|=, =|}

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

катов.

Мы специально дали достаточно общее определение, поскольку се-

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

238

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

скими буквами Γ, Δ, Λ (возможно с индексами) будем обозначать произ-

вольные (возможно пустые) наборы специфицированных формул. Ак-

сиомы исчисления секвенций — секвенции вида Γ⊕{|= A, =| A}. Вид-

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

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

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

точно показать технику переформулировок на примере правил для

⇒ и

∀.

|=⇒

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

}

Γ ⊕ {|= A ⇒ B}

=| ⇒

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

Γ ⊕ {=| A ⇒ B}

|= ∀

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

Γ ⊕ {|= ∀x A(x)} ⊕ {|= A(c

)}

=| ∀

Γ ⊕ =| ∀x A(x)

Γ ⊕ {|= A(c

n+1

)}

(9.15)

Правила для всеобщности требуют пояснения. Там, где берется ста-

рая константа, мы сохраняем |= ∀x A(x) с тем, чтобы его можно было

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

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

нет.

Исчисление секвенций — традиционного типа.Для нашего конкрет-

ного случая семантических таблиц (секвенций) нежелательные эффек-

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

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

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

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

правило вывода преобразует в результате лишь одну формулу; говорят,

что оно применяется к этой формуле. Далее, формула, к которой приме-

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

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

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

формул,входящих в полученную секвенцию.Это свойство подформуль-

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

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

логических систем.

Исчисление секвенций создано немецким логиком Г. Генценом

(G. Gentzen) в 1934 г.

Сам Генцен, и вслед за ним большинство логиков

Его судьба была трагична. Он стал членом нацистской партии и ректором Пражского

университета во время немецкой оккупации. За это он был расстрелян в 1945 г.

9.6. СЕКВЕНЦИИ

239

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

фигура Γ → Δ, где Γ и Δ — наборы формул.Γ соответствует формулам,

специфицированным как истинные, а Δ — как ложные. Пример дерева

вывода в исчислении секвенций:

|= A, |= B, =| A |= A, |= B, =| B

|= A, |= B, =| A&B

↑

|= A, =| (B ⇒ A&B)

↑

=| A ⇒ (B ⇒ A&B)

(9.16)

В связи с локальной структурой дерева вывода появляется еще одно

важное понятие. Если секвенция

Δ находится в дереве выше секвен-

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

определить подформулу одной из формул Γ, в которую она переходит.

Например, =| B из листа 2 переходит в подчеркнутую B в исходной

=| A ⇒ (B ⇒ A&B). Дадим строгие определения.

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

Для правила

|=⇒ =| A

в одном из аргументов и

|= B

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

|= A ⇒ B

. Они соответствуют посылке и заключению этой импли-

кации. Для правила

=| ⇒

(непосредственными) результатами разбие-

ния являются

=| B

|= A

. Соответствие определяется аналогично. Для

аргумента правила

|= ∀ |= A(c

)

— (непосредственный) результат, а

|= ∀x A(x)

— результат разбиения

|= ∀xA(x)

в результирующей се-

квенции.Первый из них соответствует подформуле

A(x)

,второй —всей

формуле. Для правила

=| ∀ =| A(c

n+1

)

— (непосредственный)результат

разбиения

=| ∀x A(x)

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

A(x)

. Для осталь-

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

рым применяется правило, определяются аналогично. Для всех формул

из

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

заключении правила.

Если A есть результат разбиения B, B — результат разбиения C, то

A есть результат разбиения C и соответствует той подформуле C, кото-

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

, соответствующей B в C, подфор-

муле A

, соответствующей A в B

. Определим истинность и ложность

Часто результаты разбиения называют предками соответствующей формулы. Но эта

240

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

секвенции в интерпретации.

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

Секвенция

истинна в интерпретации

, если хо-

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

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

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

блицы =| A, мы стремимся вывести секвенцию {=| A}, истинность ко-

торой означает истинность A.

Теорема 9.1. (Теорема корректности для исчисления секвенций)

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

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

Базис. Пусть вывод состоит из одной секвенции. Тогда она является

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

истинная, и как ложная. Один из ее экземпляров и противоречит специ-

фикации.

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

квенций

< n. Докажем ее для секвенций, выводимых за n шагов. Разбе-

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

для ⇒ и ∀. Остальные рассматриваются аналогично. Пусть последним

применялось правило =| ⇒, получена Γ ⊕{=| A ⇒ B}из Γ⊕{=| B}⊕

{|= A}. По предположению индукции, исходная секвенция истинна в

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

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

истинны либо ложны в любой интерпретации

. Если аргумент ложен,то

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

тинна. По таблице истинности для ⇒, ложно A ⇒ B. Обратно, если

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

ложно A ⇒ B.По таблице истинности,тогда истинна A и ложно B. Зна-

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

результата эквивалентны, эквивалентны и условия их истинности.

Для правила =| ⇒ установим эквивалентность истинности обоих

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

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

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

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

шие).

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

бы сказать: секвенции в посылке и заключении эквивалентны.