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

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

10.5. СУПЕРСТРУКТУРЫ И ТЕОРЕМА ЛОСЯ

291

некоторое n

. Фильтр, состоящий из всех множеств, содержащих некоторе x

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

бой фильтр, а множество всех конечных множеств является фильтром. Значит,

есть ультрафильтр, содержащий лишь бесконечные множества

. Но вот по-

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

что:

Предложение 10.5.7. В теории множеств нет такой формулы A(X), что

∃1X A(X) и такое X является неглавным ультрафильтром на N.

Говорят, что предикат истинен на большинстве элементов I, если множе-

ство истинности предиката принадлежит ультрафильтру над I.

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

ной топологии и функционального анализа. В логике они в основном использу-

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

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

например, одноместный предикат P . Если P (a) = >, P (b) = ⊥, то по опреде-

лению прямого произведения естественно положить P (ha, bi) = h>, ⊥i. Пол-

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

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

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

Возьмем произвольный неглавный ультрафильтр Aнад X.Возьмем семей-

ство моделей (M

)

x∈X

. Ультрапроизведение строится как прямое произведе-

ние

i∈X

, факторизованное по отношению

{(a, b) | {i | a

= b

} ∈ A}.

Таким образом, элементарная формула считается истинной на объектах из уль-

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

ножаемых моделей.

Докажем теперь, что ультрапроизведение моделей теории Th само являет-

ся моделью теории Th. Для этого установим, что любая формула, а не только

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

истинна на большинстве компонент.

Предложение 10.5.8. (Теорема об ультрапроизведениях)Любая формула ис-

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

большинстве компонент.

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

и дизъюнкции индукционный шаг следует из замкнутости ультрафильтра от-

носительно объединений и пересечений. Для отрицания достаточно заметить,

Но, конечно, не все: если и само X, и его дополнение бесконечны, то ультрафильтр

содержит одно и только одно из них.

292

ГЛАВА 10. НЕСТАНДАРТНЫЙ АНАЛИЗ

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

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

другие связки и отрицание. Остаются кванторы. ∀x A(x) ложно в ультрапро-

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

)

i∈I

, такой, что множество таких i ∈ I, что M

|= A(a

), принадлежит уль-

трафильтру. Но если ∀x A(x) ложно на большинстве компонент, то найдется

элемент ультрафильтра X ⊂ I, такой, что для каждого i ∈ X найдется a

, при

котором A(a

) ложно в M

. Эти a

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

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

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

тинна на большинстве компонент ттт она не является ложной на большинстве

компонент.

Итак, если все компоненты ультрапроизведения (и даже их большинство)

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

ее моделью.

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

множество последовательностей стандартных действительных чисел, но эти

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

элементов.

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

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

ко два значения (скажем, 0 и 1), то она равна одному из этих чисел (какому

именно, зависит от ультрафильтра).

Глава 11. Естественный вывод

в классической логике

§ 11.1. О СТРУКТУРЕ МАТЕМАТИЧЕСКИХ

ДОКАЗАТЕЛЬСТВ

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

плохо работают в конкретных теориях. Это скорее чисто логическое сред-

ство. Математик доказывает утверждение, и даже построение контр-

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

ку при этом он также опирается на теорию. При помощи семантических

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

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

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

ке контрпримера.

Рассмотрим типичные блоки математического доказательства. Оно

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

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

ством C” или, что то же самое, “Если объект A таков, что B, то для не-

го выполнено и C”. Далее произносится ритуальная фраза типа “Возь-

мем произвольное x (A), такое, что B”. К выбранному x применяются

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

которым они опять-таки применяются. Порою появляются конструкции

типа: “Докажем следующее вспомогательное утверждение”, “Разберем

по отдельности все возможные случаи”, “Предположим противное...

Полученное противоречие доказывает теорему”, “Аналогично преды-

дущему...”, “Очевидно, что...”. Очевидно, что замечания “Аналогич-

но...” и аналогичное ему ”Очевидно, что...” чаще всего являются ука-

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

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

ставить в формальном виде.

294

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

Для начала проиллюстрируем на классических примерах, как эти

конструкции взаимодействуют между собой. Известно, что математика

как наука началась с доказательства Теэтета

несоизмеримости диаго-

нали квадрата с его стороной

. Воспроизведем, в осовремененных тер-

минах, но пользуясь лишь знаниями, известными во времена Теэтета, ее

доказательство.

Пусть, напротив, некий отрезок

α целое число раз укладывается и в

стороне квадрата, и в его диагонали. Обозначим отношение длины сто-

роны квадрата к α через n, а его диагонали — через m. Без ограничения

общности можно считать, что одно из чисел n, m нечетно. В противном

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

пор, пока они оба оставались бы четными. Далее, по теореме Пифагора,

+ n

= 2n

= m

. Значит, квадрат m — четное число, и следователь-

но, само m четно. Значит, n нечетно, и квадрат его также нечетен. Но

поскольку m четно, m = 2∙k, и m

= 4∙k

. Следовательно, 2∙n

= 4∙k

и сокращая на 2, получаем n

= 2 ∙k

Значит, n — четное число, но это

противоречит сделанному предположению, что среди n, m есть нечет-

ное число. Полученное противоречие доказывает, что такого отрезка α

быть не может.

Данное доказательство имеет сложную логическую структуру. Есть

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

зультата (о том, что одно из чисел n, m может предполагаться нечет-

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

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

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

из XIX века.

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

надлежит данный результат. Одни ссылаются на Филолая, другие утверждают, что он

всего лишь разгласил результаты школы Пифагора, скрывавшиеся от профанов во избе-

жание соблазна. Но Теэтет, во всяком случае, дал ясное и законченное доказательство.

Многие считают, что ее началом была теорема Пифагора, но это, пожалуй, неточно

по следующим причинам. Во-первых, теорема Пифагора имеет естественную и при-

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

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

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

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

римость диагонали со стороной невозможно, теорема Теэтета уже чисто теоретический

результат. Более того, для греков формулировка этой теоремы была и крайне неесте-

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

иначе ее бы не приняли.

11.1. О СТРУКТУРЕ МАТЕМАТИЧЕСКИХ ДОКАЗАТЕЛЬСТВ

295

Докажем, что имеются два иррациональных числа a, b, такие, что a

рационально. Рассмотрим число

√

. В 30-е годы XX века было дано

весьма сложное доказательство того, что это число иррационально, но

в XIX веке это было неизвестно. Тем не менее уже тогда, конечно же,

было известно, что это число либо рационально, либо иррационально.

Разберем оба этих случая по отдельности.

Пусть

√

рационально. Тогда искомые a, b уже найдены и оба рав-

ны

√

. Пусть теперь

√

иррационально. Тогда положим a =

√

b =

√

. Тогда



√



√

2∙

√

= 2.

Итак, в любом случае искомые a, b существуют, что и требовалось

доказать.

Подытожим

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

в каждом из которых мы ссылаемся лишь на ранее доказанные ли-

бо предположенные факты.

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

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

ющих лишь внутри данного вспомогательного вывода. Соответ-

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

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

допущения.

• И основное доказательство, и вспомогательные выводы начина-

ются с постановки цели (того, что требуется доказать) и заверша-

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

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

быть объявлены произвольными.

296

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

§ 11.2. ПРАВИЛА ЕСТЕСТВЕННОГО ВЫВОДА

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

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

ется в нашем пособии и в упражнениях. После появления языков про-

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

перестал быть экзотикой. Никто не пытается сначала дать полное фор-

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

этом языке. А сложность концепций логики и языков высокого уровня

одна и та же.

11.2.1. Общая структура.

Импликация и конъюнкция

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

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

правило позволяет перейти от формул к формулам, например, правило

применения ⇒, обычно называемое “правилом извлечения следствий”

или традиционным латинским именем modus ponens,

A A ⇒ B

позволяет перейти от формул A и A ⇒ B к формуле B. Второе из пра-

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

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

тельный вывод:

∗ A



∙∙∙

A ⇒ B

Вспомогательный вывод (или подвывод) начинается с допущения, отме-

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

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

могательного вывода. Сам вспомогательный вывод может состоять из

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

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

шо известную Вам из языков программирования; на самом деле она бы-

ла заимствована языками программирования из логики). Он помечает-

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

11.2. ПРАВИЛА ЕСТЕСТВЕННОГО ВЫВОДА

297

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

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

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

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

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

имеет доступ только к его допущению и результату). А вот во внутрен-

ние подвыводы результаты, полученные в объемлющих, могут перено-

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

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

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

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

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

ная этого внутреннего блока.

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

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

После этого само следствие уже будет доказано абсолютно, без всяких

допущений.

Как видно, для импликации были два правила: правило, позволя-

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

доказывать импликацию, — правило удаления и правило введения, раз-

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

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

ло в некотором отношении является следствием собирающего: если из

A можно вывести B, то получив A, имеем право заключить и B. Такие

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

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

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

Теперь добавим правила для конъюнкции, которые гораздо проще и

очевиднее:

Соединение Разъединение

A B

A & B

A B

При помощи этих четырех правил можно привести первый пример:

вывод формулы (A ⇒ B) & (B ⇒ C) ⇒ (A ⇒ C). Построим этот

вывод постепенно.

298

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

Итак, нужно доказать импликацию. Для этого необходимо предпо-

ложить посылку и вывести ее заключение.

∗ (A ⇒ B) & (B ⇒ C)



∙∙∙

A ⇒ C

(A ⇒ B) & (B ⇒ C) ⇒ (A ⇒ C)

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

∗ (A ⇒ B) & (B ⇒ C)



A ⇒ B

B ⇒ C

∙∙∙

A ⇒ C

(A ⇒ B) & (B ⇒ C) ⇒ (A ⇒ C)

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

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

заключение C. Но из A по

modus ponens

следует B, а из B — C. В итоге

получаем

∗ (A ⇒ B) & (B ⇒ C)



A ⇒ B

B ⇒ C

∗ A



A ⇒ C

(A ⇒ B) & (B ⇒ C) ⇒ (A ⇒ C)

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

иметь в виду и данные, и цель

11.2.2. Дизъюнкция и разбор случаев

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

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

Нужно помнить известную шутку: “Дурак начинает решать задачу с начала, ум-

ный — с конца, а программист — с середины”.

11.2. ПРАВИЛА ЕСТЕСТВЕННОГО ВЫВОДА

299

зирующийся на дизъюнкции, известен еще со времен Аристотеля. Это

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

Если

A ∨ B, и из A следует C, а из B следует D, то C ∨ D.

Например, если все живущие в Вайвоже — удмурты или русские,

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

рыжие или русые.

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

ся как следующее правило:

Конструктивная дилемма:

A ∨ B

∗ A



∙∙∙

∗ B



∙∙∙

C ∨ D

Но при чисто формальном рассмотрении данного правила возникает

ряд частных, однако тонких вопросов. Что делать, если C и D совпада-

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

сти C ∨ D из C? Хоть последний переход и кажется ненужным, но он

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

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

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

Правило разбора случаев:

A ∨ B

∗ A



∙∙∙

∗ B



∙∙∙

Правила ослабления:

A ∨ B

Покажем, как при помощи только что введенных правил получить

правило конструктивной дилеммы. Пусть имеются A ∨ B и выводы

: C из A и Σ

: D из B. Тогда можно вывести C ∨ D.

Конструктивная дилемма:

A ∨ B

∗ A



C ∨ D

∗ B



C ∨ D

300

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

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

сколькими фиксированными шагами вывода. Такие правила называют-

ся выводимыми в исчислении.

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

ет, что и известное правило цепного заключения, или правило силлогиз-

ма, также выводимо:

A ⇒ B B ⇒ C

A ⇒ C

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

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

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

туру.

11.2.3. Отрицание. Приведение к абсурду

и “от противного”.

A ∨ ¬A

Теперь перейдем к правилам для отрицания. Чтобы доказать отрица-

ние ¬A, необходимо предположить A и вывести из него противоре-

чие. Только тогда мы можем с уверенностью заявить, что A ложно. Дан-

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

латыни

reductio ad absurdum

. Такой способ, конечно же, противоречит

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

ниях наших депутатов) приему: чтобы опровергнуть A, нужно просто

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

этого не может быть; чтобы доказать A, нужно прежде всего предпо-

ложить само A. Математик не имеет права пользоваться грязными при-

емами, стремясь доказать A, он имеет право предположить лишь про-

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

касающееся отрицания, несколько необычно: это просто правило сня-

тия двойного отрицания.

Reductio ad absurdum:

∗ A



∙∙∙

¬A

Двойное отрицание:

¬¬A