«Прикладная логика Учебное пособие Рекомендовано Государственным комитетом Российской Федерации по высшему образованию в качестве учебного пособия для студентов высших учебных заведений, обучающихся по специальностям ...»

Разберемся в разнице между конкретной теорией и логикой. Почему теорию множеств безоговорочно считают конкретной, а вот язык предикатов — логическим? Для этого рассмотрим множество интерпретаций, в которых истинны теоремы теории множеств и множество интерпретаций, в которых истинны логические теоремы. Логические теоремы — тавтологии, и поэтому истинны в любых интерпретациях. Теоремы теории множеств истинны лишь в ее моделях. Очевидно, что класс всех интерпретаций намного шире и намного проще определен, чем класс моделей теории множеств.

Проницательный читатель может заявить: а ведь формулируя определение интерпретации, мы также принимали целый ряд предположений! Приведем два наиболее явственных: логических значений лишь два, универс непуст... А сколько еще неявных предположений пролезло с использованными математическими терминами? Ну ладно, насчет теории множеств я еще могу согласиться, что это — слишком конкретная теория, но чем хуже, например, отношение порядка, чем отношение равенства? Почему теория частичного порядка считается математической, а не логической?

Как часто бывает, кое в чем читатель прав. В вопросе стоит разобраться с другой стороны. Чем же помешает отношение порядка? Рассмотрим простую теорему, явившуюся одним из первых строго установленных свойств классической логики. Пусть A(x1,..., xn ) — формула.

Определим предикатор как выражение вида x1,..., xn A(x1,..., xn ).

Здесь служит квантором, связывающим переменные x1,..., xn. Предикатор служит синтаксическим объектом для подстановки вместо предикатов. Теперь можно определить подстановку предикатора вместо предиката аналогично тому, как мы делали для термов и переменных. Заменяются лишь базисные шаги.

Как и для термов, подстановку часто сокращенно обозначают Следующее свойство выполнено лишь для тавтологий и практически всегда нарушается в конкретных теориях. Оно является в некотором смысле характеристическим свойством логики вообще, в отличие от частных теорий; гранью, отделяющей логические теории от прикладных. Логические теории рассчитаны на весьма общий класс интерпретаций. Прикладные имеют в виду конкретный класс моделей со специфичной интерпретацией предикатов и функций7.

В этом смысле самые абстрактные из математических теорий, например, теория множеств и теория категорий, называются в логике прикладными.

ГЛАВА 8. СЕМАНТИКА КЛАССИЧЕСКОЙ ЛОГИКИ

Теорема 8.3. (Теорема о подстановке вместо предикатов) Если C является тавтологией классической логики, P — n-арный предикат, n-местный предикатор со свободными переменными xn+1,..., xm, то тавтологией является и формула C{P | A}} Доказательство. Рассмотрим два случая. Пусть сначала P не входит в A. Поскольку P не входит в C{P | A}, по любой интерпретации этой формулы строится интерпретация самой C, в которой она имеет то же значение, определяя P (t1,..., tn ) через значение A(t1,..., tn ). А по предположению C — тавтология. Значит, результат замены истинен во всех интерпретациях.

Пусть теперь P входит в подставляемый предикатор. Тогда любое вхождение P в C{P | A} является результатом одной из замен, и по любой интерпретации M формулы C{P | A} строим другую интерпретацию M1 для C, такую, что Для этого заменяем значение P на соответствующее значение A.

Теперь рассмотрим расширение языка логики предикатов, в котором сохраняется теорема о подстановке вместо предикатов. Разрешим всевозможные конечные типы, построенные из исходных типов o и t (объекты и логические значения), и выдающие результатом логические значения. Таким образом, теперь аргументами предикатов могут быть предикаты. Разрешим переменные по каждому типу и обычные кванторы всеобщности и существования по каждому типу. Итак, теперь у нас могут быть переменные по логическим значениям, переменные по одноместным обычным предикатам, переменные по предикатам, первым аргументом которых служит двуместный предикат, вторым — логическое значение, третьим — объект и т. д., и т. п. Но поскольку язык строго типизирован, переменные для каждого типа объектов свои, и для каждого аргументного места предиката точно указывается тип соответствующего аргумента. Полученную систему назовем общим логическим языком конечных типов.

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

Теперь хотелось бы дать синтаксический метод проверки логического следования, но доказано, что полной формализации не может быть уже для языка второго порядка, включающего лишь переменные по предикатам, аргументами которых являются объекты. Более того, если теорема полноты показала, что понятие общезначимости в классической логике предикатов определяется полностью и однозначно, то здесь появляется глубоко скрытая, зато неустранимая, неоднозначность. Уже в логике второго порядка появляются формулы, общезначимость которых зависит от неразрешимых проблем современной математики и теории множеств. Подробнее мы вернемся к этому после накопления соответствующего аппарата, а пока что необходимо сделать предупреждения.

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

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

Опираясь на принцип свертки, можно обосновывать многие полезные свойства понятий высших порядков. Например, устанавливается существование булевых операций над предикатами любых типов. Ниже рассмотрена формула, выражающая существование объединения множеств объектов. Здесь мы иллюстрируем еще один часто применяемый способ различения переменных разных типов: переменные для предикатов изображаются большими буквами, а их местность — скобками с соответствующим числом аргументных мест. Таким образом, все большие буквы здесь типа o t, где o — тип объектов.

Общее свойство логик — отсутствие конкретных понятий.

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

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

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

ГЛАВА 8. СЕМАНТИКА КЛАССИЧЕСКОЙ ЛОГИКИ

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

8.5.1. Студент Гениалькис заявил, что никакие предикаторы не нужны, поскольку у нас есть квантор свертки, и лучше подставлять просто множества. Можете ли Вы ему возразить?

Глава 9. Семантические таблицы для классической логики

ОТ ТАБЛИЦ ИСТИННОСТИ

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

§ 9.1.

Рассмотрим построение таблицы истинности пропозициональной формулы (A B C) (A B) (см. табл. 9.1). Анализируя таблицу, можно отметить, что большинство информации в ней избыточно. Таблицу можно значительно сократить, пользуясь следующими правилами: для истинности дизъюнкции достаточно истинности одного из членов; для ложности конъюнкции достаточна ложность одного из членов;

истина следует из всего что угодно; из лжи следует все что угодно. Сокращенная таблица истинности показана на табл. 9.2.

При таком сокращении самым тонким местом является проверка того, что ни один случай не упущен. Можно создавать много способов сокращения таблиц истинности, но в некотором смысле все это будет

A B C BC ABC AB

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

A B C BC ABC AB

Таблица 9.2: Сокращенная таблица истинности изобретением велосипеда, поскольку, базируясь на правилах сокращения, голландский логик Бет (E. W. Beth) создал в 50-х годах формализм, гарантирующий полноту разбора и выполняющий все прямые сокращения. Он основан на необходимых и достаточных условиях истинности и ложности формул. Начнем с примера для той же формулы.

Ищем все возможные случаи, когда формула ложна. Если таковых не найдется, то она истинна. Наша формула представляет собой импликацию, импликация ложна, если ее посылка истинна, а заключение ложно.

Получаем следующее преобразование:

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

Бет оптимально подобрал два случая, исчерпывающих все возможности, когда импликация истинна: необходимо и достаточно, чтобы A было ложно либо B истинно. То, что мы разбираем два независимых случая, отражается разбиением таблицы на подтаблицы, в которых общее лишь логично разобьется и дизъюнкция.

Здесь в двух из трех образовавшихся подтаблиц встретились противоречия; такие подтаблицы называются закрытыми и отмечаются двойной чертой. Оставшаяся подтаблица выдала тот единственный набор значений, при котором формула ложна: A истинно, B ложно и C истинно. Итак, мы получаем следующий метод проверки истинности формулы либо построения контрпримера. Предполагаем, что формула ложна.

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

ПРАВИЛА РАЗБИЕНИЯ ФОРМУЛ

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

§ 9.2.

Просуммируем правила разбиения для связок логики высказываний.

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

Теперь остается заняться практикой и не забывать, что в любом доказательстве правильная общая структура значит не меньше, чем праГЛАВА 9. КЛАССИЧЕСКИЕ СТ вильность отдельных шагов. Хорошо и то, что любая последовательность правильных шагов приводит к результату, хотя, конечно, удачный выбор порядка разбиений может сильно сократить таблицу.

9.2.1. Мы научились проверять на семантических таблицах высказывания на тождественную истинность. А как их проверять на тождественную ложность? Что в этом случае даст незакрытая семантическая таблица?

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

9.2.4. (A&B C) (A C) (B C) 9.2.5. (A C) (B C) (A&B C) 9.2.6. (A&(B C)) (A&C) (B&C) 9.2.7. (A&(B C)) (A&C) (A&B) 9.2.8. (A&B) (A&C) (A&(B C)) 9.2.9. ((A B) (C D)) (A C)&(D B) 9.2.10. ((A B) C) A (B C) 9.2.11. A (B C) ((A B) C) 9.2.12. (A (B&C)) (A B)&(A C) 9.2.13. (A B)&(A C) (A (B&C)) 9.2.14. (¬A B)&(A C) B C 9.2.15. B C (¬A B)&(A C) 9.2.16. (A B)&(A C)&(A D) ¬A 9.2.17. (B A)&(C A)&(D A) A 9.2.18. (A B C)&(B ¬A)&(C D)&(D B) (A E) 9.2.20. (A B C)&(¬A C) B C 9.2.21. ((A C) D)&¬D A&¬C 9.2.22. (A B)&(B C) (¬A C) 9.2.23. Майор Тронин в результате расследования установил, что два сотрудника организации п/я № 13 являются агентами. Медников — агент английский либо американский, а Иванов — английский либо израильский. С присущей ему проницательностью тов. Тронин сделал вывод, что п/я № 13 находится под контролем “Intelligence Service”. Прав ли он?

9.2.24. Если в России пытаются проводить реформы, то начинается смутное время. Если начинается смутное время, то либо наступает гражданская война, либо иностранное нашествие, либо Россия теряет часть территорий. Если наступает гражданская война, то население испытывает ужасные бедствия. Не лучше приходится населению и при нашествии. Сейчас в России пытаются проводить реформы. Значит, российский народ ждут ужасные бедствия.

9.2.25. (L. Carroll*) Он никогда не поет больше часа. Если кто-то поет больше часа, он надоедает окружающим. Тот, кто не надоедает окружающим, — желанный гость. Значит, он — желанный гость.

9.2.26. Создайте правила разбиения для эквивалентности и на их основе постройте семантическую таблицу для ((A B) C) 9.2.27. (J. Venn) Существовал клуб с такими правилами:

1. Члены финансового комитета должны избираться среди членов общей дирекции.

2. Нельзя быть одновременно членом общей дирекции и членом библиотечного комитета, не будучи членом финансового 3. Ни один член библиотечного совета не может быть членом финансового комитета.

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

Упростите правила.

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

§ 9.3.

В отличие от таблиц истинности, метод семантических таблиц обобщается на всю логику предикатов. Здесь техническое улучшение, которым казалось исключение лишних случаев из перебора, переходит в принципиальное. Это — типичная ситуация в истории науки. Стремление улучшить изложение какого-то темного места гораздо чаще приводит к принципиальным открытиям, чем амбициозные попытки перевернуть науку и создать какую-либо “общую теорию всего”. Теория относительности была создана Эйнштейном в результате доводки до логического конца анализа электродинамики движущихся тел, общая теория относительности также почти как техническое улучшение интенсивно ведшихся в то время многими крупными учеными работ по применению тензорных методов к механике. А вот все его многолетние усилия создать общую теорию поля не привели ни к чему. Лобачевский создал неевклидову геометрию, пытаясь усовершенствовать изложение геометрии для исключительно тупого контингента слушателей, примерно соответствующего нынешнему факультету повышения квалификации1.

Рассмотрим условия истинности и ложности всеобщности и существования. Поскольку x A истинна тогда и только тогда, когда A(c) истинно для любого конкретного c, мы, имея |= x A, можем получить A(ci ) всякий раз, когда в таблице либо подтаблице появляется объект ci.Если же = x A, то мы знаем лишь, что существует такой объект a, для которого A(a) ложно. Чтобы отобразить это, постулируем = A(cn+1 ) для нового, ранее в таблице не встречавшегося, объекта cn+ (называемого вспомогательной константой). Таким образом, приходим к следующим правилам разбиения для кванторов.

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

Рассмотрим пример: проверка формулы В дальнейшем для единообразия вспомогательные константы обозначаются c1, c2,... Мы ввели объект c1, рассмотрев |= x A(x), после чего подставили его в две другие кванторные формулы. Следующий пример показывает, что не всегда удается обойтись одним объектом.

Здесь видно, что нам пришлось использовать |= x (A(x) B(x)) дважды: для c1 и c2. И именно из-за различия этих двух значений таблица не закрылась; незапертая подтаблица дает следующую опровергающую модель:

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

Следующий пример иллюстрирует еще две особенности, возникающие в предикатных семантических таблицах: возможность бесконечного порождения констант и аномалия с первым объектом. Он заодно показывает, что незапертость подтаблицы приходится порою усматривать более или менее косвенно, а не устанавливать доведением построения до конца, и что одна и та же формула может использоваться бесконечное количество раз.

Итак, бесконечно порождаются новые константы ci, для которых выполнено |= A(ci, ci+1 ), но = A(ci, ci ). Немного разобравшись с анализируемой формулой, мы видим, что построенная опровергающая модель отнюдь не минимальная. Достаточно было бы рассмотреть множество из двух элементов.

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

9.3.1. [K] Некоторые цыплята — кошки. Некоторые кошки знают французский язык. Значит, некоторые цыплята знают французский.

9.3.2. x (A(x) y A(y))2.

9.3.3. x (A B(x)) A x B(x).

Р. Смальян прокомментировал это высказывание следующим анекдотом. Заходит ковбой в бар и говорит бармену: “Мне налей и всем налей. Такой уж я человек: когда я пью, все пьют”. Через некоторое время: “Мне повтори и всем повтори. Такой уж я человек: когда я пью, все пьют”. Затем кладет на стойку деньги: “С меня возьми и со всех возьми. Такой уж я человек: когда я плачу, и все платят”.

9.3.4. x (A(x) B(x)) x A(x) x B(x).

9.3.5. x A(x)&x (¬A(x) B(x)) x B(x).

9.3.6. x A(x)&x B(x) x (A(x) B(x)).

9.3.7. xA(x)&xC(x)&xB(x) x(A(x)&B(x)&C(x)).

9.3.8. x (A(x)&B(x)) x A(x)&x B(x).

9.3.9. (xA(x) xB(x)) x(A(x) B(x)).

9.3.10. ¬x(A(x) B(x)) xA(x)&xB(x).

9.3.11. xyA(x, y)&xyB(x, y) xy (A(x, y)&B(x, y)).

9.3.12. x(A(x) B(x))&(xA(x) xC(x))&x(B(x) C(x)) 9.3.13. x (A(x) B(x))&x(A(x) C)&x(C B(x)) xB(x).

9.3.14. x(A(x) B(x))&x¬A(x)& xy(B(x) C(y))&xD(x) x(C(x)&D(x)).

9.3.15. xy (A(x) B(y))&(xA(x) C) (C zB(z)).

9.3.16. xy(A(x) B(y))&(xC(x) xA(x))&x(¬C(x) B(x)) 9.3.17. ¬(xA(x) yB(x, y)) x¬A(x).

9.3.18. xy (A(x) B(y)) (xA(x) xB(x)).

9.3.19. x(A(x) B(x))& x(B(x)&¬C(x)) x(B(x)&¬A(x)).

9.3.20. (xB(x) xC(x))& x(C(x) B(x)) xB(x).

9.3.21. x (C(x) B(x)&D(x))& x(A(x)&C(x)) x(A(x)&B(x)).

9.3.22. [K] Некоторые птицы, гордящиеся своим хвостом, не могут петь.

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

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

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

9.3.23. [K] Все львы свирепы. Некоторые львы не пьют кофе. Следовательно, некоторые из тех, кто пьет кофе, не свирепы.

9.3.24. [K] Ни одно ископаемое животное не может быть несчастно в любви. Устрица может быть несчастна в любви. Следовательно, некоторые устрицы — не ископаемые животные.

9.3.25. [K] Золото тяжелое. Ничто, кроме золота, не может заставить его замолчать. Следовательно, ничто легкое не может заставить его замолчать.

9.3.26. Некоторые лампочки плохо светят. Лампочки предназначены для того, чтобы светить. Следовательно, некоторые вещи, предназначенные для того, чтобы светить, светят плохо.

9.3.27. [K] Некоторые подушки мягкие. Ни одна кочерга не мягкая. Следовательно, некоторые кочерги — не подушки.

9.3.28. [K] Лишь тот, кто храбр, достоин славы. Некоторые хвастуны — трусы. Следовательно, некоторые хвастуны недостойны славы.

9.3.29. [K*] Необразованные люди обо всем судят поверхностно. Среди студентов Удмуртского университета есть и образованные люди.

Значит, некоторые студенты УдГУ не судят обо всем поверхностно.

9.3.30. [K*] Все козлята прыгают. Ни одно молодое животное не прыгает, если оно не здорово. Следовательно, все молодые козлята здоровы.

9.3.31. Некоторые козы любят сено. Ни одна собака сена не любит. Значит, некоторые собаки — не козы.

9.3.32. Те, кто что-то учил, решили некоторые задачи. Андрей не решил ни одной. Значит, он не учил ничего.

9.3.33. Все рыбаки любители приврать. Все священники соблюдают заповеди. Никто не может и соблюдать заповеди, и вместе с тем врать. Значит, ни один рыбак не священник.

9.3.34. Не все политики мошенники. Все мошенники умны. Значит, некоторые политики глупы.

9.3.35. Студенты — любители покушать. Некоторые студенты худые.

Не все те, кто любит покушать, студенты. Значит, некоторые любители покушать не являются худыми студентами.

9.3.36. Все мафиози жестоки. Некоторые чеченцы жестоки. Следовательно, некоторые чеченцы — мафиози.

9.3.37. Все шутки для того и предназначены, чтобы смешить людей. Ни одно постановление Думы не является шуткой. Значит, ни одно такое постановление не предназначено для того, чтобы смешить

СОКРАЩЕННЫЕ СЕМАНТИЧЕСКИЕ ТАБЛИЦЫ

§ 9.4.

Рассмотрим случай, когда часть компонент в формуле избыточна. Построим таблицу для формулы Здесь видно, что разбор вариантов по первой импликации ничего не дал, и можно было начать сразу со второй, получив гораздо более приличную таблицу.

Но как это усмотреть в самой таблице? В таблице (9.8) еще до ее разбиения появилась формула |= B, которая получилась во втором варианте

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

первого разбиения. Значит, в этом варианте ни одной новой формулы не появилось, и мы сделали пустой шаг3.

Определение 9.4.1. Шаг построения таблицы называется избыточным, если хотя бы в одной из получающихся подтаблиц не появляется новых формул, либо если разбивается формула |= x A(x), а в таблице уже имеется формула |= A(ci ), либо разбивается = x A(x), а в таблице уже имеется = A(ci ). Подтаблица называется финальной, если в ней не может быть сделано ни одного неизбыточного применения правил.

Избыточные разбиения просто не нужно делать. Более того, понятие избыточного разбиения позволило нам дать точный ответ на вопрос, когда же можно переходить к построению контрпримера: когда нашли финальную подтаблицу.

На рассмотренных практических примерах видно, что иногда разбор при помощи семантических таблиц можно сократить далее. Например, если в подтаблице встречаются формулы |= A B и |= A, то подтаблица с = A сразу же закрывается, и нетривиальна лишь таблица с |= B.

Здесь без нарушения строгости и общности можно обойтись без разделения таблицы и просто добавить |= B. Это правило сокращения формулируется следующим образом:

Modus Ponens — название этого правила в традиционной логике.

Аналогично устанавливаются следующие правила сокращения:

На самом деле ничуть не лучше и формула = A, появившаяся в первом варианте, поскольку элементарная формула A больше нигде не встречается.

Еще один класс правил сокращения, применимых менее часто, это контрприменения, или обращения правил, не разбивающих таблицу. Например, имея |= A и |= B, можно заключить |= A&B. Эти правила целесообразно применять для того, чтобы избежать разбиения таблицы по сложной формуле в ситуации, подобной следующей:

В отличие от предыдущих правил сокращения, которые являлись полностью безопасными, следующие правила сокращают лишь поиск опровержения, а при поиске доказательства заводят в тупик. Они основаны на наблюдении, что семантическая таблица с кванторами не всегда дает минимальную опровергающую модель. Избежать этого можно, разрешив подставлять в кванторные правила, в которых требуется новая константа, константу имеющуюся. Если при такой попытке подтаблица не закрылась, то мы находим опровергающую модель, если же закрылась, то попытка наша неудачна и нужно вернуться к стандартным правилам. Рассмотрим, как с помощью этого приема упрощается построение последней таблицы предыдущего параграфа.

А вот если взять в предпоследней строке c2 вместо c1, наша таблица “закроется”.

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

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

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

Работая в одном направлении (доказательство либо опровержение), нельзя слишком увлекаться приведенными выше послаблениями, поскольку и Ваша первоначальная оценка формулы как истинной либо опровержимой может оказаться неверной, и сама формула в реальных задачах может быть видоизменена, так как никакая формализация не отражает полностью содержания реальной задачи.

При оформлении готового решения эти послабления можно использовать вовсю.

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

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

Избыточное разбиение формул делать не нужно.

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

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

9.4.1. ((A B&C) D)&(C B) (A C).

9.4.2. (A B D&C)&((A C) E)&((A D) H)&(B 9.4.4. (A B D&C) (A C)&(A D)&(B D).

9.4.5. (A C)&(A D)&(B D) (A B D&C).

9.4.6. (A B D&C)&¬A ¬B C D.

9.4.7. A C D (A&¬B C)&(D&B C).

9.4.8. (A&B D C) D (¬C&A ¬B).

9.4.9. (A B D&C)&((A C) E)&((B D) H)& 9.4.13. (A D&C)&((A D) E)&((A C) H)&(E H 9.4.14. ((A B&C) D)&(A B)&(E&A C) (E D).

9.4.15. ((A B&C) D)&(A&E B)&(¬E&A C) D.

9.4.16. (A&H B)&(¬H&A C)&(¬A D) B C D.

9.4.17. (A B C D)&((A D) E)&((A C) E) E.

9.4.19. ((A B) (A C))&((A B C) D)&(D&E 9.4.20. (A B&C)&(B D&E)&(C F )&(E&F G)&(G&D 9.4.21. x(A(x)&B(x))&x(A(x) C(x))&x(B(x) D(x))& 9.4.22. x(A(x) B(x))&x(A(x) C)& 9.4.23. (x A(x) x B(x))& x(C(x) A(x))&x(C(x) D) 9.4.24. x(A(x) xB(x))&x(C(x) A(x))& 9.4.25. xy(A(x, y) B(y, x))&xy(A(x, y) C(x))&

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

9.4.26. xyA(x, y)&xy¬A(x, y)&xy(A(x, y) B(x))& xy(¬A(x, y) C(x)) x(H(x) B(x)&C(x)).

9.4.27. xyA(x, y)&xy(A(x, y)&B(x) C(x, y))& 9.4.28. xyA(x, y)&xy(A(x, y)&B(x) C(x, y))& 9.4.29. x(A(x) y(B(y)&R(x, y)))&x(A(x) y(Q(y) 9.4.30. x(Q(x)&y(B(y) R(x, y))) (x(Q(x) B(x)) 9.4.31.

9.4.32. x(A(x) y(Q(y) ¬R(x, y)))&x(A(x)& y(B(y) R(x, y))) ¬x(¬Q(x)&B(x)).

9.4.33.

9.4.34. x(P (a, x) Q(x, b))&(y Q(y, b) y Q(b, y)) 9.4.35.

¬x(A(x) y(B(y) R(x, y))) ¬x(B(x) A(x)).

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

9.4.37. Если пойдешь в лес весной, тебя укусит клещ. Те, кого кусает клещ, заболевают энцефалитом или им делают укол. Тех, кто заболел, кладут в больницу. В больнице всегда делают уколы. Значит, если весной пойдешь в лес,...

9.4.38. Будешь есть много хлеба, потолстеешь. Толстяки больны и вялы. Больные не могут добиться успеха, если им не повезет. Вялым людям никогда не везет. Значит, чтобы добиться успеха, необходимо...

9.4.39. Старательные люди добиваются успеха. Лишь тот может считаться старательным, кто работает не менее десяти часов в сутки. Нельзя одновременно работать и отдыхать по десять часов в сутки. Легкомысленные люди отдыхают не менее десяти часов в сутки. Следовательно, легкомысленные люди...

9.4.40. Розовая вода приятно пахнет. Ни одно лекарство не пахнет приятно. Если человек болен, он должен принимать лекарство либо соблюдать режим. Соблюдать режим и не принимать лекарство нельзя. Следовательно, если человек употребляет розовую воду, 9.4.41. Если по телевизору не идет интересное кино, то в общежитии собирается веселая компания. Веселая компания всегда шумна.

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

Смотреть телевизор и готовиться к занятиям нельзя. Значит, в общежитии...

9.4.42. Известно, что убийца — Джон, Билл или Джек. Если Джон или Джек — убийца, то убийство было после полуночи. Если убийство было до полуночи, то Джон лжет или Билл — убийца. Если Джон не лжет, то убийца — Билл. Следовательно, Билл — убийца или убийство было после полуночи.

9.4.43. Коля и Вася никогда не бывают вместе. Маша придет на вечеринку только вместе с Колей, Вася — только вместе с Глашей.

Вечеринка веселая, только если на ней присутствуют и Маша, и Глаша. Значит, веселых вечеринок не бывает.

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

9.4.44. Все парни самолюбивы. Ни один самолюбивый студент не аккуратен. Некоторые студенты аккуратны. Значит, некоторые студенты — не парни.

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

§ 9.5.

Исчисление — еще одно важнейшее понятие, наряду с формальным языком и семантикой введенное в число базовых математических конструкций математической логикой. Исчисление I опирается на некоторый формальный язык L и задает подкласс синтаксически правильно построенных объектов этого языка, порождаемых, или выводимых, в I.

Для описания таких объектов и действий с ними используется новый класс синтаксических конструкций — выводы (часто называемые в конкретных исчислениях порождениями либо доказательствами). Выводы включают в себя формулы, термы либо другие объекты языка L, организованные в систему таким образом, что каждый из них связан с ограниченным числом других согласно четким и проверяемым правилам, а глобальная структура вывода также подчинена четким и проверяемым условиям.

Пример 9.5.1. Исчисление, порождающее подстановки порядка n.

Выводимые объекты — векторы вида (i1,, in ), все ik попарно различны и находятся в диапазоне 1 : n. Как известно, такие кортежи задают перестановки чисел 1,, n.

Выводы — циклические ориентированные графы с k пронумерованными вершинами, такие, что вершина i+1 следует за i при i < k, первая следует за k-той, каждой вершине i сопоставлена подстановка i ; подстановка в вершине, следующей за i, является произведением 1 и i.

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

Простейшим подклассом исчислений являются исчисления традиционного типа. Такое исчисление I задается описанием языка L, аксиом, являющихся выражениями языка L, и правил вывода, каждое из коИСЧИСЛЕНИЯ ТРАДИЦИОННОГО ТИПА торых имеет фиксированное конечное число посылок и одно заключение. Правила вывода обычно записываются в следующей форме:

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

формальные объекты, выведенные ранее, к которым разрешается применить правило. Под чертой стоит заключение, или результат: объект, который будет выведен после применения правила4. Рядом с правилом написано его имя (например, Z ). В соответствии с этим возникает следующее индуктивное определение выводимых (или порождаемых) объектов.

Определение 9.5.1. Если — аксиома, то — выводимый объект.

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

Процесс порождения объекта согласно данному индуктивному определению представляется деревом, как доказано в § 6.1.

Определение 9.5.2. Вывод в исчислении I традиционного типа — конечное нагруженное дерево, листьям которого сопоставлены аксиомы, ребрам — положительные натуральные числа, остальным вершинам — пара из имени правила и объекта, получающегося применением данного правила к объектам, сопоставленным вершинам, непосредственно следующим за данной, взятым в порядке, соответствующем числам, приписанным ребрам, ведущим в эти вершины, причем количество вершин, непосредственно следующих за данной, равно количеству посылок в соответствующем правиле (обозначим его n), а ребра, в них ведущие, взаимно-однозначно занумерованы числами от 1 до n.

Таким образом, правила в исчислении, в отличие от правил в алгоритме или предложений в программе, лишь дают возможность совершить какие-то преобразования, но не обязывают нас сделать это. Как говорят, исчисление порождает объекты.

Пример 9.5.2. Рассмотрим исчисление для порождения палиндромов, или перевертышей (слов типа ‘кабак’), в алфавите A. Пусть — переУдвоение терминов имеет здесь смысл для того, чтобы, с одной стороны, подчеркнуть сходство как с импликацией, так и с процедурой, и, с другой стороны, избегнуть путаницы при рассмотрении правил, относящихся, например, к импликации.

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

менная, значениями которой являются буквы в алфавите A. Аксиомами являются пустое слово, обозначаемое (для того, чтобы его увидеть), и любая буква. Правило вывода единственное и с одной посылкой.

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

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

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

На самом деле выводимым оказывается любой объект, встречающийся в некотором выводе. Таким образом, исчисления традиционного типа позволяют порождать и использовать лишь абсолютно правильные конструкции; если они имеют дело с формулами, то они не позволяют применять никаких гипотез, допущений и т. п. С точки зрения современной теории творческого мышления они формализуют полностью рутинный стиль мышления, когда человек не может даже допустить ничего, кроме того, что он считает истинным. Но с чисто математической точки зрения такое свойство традиционных исчислений часто полезно для доказательства точных результатов. Строго сформулировав исчисление, необходимо исследовать для него проблемы корректности и полноты.

Корректность означает согласованность исчисления с семантикой выводимых объектов (в частности, для исчисления традиционного типа тождественную истинность всех доказуемых объектов). Корректность, безусловно, необходима для применения исчисления. Полнота означает возможность вывести любой семантически правильный объект в нашем исчислении. Полнота не является столь обязательным свойством, а зачастую и просто теоретически недостижима. Но уж если она возможна, иметь ее стоит.

Пример 9.5.3. Рассмотрим исчисление E равенств натуральных чисел, представленных в следующей форме: n как Язык состоит из равенств n = m.

Аксиома единственная: 0 = 0. Правило вывода также одно:

Легко видеть, что это исчисление полно и корректно относительно обычной интерпретации равенств.

Пример 9.5.4. Немного изменим определение натурального числа из прошлого примера, отбросив 0. После этого, наряду с исчислением, получающимся из предыдущего заменой аксиомы на ‘=’, можно сформулировать исчисление E1, которое кажется более эффективным, добавив правило где соединение есть просто приписывание одного слова к другому, а не умножение. Тем не менее можно доказать, что ни одно дерево вывода в расширенном исчислении не содержит меньше правил, чем в исходном.

Этот пример ставит важный и тонкий вопрос, связанный с представлением данных. Вывод представлен как дерево. Но дерево плохо тем, что его ветви абсолютно независимы, и получив однажды n = n, мы должны на другой ветви получать его вновь. Нельзя ли перейти к более эффективному представлению, не заставляющему копировать множество раз одни и те же куски вывода?

Таким представлением является сеть вывода. Ниже дана сеть вывода формулы 8 = 8, более короткая, чем соответствующее дерево.

SSSSSSSS = SSSSSSSS

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

Сеть часто представляется в другом виде, более удобном для использования в математическом тексте. Это последовательность объектов. Каждый объект в этой последовательности является либо аксиомой, либо получается по одному из правил вывода из объектов, стоящих ранее.

Известно, что при преобразовании сети в дерево количество объектов в выводе порою растет экспоненциально, т. е. пропорционально c an, где a > 1, n — количество объектов в выводе, c — константа.

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

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

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

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

9.5.2. Верно ли, что в рассмотренном выше исчислении для подстановок порядка k любая подстановка, встретившаяся в выводе, является выводимой?

9.5.3. Докажите, что в расширенном исчислении из примера 9.5.4 n=n выводится не менее чем за n применений правил.

9.5.4. Пусть задано исчисление традиционного типа, в котором языком является множество всех слов в алфавите {abc}, аксиомой — a, правилами вывода Здесь X, Y — произвольные слова.

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

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

слова X, Y связаны ребром, если Y переводится правилом в 3. Привести пример слова, имеющего два существенно различных вывода.

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

9.5.5. Пусть задано исчисление традиционного типа, в котором языком является множество всех слов в алфавите {ab}, аксиомой — b, правилами вывода 1. Показать, какие выражения выводимы в исчислении.

2. Дать семантику, относительно которой данное исчисление 3. Показать, что правило 9.5.6. Рассмотрим теорию AA над языком слов в алфавите {S+=} c аксиомой += и правилами вывода 1. Вывести SS+SSS=SSSSS.

2. Доказать, что правило допустимо в исчислении AA.

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

9.5.7. Рассмотрим исчисление в алфавите {()}. Аксиома:. Правила 1. Охарактеризовать выводимые объекты.

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

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

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

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

Здесь — произвольное слово, T — слово из букв t. Вывод — конечный граф, начальными вершинами которого являются аксиомы, T в каждом применении правила I отлично от использованных в остальных применениях этого правила, в каждом цикле применяется хотя бы одно правило P. Выводимые объекты — встречающиеся в выводе. T определено в выводе, если оно является заключением правила I.

1. Показать, что все T, встречающиеся в любом выводе, определены.

2. Показать, что если сопоставить нашим выражениям типы Паскаля по принципу: i integer; r real; b boolean;

x; (здесь T — идентификатор a, определенный опиc char; (1... n ) record a1 : x1 ;... an : xn end;

санием type a=x; x — тип, сопоставленный выражению, ai — произвольные неповторяющиеся идентификаторы), то наше исчисление может рассматриваться как способ вывода корректных описаний типов языка Паскаль.

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

9.5.10. Сформулировать полное и корректное исчисление для равенств постоянных выражений, составленных из натуральных чисел при помощи операций сложения.

9.5.11. Сформулировать полное и корректное исчисление для равенств постоянных выражений, составленных из натуральных чисел при помощи операций сложения и умножения.

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

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

§ 9.6.

Для того, чтобы доказать корректность и полноту аппарата семантических таблиц для классической логики, необходимо прежде всего полностью формализовать этот термин, превратить его в математическую структуру.

Как обычно, точная формализация требует введения вспомогательных понятий, выявляющих многое из того, что скрыто за “общепонятными” словами в нестрогом описании. Важнейшее из них — секвенция.

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

Секвенция отображает некоторую стадию построения подтаблицы и состоит из всех результатов, полученных в ней в данный момент. Эти результаты, как мы уже видели, не просто формулы, а формулы с дополнительными спецификациями. Далее, при интерпретации секвенции необходимо учесть, что в некотором смысле метод семантических таблиц — метод доказательства от противного. Стремясь убедиться, что формула — тавтология, мы предполагаем, что она ложна, и старательно выискиваем все возможности, чтобы это нежелательное предположение оправдалось. Лишь неудача всех возможных попыток опровергнуть формулу заставляет нас принять, что она тождественно истинна.

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

Определение 9.6.1. Если задано множество спецификаций S, и S, а A — формула, то A — специфицированная формула. Секвенция — набор специфицированных формул. Классическая секвенция — секвенция, где S есть {|=, = }, а формулы являются формулами логики предикатов.

Мы специально дали достаточно общее определение, поскольку секвенции используются и для неклассических логик. Большими гречеГЛАВА 9. КЛАССИЧЕСКИЕ СТ скими буквами,, (возможно с индексами) будем обозначать произвольные (возможно пустые) наборы специфицированных формул. Аксиомы исчисления секвенций — секвенции вида {|= A, = A}. Видно, что аксиомы соответствуют закрывшимся подтаблицам, содержащим противоречия. Теперь правила для семантических таблиц могут быть переформулированы в правила исчисления секвенций. Нам достаточно показать технику переформулировок на примере правил для и Правила для всеобщности требуют пояснения. Там, где берется старая константа, мы сохраняем |= x A(x) с тем, чтобы его можно было использовать и для других констант. Если же введена новая константа, мы уже выжали из квантора все, что возможно, и сохранять его смысла нет.

Исчисление секвенций — традиционного типа. Для нашего конкретного случая семантических таблиц (секвенций) нежелательные эффекты традиционного определения в значительной степени нейтрализуются тем, что нас интересует не столько вся секвенция как целое, сколько отдельные специфицированные формулы, входящие в нее. Еще одной приятной особенностью исчисления секвенций является то, что каждое правило вывода преобразует в результате лишь одну формулу; говорят, что оно применяется к этой формуле. Далее, формула, к которой применяется правило, собирается из своих подформул (возможно, с подставленными значениями свободных переменных). Таким образом, в дереве вывода в исчислении секвенций встречаются лишь подформулы формул, входящих в полученную секвенцию. Это свойство подформульности является чрезвычайно ценной особенностью секвенций и семантических таблиц, делающей их мощным инструментом в исследовании логических систем.

Исчисление секвенций создано немецким логиком Г. Генценом (G. Gentzen) в 1934 г.5 Сам Генцен, и вслед за ним большинство логиков Его судьба была трагична. Он стал членом нацистской партии и ректором Пражского университета во время немецкой оккупации. За это он был расстрелян в 1945 г.

применяют другую систему обозначений: секвенция представляется как фигура, где и — наборы формул. соответствует формулам, специфицированным как истинные, а — как ложные. Пример дерева вывода в исчислении секвенций:

В связи с локальной структурой дерева вывода появляется еще одно важное понятие. Если секвенция находится в дереве выше секвенции, то для каждой из формул имеется возможность однозначно определить подформулу одной из формул, в которую она переходит.

Например, = B из листа 2 переходит в подчеркнутую B в исходной = A (B A&B). Дадим строгие определения.

Определение 9.6.2. Для правила |= = A в одном из аргументов и |= B в другом являются (непосредственными) результатами разбиения |= A B. Они соответствуют посылке и заключению этой импликации. Для правила = (непосредственными) результатами разбиения являются = B и |= A. Соответствие определяется аналогично. Для аргумента правила |= |= A(ci ) — (непосредственный) результат, а |= x A(x) — результат разбиения |= xA(x) в результирующей секвенции. Первый из них соответствует подформуле A(x), второй — всей формуле. Для правила = = A(cn+1 ) — (непосредственный) результат разбиения = x A(x) и соответствует подформуле A(x). Для остальных правил результаты разбиения и соответствия для формул, к которым применяется правило, определяются аналогично. Для всех формул из они сами в аргументе являются результатами разбиения их же в заключении правила.

Если A есть результат разбиения B, B — результат разбиения C, то A есть результат разбиения C и соответствует той подформуле C, которая соответствует в подформуле B, соответствующей B в C, подформуле A, соответствующей A в B 6. Определим истинность и ложность Часто результаты разбиения называют предками соответствующей формулы. Но эта

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

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

Определение 9.6.3. Секвенция истинна в интерпретации M, если хотя бы одна из ее формул противоречит своей спецификации; она ложна, если все формулы соответствуют своим спецификациям.

Таким образом, предполагая в начале построения семантической таблицы = A, мы стремимся вывести секвенцию { = A}, истинность которой означает истинность A.

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

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

Базис. Пусть вывод состоит из одной секвенции. Тогда она является аксиомой. Значит, в ней есть формула, которая специфицирована и как истинная, и как ложная. Один из ее экземпляров и противоречит спецификации.

Шаг. Пусть корректность доказана для всех выводов с числом секвенций < n. Докажем ее для секвенций, выводимых за n шагов. Разберем случаи, когда результирующая секвенция получается по правилам для и. Остальные рассматриваются аналогично. Пусть последним применялось правило =, получена { = A B} из { = B} {|= A}. По предположению индукции, исходная секвенция истинна в любой интерпретации M. Докажем более сильное, чем непосредственно требуется, утверждение: аргумент и результат правила одновременно истинны либо ложны в любой интерпретации7. Если аргумент ложен, то все формулы из удовлетворяют своей спецификации, B ложно, A истинна. По таблице истинности для, ложно A B. Обратно, если результат ложен, то все формулы из специфицированы правильно, и ложно A B. По таблице истинности, тогда истинна A и ложно B. Значит, и аргумент тоже ложен. Поскольку условия ложности аргумента и результата эквивалентны, эквивалентны и условия их истинности.

Для правила = установим эквивалентность истинности обоих аргументов и результата или, что эквивалентно, ложности хотя бы одного из аргументов и ложности результата. Если ложен результат правила, терминология зависит от точки зрения. Если рассматривать исчисление секвенций, то они скорее предки, а если рассматривать таблицы, они — потомки (конечно, измельчавшие).

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

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

По таблице истинности, тогда ложно A или истинно B. Значит, хотя бы одна из посылок истинна. Наоборот, если ложен один из аргументов правила, то все формулы из специфицированы правильно, и ложна посылка импликации либо истинно ее заключение. В любом из этих случаев A B истинна. Теперь рассмотрим правило |=. Если ложен аргумент, то соответствуют своим спецификациям все формулы из результата, поскольку все они входили в аргумент. Если истинен результат, то он полностью входит в аргумент, а A(ci ) истинно, поскольку истинно И наконец, рассмотрим =. Здесь уже не выполнена эквивалентx A(x).

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

A(cn+1 ) может быть истинно в интерпретации M, хотя xA(x) ложно в M. Но:

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

В самом деле, возьмем произвольную интерпретацию M сигнатуры секвенции { = xA(x)}. В ней нет интерпретации для cn+1, поэтому ей соответствует целое семейство (Ma )aU интерпретаций аргумента, отличающихся от M лишь тем, что cn+1 имеет значение a U. В каждой из Ma аргумент истинен по предположению индукции. Если для некоторого a U противоречит своей спецификации одна из формул, то поскольку она не содержит cn+1, она сохранит то же значение и в M, и результат будет истинен. Если же ни для какого a U ни одной такой формулы из не найдется, то в любой Ma = A(cn+1 ) противоречит своей спецификации, и, значит, A(cn+1 ) истинна при любом значении cn+1 из U. По определению истинности, тогда в M истинна xA(x), эта формула противоречит своей спецификации и результат истинен.

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

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

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

Упражнения к § 9. 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. Докажем утверждение xy(x = y y = x).

Семантические таблицы для равенства являются частным случаем семантических таблиц для теории. Пусть нам надо установить, является ли A теоремой Th. Тогда построим вывод секвенции |= Th { = A}.

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

Здесь |= Th означает совокупность всех аксиом Th, специфицированных как истинные. В семантической таблице это означает возможность в любой момент выписать формулу |= B, где B Th. Поскольку аксиом может быть бесконечно много, нецелесообразно требовать обязательно выписывать их все в самом начале.

Правила для логики с равенством можно проинтерпретировать как применение теории со следующими аксиомами: обычная аксиома xx = x и две схемы аксиом где A — произвольная формула, не содержащая других свободных переменных, кроме z.

И наконец, рассмотрим случай, когда в сигнатуре теории присутствуют функции. Здесь действует очень простой закон. Выражения c, f (c), f (f (c)),... считаются различными, если в таблице не установлено равенство каких-либо из них, но ни одно из них не годится как новое, даже если оно еще никуда не подставлялось. Новой может быть лишь вспомогательная константа ci. Когда появляется одна такая константа, то в таблице с функциональными символами она порождает бесконечно много выражений, которые требуется подставлять там, где правило использует старые объекты.

Проверить истинность следующих формул и рассуждений в логике с равенством и/или функциональными символами.

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)) 9.7.7. x y(x = f (y))& x f (f (x)) = x 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. Все павлины гордятся своим хвостом. Если кто-то гордится чемто, не представляющим ценности, то он не может сделать ничего путного. Этот мост сделан павлинами. Все мосты в данной местности, кроме одного, — хорошего качества...

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

9.7.18. Те, кто любит учиться, не нуждаются в поощрениях. Для тех, кто не любит учиться, поощрение бесполезно. Следовательно... 9.7.19. Армия — школа жизни. Если жизнь бестолковая, то такова же и школа. Российская жизнь в данную пору — бестолковая. Только толковая армия может выиграть войну. Значит,...

9.7.20. Чтобы проиграть войну, нужно проиграть хотя бы одно сражение. Наполеон в кампании 1812 г. выиграл все сражения. Эту кампанию он вел с Россией. Значит,... 9.7.21. Суворов во время итальянского похода выиграл все битвы и расстроил все планы противника. Если нет предательства, то расстроить планы противника достаточно для того, чтобы выигрыш битвы гарантировал победу в войне. Суворов проиграл Итальянскую кампанию. Значит,...

9.7.22. (Н. Макиавелли)11 Чтобы добиться успеха, политику необходимо выглядеть добродетельным. Кроме добродетельных и аморальных, никто не может выглядеть добродетельным. Если бы добивались успеха лишь аморальные политики, то никто не был бы добродетельным. Некоторые люди добродетельны...

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

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

Никколо Макиавелли — флорентийский общественный деятель и писатель. Он прославился своими книгами «Государь» и «Республика», в которых безжалостно показывал реальную, совершенно аморальную и бесчестную политику. Например, один из его принципов гласит, что пришедшему к власти в результате переворота правителю нужно опираться не на тех, кто поддержал его из идеи, а на тех, кто примкнул к нему ради выгоды, поскольку первые потребуют выполнения данных им обещаний.

Поскольку такой показ воспринимался как оправдание существующих гадостей, Макиавелли сам заслужил репутацию бесчестного человека, а неприличное поведение политиков до сих пор называют ‘макиавеллизм’. Сам Макиавелли в жизни был приличным человеком, но его вина в том, что он ставил личность ниже государства, что явилось корнем неисчислимых бед в истории.

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

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

§ 9.8.

Теорему полноты есть смысл доказывать не только для логики предикатов, но и для любой теории, базирующейся на классической логике, воспользовавшись сделанным в предыдущем параграфе обобщением семантических таблиц. Нам необходимо установить, что для каждой теоремы A теории Th найдется замкнутая семантическая таблица. Но здесь нужно было бы установить общий метод доказательства любой теоремы, а такового не существует, как будет доказано в разделе, посвященном теории алгоритмов. Поэтому придется действовать от противного: доказать, что незамкнутая семантическая таблица, удовлетворяющая некоторым критериям полноты, дает опровергающую модель для A, т. е. модель Th, в которой ложно A. Далее установим, что начатую семантическую таблицу можно продолжить до полной. По контрапозиции отсюда следует, что полная семантическая таблица для любой теоремы закроется. Реализация изложенной схемы доказательства требует введения ряда важных вспомогательных понятий: полная таблица, незавершенная таблица...

Определение 9.8.1. Незавершенная семантическая таблица — дерево, каждой вершине которого сопоставлена секвенция, и секвенция в каждой вершине, не являющейся листом, получается из непосредственно следующих за ней по одному из правил вывода исчисления секвенций.

Таким образом, в незавершенной таблице снимаются требования конечности путей и того, что листьями могут быть лишь аксиомы. Содержательно говоря, незавершенная таблица является результатом нескольких разбиений, проделанных над интересующей нас формулой. Незавершенная таблица является одним из простейших примеров важного и для теории, и для приложений семейства понятий — незавершенных выводов.

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

Определение 9.8.2. Шаг разбиения — добавление правила и вершин над листом незавершенной таблицы, не являющимся аксиомой, таким образом, чтобы был получен по правилу из добавленных вершин.

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

Формула A пройдена в секвенции, если она присутствует либо в самой, либо в какой-нибудь секвенции на пути из корня незавершенной семантической таблицы в. Шаг разбиения избыточен, если хотя бы в одной из добавленных секвенций все непосредственные результаты разбиения пройдены в. Секвенция финальна, если она аксиома либо каждый шаг разбиения, применимый к ней, избыточен. Путь незаперт, если он бесконечен либо заканчивается в финальной секвенции, не являющейся аксиомой.

Семантическая таблица полна, если все листья являются финальными секвенциями и для любого незапертого пути в ней выполнены следующие три (для таблиц в теории — четыре) условия:

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

2. Для любой встречающейся в некоторой секвенции пути формулы вида = x A(x) ( |= x A(x)) на встретится формула вида 3. Для любой константы ci, входящей в некоторую формулу на, и для любой встречающейся в некоторой секвенции формулы вида |= xA(x) ( = xA(x)) на встретится формула |= A(ci ) 4. (Для таблиц в теории Th) На встречается |= A для любой A Лемма 9.8.1. (О построении контрпримера) В полной таблице по любому незапертому пути из корня можно построить интерпретацию, в которой истинны все встречающиеся на нем секвенции.

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

Построение контрпримера. В качестве универса контрмодели M возьмем множество всех констант, встречающихся в секвенциях пути В современном теоретическом программировании под верификацией понимается доказательство соответствия конструкции спецификациям, заданным при ее построении;

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

. Каждая константа означает саму себя. (P (c1,..., cn )) есть, если = P (c1,..., cn ) встречается в какой-то секвенции на ;, если встречается |= P (c1,..., cn ). В остальных случаях оно определяется произвольным образом.

Верификация построения. То, что все секвенции пути истинны, означает, что все встречающиеся в них формулы удовлетворяют своим спецификациям. Это утверждение доказывается индукцией по построению формулы.

Прежде всего элементарная формула, встретившаяся в некоторой секвенции i на пути, будет присутствовать и во всех последующих секвенциях, поскольку ни одно правило не может ее разбить. Поэтому на незамкнутом пути не встретится противоречащих друг другу элементарных формул, и модель M определена корректно. Далее, по построению все элементарные формулы удовлетворяют своей спецификации.

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

Шаг индукции. Пусть соответствие спецификации уже доказано для всех формул с числом логических связок меньше n. Пусть A имеет n логических связок. Разберем случаи, соответствующие построению и спецификации A.

Если рассматриваемая формула есть |= (B C), то, по определению полноты, на пути найдется либо |= C, либо = B. По предположению индукции, эти формулы удовлетворяют своим спецификациям.

В каждом из этих случаев истинно (B C). Если она есть = (B C), то по полноте на пути встретятся и |= B, и = C. Поскольку они удовлетворяют своим спецификациям, (B C) ложно.

Если формула имеет вид = x A(x), то по условию полноты таблицы на пути встретится = A(ci ) для какого-то ci, и x A(x) ложно.

Если формула есть |= x A(x), то по полноте на встретится |= A(ci ) для любой константы ci, принадлежащей универсу контрмодели M. По предположению индукции, любая из = A(ci ) удовлетворяет своей спецификации и, значит, истинна. Но тогда по определению истинности истинно и x A(x).

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

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

Для этой цели сформулируем стратегию корректного разбиения формул, приводящую к такой таблице. Стратегия не будет определять однозначно, какая формула должна быть разбита в данный момент. Она лишь ограничивает допустимые разбиения.

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

Занумеруем все константы из сигнатуры теории нечетными натуральными числами. Все вспомогательные константы занумеруем четными. Занумеруем все аксиомы теории. Введем дополнительные спецификации для аксиом теории и многократно используемых (МИ) формул вида |= x A(x) и = x A(x). Аксиома может быть разрешена или задержана. Каждой МИ-формуле сопоставим множество констант, по которым она уже разбивалась; кроме того, она может быть временно запрещена. Формула временно запрещается, когда происходит ее разбиение. Корректное разбиение МИ-формулы может производиться лишь по константе ci, при этом ci добавляется к. Корректное разбиение не может производиться по временно запрещенной или задержанной формуле. Секвенция условно финальна, если в ней не может быть произведено ни одного неизбыточного корректного разбиения.

Стратегия корректного разбиения. Вначале задерживаем все аксиомы, кроме первой, и не запрещаем ни одной МИ-формулы. Пока формула не является условно финальной, производятся лишь корректные разбиения, причем разбиение МИ-формулы производится по константе ci, имеющей минимальный номер среди всех таких констант, встречающихся в незадержанных формулах секвенции. Когда секвенция оказалась условно финальной, разрешаем первую из задержанных аксиом и снимаем все временные запрещения.

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

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

Лемма 9.8.3. (Лемма о корректных разбиениях) Любая последовательность корректных разбиений над секвенцией, содержащей конечное число разрешенных аксиом, за конечное число шагов приводит к условно финальной.

Доказательство. Определим ранг секвенции как количество логических связок в формулах, не являющихся задержанными либо временно запрещенными. В условиях леммы ранг конечен, поскольку число таких формул конечно. При каждом разбиении ранг уменьшается на 1.

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

Докажем теперь, что для каждой МИ-формулы A, встретившейся в секвенции на незамкнутом пути, на этом пути встречаются результаты ее разбиения по каждой константе ci, встречающейся на. Если завершается финальной секвенцией, то любое разбиение A избыточно и, соответственно, любое разбиение по любой константе ci пройдено в финальной секвенции. Если же путь бесконечен, то в промежутке между i-той и (i + 1)-ой условно финальными секвенциями, встретившимися на после появления A и ci, A будет разбито по ci.

Для любой обычной формулы результаты ее разбиения встретятся на до следующей условно финальной секвенции после того, как она появилась либо стала разрешена (если формула является аксиомой).

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

Таким образом, если полная таблица не является выводом в исчислении секвенций, то она дает модель, в которой все аксиомы Th истинны, а проверяемая формула A ложна. Комбинируя доказанное утверждение с теоремой корректности, получаем:

Теорема 9.2. (Теорема полноты классической логики) Th A тогда и только тогда, когда существует вывод секвенции |= Th { = A}.

Таким образом, синтаксическая доказуемость при помощи семантических таблиц совпадает с семантическим отношением логического следования. Теорема полноты (в формулировке, связанной с другой формализацией логики) была первым фундаментальным результатом математической логики, доказанным в 1930 г. великим логиком XX века К. Г делем (K. G del)13. Теорема полноты влечет несколько важных следствий.

Определение 9.8.3. Th синтаксически непротиворечива, если не замыкается семантическая таблица ни для какой формулы вида A&¬A.

На самом деле теорему полноты (в форме теоремы существования модели) предвосхитил, но не сумел понятно сформулировать и доказать Лёвенгейм (L. L wenheim) еще в 1915 г. Его работа осталась незамеченной и была заново открыта лишь после доказаo тельства Гёделя.

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

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

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

Следствие 2. (Теорема компактности) Если Th A, то найдется конечная подтеория Th0 Th, такая, что Th0 A.

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

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

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

Доказательство. Действуем от противного. Если семантическая таблица для |= T h { = A&¬A} замкнута, то найдется конечная Th0 Th, такая, что Th0 противоречива. Значит, если теория противоречива, то противоречива некоторая ее конечная подтеория. По контрапозиции, получаем отсюда искомую форму теоремы компактности.

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

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

Следствие 5. (Теорема о взаимной противоречивости) Если теории Th1 и Th2 непротиворечивы, а теория Th1 Th2 противоречива, то найдется конечное число аксиом Th1 и конечное число аксиом Th2, которые противоречат друг другу.

Следствие 6. (Теорема о взаимной непротиворечивости) Если теории Th1 и Th2 непротиворечивы и любое конечное число аксиом Th2 не противоречит Th1, то теория Th1 Th2 непротиворечива.

Доказательства этих следствий являются экзаменационными дополнительными вопросами на оценки 4–5.

Вы видите, сколько разнообразных форм, внешне совершенно не похожих друг на друга, может быть выведено как непосредственные следствия фундаментальной теоремы. Таким свойством обладают все принципиальные математические результаты. Но отнюдь не всегда их следствия становятся ясны сразу после их открытия. На первый взгляд (скажем) теорема компактности выглядит как тривиальное следствие теоремы полноты. Но потребовалось около двух десятилетий для формулировки теоремы компактности после того, как была полностью осознана формулировка теоремы полноты, да и первые ее доказательства были не такими простыми. Более совершенный аппарат позволяет ярче выделить взаимосвязи. Интересна и ее история. Она была доказана русским логиком А. И. Мальцевым во время II мировой войны и опубликована в Вестнике Ивановского педагогического института. Естественно, что публикация осталась незамеченной, и десятью годами позже она была “переоткрыта” Л. Хенкиным. Правда, историческую справедливость удалось восстановить, но теперь кое-кто утверждает, что она практически содержалась в уже упомянутой работе Лёвенгейма.

Упражнения к § 9. 9.8.1. Доказать, что любая модель теории Th с равенством может быть преобразована в такую, в которой равенство определяется как совпадение.

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

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

9.8.4. Студент Гениалькис доказал, что все счетные модели теории с равенством R, описывающей порядок и его взаимоотношения со сложением и вычитанием на множестве рациональных чисел и имеющей перечисленные ниже аксиомы, изоморфны:

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

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

9.8.5. Известно, что если из предыдущей теории выбросить сложение, то все ее счетные модели действительно будут изоморфны. Как же согласовать это с существованием нестандартных моделей?

9.8.6. Какая аксиома теории R лишняя (следует из остальных)?

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

СЕЧЕНИЯ

§ 9.9.

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

Теорема об устранении сечений. Если семантические таблицы для { = A} и {|= A} закрываются, то закрывается и семантическая таблица для.

Доказательство. Поскольку в любой интерпретации A либо истинно, либо ложно, в соответствующей секвенции противоречит (по теореме корректности) своей спецификации одна из формул. Значит, тождественно истинна и по теореме полноты имеет замкнутую семантическую таблицу.

Правило сечения присутствовало в исходной генценовской формулировке исчисления секвенций, и доказательство устранимости сечений было первым серьезным результатом его работ. Формула A называется формулой сечения либо формулой, по которой производится сечение.

Заметим, что наше доказательство, хотя и краткое, обладает одним существенным недостатком, которого лишено гораздо более длинное доказательство Генцена. Оно полностью неконструктивно, не дает никакого способа преобразования замкнутых таблиц для его посылок в таблицу для заключения, кроме тривиального указания “ищите и обрящете”. Логический статус приведенного доказательства полностью аналогичен логическому статусу следующего доказательства того, что в шахматах, правила которых видоизменены таким образом, что каждая сторона делает два хода подряд, белые проиграть не могут.

В детерминированной конечной игре обязательно имеется либо стратегия, ведущая к выигрышу одной из сторон, либо стратегия, ведущая к ничьей14.

Кажется, что оговорка о конечности здесь перестраховка, но предположение о существовании выигрышной стратегии у одного из игроков для бесконечных игр оказалось новой аксиомой теории множеств, альтернативной аксиоме выбора (т. е. несовместимой с ней, но вроде бы не противоречащей всем остальным аксиомам)!

Рассмотрим три возможных случая. Если стратегия ведет к выигрышу белых либо к ничьей, то все доказано. Пусть она ведет к выигрышу черных. Тогда, воспользовавшись тем, что есть фигура, которая может ходить в начальной позиции (а именно, прыгающий через другие фигуры конь), сделаем ею ход, а затем вернем ее на исходную позицию (например, 1. Kg1–f3, Kf3–g1). Тогда мы передадим ход черным, и по предположению они теперь должны проиграть, что абсурдно. Итак, третий случай исключается.

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

Устранение сечений внешне похоже на разбор случаев A ¬A, но отнюдь не сводится к нему. Оно имеет место и для многих неклассических логик, в которых закон исключенного третьего отсутствует. Оно проваливается в ряде систем, в которых закон исключенного третьего есть.

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

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

Перед тем как их определить, докажем возможность некоторых преобразований выводов в исчислении секвенций, а именно: ослабления секвенций путем дописывания новых членов, подстановки конкретного значения вместо вспомогательной константы в заключении, т. н. обращения всех правил исчисления секвенций15 и сокращения нескольких экземпляров одинаковых формул в заключении вывода. Далее покажем, что эти преобразования не усложняют вывода, но при этом несколько На самом деле мы уже указали на возможность обращения правил, разрешив пользоваться для сокращения семантической таблицы обратными преобразованиями.

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

модифицируем понятие вывода. Аксиомами теперь будут лишь противоречия из элементарных формул. Очевидно, что любое противоречие из пары сложных формул разбивается на элементарные, так что с теоретической точки зрения понятие выводимости не изменяется16.

Предложение 9.9.1. (Подстановка) Вывод секвенции {A(cn+1 )}, где cn+1 не входит в, без увеличения числа применений правил и сложности встречающихся формул перестраивается в вывод {A(x | t)} для произвольного терма t.

Доказательство. Начнем с частного случая подстановки — переименования вспомогательной константы. Докажем, что если cl не входит в формулы из, то вывод [x | cn+1 ] можно преобразовать в вывод [x | cl ]. В самом деле, противоречия после такой замены останутся противоречиями, и мы получаем базис индукции по длине вывода. Далее, все применения правил после такой замены остаются корректными применениями правил, кроме, может быть, двух правил, использующих17 вспомогательную константу, да и то в случае, когда эта константа совпадает с cl. Рассмотрим одно из них, например, Здесь, как и ниже в описаниях преобразований, обозначает вывод стоящей ниже его секвенции. В меньше применений правил, чем в исходном выводе, не содержит cl. Поэтому по предположению индукции l можно переименовать везде внутри, например, заменив ее на k, не входящее в и не совпадающее с cn+1. После чего x можно повсюду заменять на cl.

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

Результат применения преобразования подстановки к выводу обозначаем, аналогично подстановке в формулу, [cn+1 | t]. Проведенное Конечно, с практической точки зрения может быть утомительно разбивать до элементарных компонент уже встретившееся противоречие.

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

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

Предложение 9.9.2. (Ослабление) Вывод секвенции перестраивается без увеличения числа применяемых правил и сложности формул в вывод секвенции.

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

Предложение 9.9.3. Вывод заключения любого из правил исчисления секвенций перестраивается в вывод любой из своих посылок без увеличения числа применяемых правил и сложности формул.

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

Если примененных правил вообще нет, то исходная секвенция — аксиома, а поскольку противоречие состоит из элементарных формул, оно находится в, и результирующая секвенция также является аксиомой.

Пусть теперь обратимость доказана для всех выводов с числом правил не более n. Докажем для выводов с n + 1 правилом.

Проанализируем правила обращения для конъюнкции и всеобщности (остальные правила рассматриваются совершенно аналогично).

Докажем, что вывод {|= A & B} без усложнения перестраивается в вывод {|= A, |= B}. Проанализируем последнее из примененных в выводе правил. Если это правило создало |= A & B, то просто отбрасываем его, если же оно его не затрагивало, то обращаем по предположению индукции выводы-посылки данного правила. Так же поступаем в случае = A & B, но здесь в случае, если последним применялось правило = &, отбрасываем целое поддерево вывода, поскольку нас интересует лишь одна из его посылок.

Рассмотрим перестройку вывода секвенции { = x A(x)} в вывод секвенции { = A(cn+1 )}. Опять-таки если последнее правило создало = x A(x), то отбрасываем его, иначе обращаем вывод посылки. Для истинности рассуждение совершенно аналогично.

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

Предложение 9.9.4. Вывод секвенции {|= A, |= A} без увеличения числа применений правил и сложности встречающихся формул перестраивается в вывод {|= A}. Аналогично для = A.

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

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

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

Если последним применялось правило к сокращаемой формуле, то рассмотрим ее вид. Пусть она имеет вид B & C. Тогда вывод выглядит следующим образом Тогда по обратимости можно перестроить вывод без увеличения длины в вывод, дающий секвенцию А теперь, применив сокращение, получаем из него вывод Длина не больше длины, и опять можно применить предположение индукции, сократив еще раз:

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

Рассмотрим случай B C. Тогда вывод имеет форму Отсюда обращениями получаем Применяем имеющиеся по предположению индукции сокращения и возвращаем на место исходное правило:

Есть еще одно место в исчислении секвенций, где возникают трудности при нормализации. Кванторы = и |= “бессмертны”: они не исчезают и дотягиваются из результата до всех аксиом-противоречий. Как Вы видели, действительно часто их нужно использовать многократно, но не бесконечное же число раз!18 Поэтому желательно было бы коекогда от них избавляться.

Предложение 9.9.5. (Удаление последнего квантора) Если вывод имеет вид и внутри формула = x A(x) более нигде не разбивается, то без увеличения длины вывода и сложности формул можно преобразовать в вывод { = A[x | t]}. Аналогично для |=.

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

Шаг 0. Если главная связка формулы сечения является пропозициональной и она не разбивается хотя бы в одной из его посылок, либо ее Это нужно лишь для опровержения, но не для доказательства.

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

главная связка — квантор и ни в одной из посылок для него не вводится вспомогательная константа, то выполняем одно из следующих преобразований подъема сечения в зависимости от того, какое правило применялось к одной из секвенций-посылок (эта секвенция для формул с пропозициональной связкой может выбираться произвольно, а для кванторных — соответствует посылке вида {|= x A(x)} либо { = x A(x)}).

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

2 получается обращением 2, 5, 5 — два обращения 5.

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

Рассмотрим теперь кванторы.

Для вспомогательной константы:

2, 4 получаются обращениями соответствующих выводов.

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

Шаг 1. Если одна из посылок правила сечения является аксиомой, то рассматриваем следующие два подслучая.

1. Формула сечения не участвует в противоречии. Тогда и в результате правила сечения имеется то же противоречие и, следовательно, результат является аксиомой. Значит, правило сечения вместе с его посылками и всем, что лежит над ними, можно просто опустить.

2. Формула сечения участвует в противоречии. Здесь опять придется разобрать два подслучая, но они совершенно симметричны.

(a) Пусть противоречием является левая посылка. Тогда она имеет вид а правая, соответственно,

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

Заключение сечения имеет вид { = A}. Значит, его можно получить из правой посылки преобразованием сокращения (предложение 9.9.4), не увеличивая длины вывода и сложности формул.

Связка ¬. Для отрицания Связка. Для кванторов Здесь в выводе выделены все применения правила |= к формуле сечения. i — выводы посылок таких правил, в которых имеются другие применения тех же правил, j — выводы, в которых других применений |= к формуле сечения нет. i получается из i устранением последнего применения кванторного правила по предложению 9.9.5, а j — вычеркиванием всех формул |= x A(x).

Связка. Пусть главная логическая связка формулы сечения — импликация и в обоих посылках сечения она разбирается. Тогда имеем следующее преобразование:

Выводы со штрихами — ослабления соответствующих исходных выводов.

Связки &,. Для остальных бинарных пропозициональных связок преобразование определяется аналогично.

Из всех шагов нормализации обоснования требуют лишь кванторные. Достаточно заметить, что после устранения первых применений кванторного правила последующие за ними также становятся первыми, и т. п. Это легко оформляется индукцией.

Теорема 9.3. (Сильная теорема нормализации) Любая последовательность шагов нормализации за конечное число шагов приводит к выводу без сечений.

Доказательство. Для обоснования этого достаточно приписать любому сечению высоту, которая будет уменьшаться на каждом шаге нормализации и оценивается в единицах, множество которых удовлетворяет свойству бесконечного спуска. Натуральными числами оценить не получается из-за того, что слишком часто при нормализации одно сечение заменяется на несколько; приходится оценивать ординалами. А изобретение такой оценки можно рассматривать как задачу на ‘отлично’ для студента (подсказка: удобнее всего воспользоваться сложением по Куратовскому и возведением в степень).

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

9.9.1. (Для тех, кто хорошо знает официальные правила шахмат и играл в турнирах) Приведенное в примечании на стр. 254 доказательство ошибочно. Найдите неточность и исправьте ее19.

9.9.2. В японских шахматах ничьей нет. Тот, кто сделал ход, ведущий к троекратному повторению позиции, считается проигравшим. Королю не запрещено ходить под шах, так что при возникновении ситуации, которая в европейских шахматах считалась бы патом, король обязан пойти под бой и пасть смертью храбрых20. В начальной позиции многие фигуры21 могут походить и затем вернуться назад. Можно ли перенести наше доказательство на модифицированные японские шахматы? А может быть, Вы придумаете 9.9.3. Если не отказываться от неэлементарных противоречий, какой из пунктов доказательства теоремы об устранении сечений проваливается? Как можно было бы спасти его, изменив меру сложности 9.9.4. Студент Гениалькис принес Вам доказательство того, что каждый вывод секвенции { = x A(x)} можно перестроить в вывод секвенции { = A(x | t1 ),..., = A(x | tn )} для некоторых t1,..., tn, не увеличивая число шагов в выводе, но Вы тетрадь с доказательством потеряли. Как Вы ответите на вопрос Гениалькиса, верно ли его доказательство? Ошибка возникает лишь при взаимодействии с полной системой правил шахматной игры в официальных соревнованиях.

На самом деле там такая ситуация может возникнуть лишь теоретически, поскольку взятые фигуры (кроме, естественно, короля) переходят на сторону противника и воюют против бывших своих. Но это уже не имеет отношения к математическому содержанию задачи.

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

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

Глава 10. Элементы нестандартного анализа

ИСТОРИЧЕСКОЕ ВВЕДЕНИЕ

§ 10.1.

История развития математических концепций является одним из примеров творческого развития. В ней выполнены многие общие закономерности такого развития. Стоит напомнить некоторые из них, которые необходимо знать любому, решающему сложные нестандартные практические задачи1 :

1. Ни одно принципиально новое открытие не может быть обосновано его творцами строго. Более того, предложенные ими обоснования, как правило, содержат серьезные ошибки и впоследствии опровергаются.

2. Тот, кто боится делать предположения, противоречащие общепринятому и даже “здравому смыслу”, не может открыть ничего нового2.

Решение т. н. сложных нестандартных математических задач принципиально отличается. Здесь основным интересом является спортивный: решить поставленную авторитетным человеком задачу раньше других и получить славу и награду. Естественно, как и в спорте, имеются судейские коллегии, проверяющие чистоту достижения, т. е.

прежде всего его соответствие принятым правилам и традициям. Реального творчества здесь обычно не так уж много, и чаще всего творческие достижения принадлежат не тем, кто в конце концов решил задачу. Примерами здесь являются 10-я проблема Гильберта и теорема Ферма.

В теории творческого мышления это называется “инертностью”. В психологии это называется “рутинностью мышления”.

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

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

3. Не только логика открытия и обоснования, но и логика нахождения обоснования и его изложения принципиально различаются.

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

Интереснейшим и показательным примером творческого развития в математике является создание математического анализа. Известно, что в нынешнее время анализ излагается в учебниках совсем не так, как излагали его создатели, да и другие ученые вплоть до конца XVIII в. Основными понятиями служат множество, предел, функция, определяемая через множества, последовательность, определяемая через функцию.Что такое множество и зачем оно нужно в математике, осознано было лишь во второй половине XIX века4, поэтому множеств создатели анализа не знали, а вот все остальные понятия были центральными и для них. Но воспринимались они совсем не так, как в современной математике.

Так, например, практически никто не замечал аналогий между понятиями последовательности и функции. Если с последовательностью связывалась в основном идея бесконечно продолжающегося порождения элементов, возможно, путем свободного выбора, то насчет функции практически не было сомнений, что это — либо аналитическое выражение, задающее связь аргумента с результатом, либо непрерывная кривая, которая может быть начерчена, либо какой-то другой тип их явно заданной взаимосвязи. Поэтому и появился термин “неявная функция”, означавший функцию, для вычисления которой требовалось решить уравнение, зависящее от ее аргумента как от параметра.

К такому пониманию функции в некотором смысле вернулись в современной теории вычислимости, но там первичны именно законы, поВ психологии это называется “переходом ценных идей в сверхценные”.

Хотя в традиционной логике давно уже использовалось понятие класса, соответствующее по содержанию понятию множества, и попытки построить исчисление классов начались практически одновременно с созданием математического анализа; в частности, к ним приложили руку Лейбниц, Эйлер, Больцано...

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

Но более всего бросаются в глаза расхождения в определении предела и наличие в математике конца XVII–XVIII в. понятий актуально бесконечно малых величин. Математический анализ даже назывался в то время анализом бесконечно малых. Актуальные бесконечности были полностью отброшены при канонизации и уточнении изложения анализа в первой половине XIX в. Еще в 1960 г. считалось, что они забыты навсегда и представляют интерес лишь для историков науки и издателей трудов классиков того времени. Но радикальное изменение взгляда на математику, порожденное математической логикой, привело к их неожиданному возрождению на абсолютно строгом уровне5.

Важнейшими из, казалось бы, навсегда отвергнутых понятий были понятия бесконечно малых и бесконечно больших величин и понятие дифференциала функции (которое Ньютоном и Лейбницем считалось первичным по отношению к понятию производной). dy было приращением функции y = f (x) при бесконечно малом изменении x. Отношение dx было действительно результатом деления dy на dx. Конечно же, при делении одного бесконечно малого числа на другое могло получиться конечное число, но тонкость в том, что это конечное число могло содержать и бесконечно малую компоненту, которая считалась пренебрежимой по сравнению с конечным результатом и отбрасывалась.

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

Пусть dx = a, dx = b. Пусть u = y z. Тогда при бесконечно малом приращении dx аргумента x имеем:

Отбрасывая пренебрежимо малую величину dy dz, получаем Тем не менее некоторые из понятий анализа бесконечно малых, и очень полезные, до сих пор не нашли новой интерпретации. Да к ним добавились еще другие понятия, созданные гениальным английским математиком-прикладником рубежа XIX–XX веков У. Хевисайдом. Лишь простейшие из них получили интерпретацию в теории обобщенных функций, но, кажется, традиционными аналитическими средствами здесь далеко не продвинешься.

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

На этом выводе многие математики прекращали изложение, поскольку именно дифференциал, а не производная, считался первичным понятием. Но некоторые (как правило, самого высокого класса либо с наиболее тонким чувством математической строгости) делали еще пару шагов.

Последний член получившегося выражения бесконечно мал, поэтому отбросим его и получим Предел также интенсивно рассматривался математиками того времени, но определялся весьма расплывчато: как “первое и последнее” значение выражения, соответственно, при приближении к точке a и при удалении от нее. Интеграл определялся как сумма бесконечно большого числа бесконечно малых величин, примерно как Впрочем, такое выражение считалось бы неприличным, поскольку уж о бесконечно больших натуральных числах математики, ясное дело, стыдились говорить6.

Подобные фокусы, когда бесконечно малые величины то полноправно использовались в преобразованиях, то вдруг отбрасывались, причем иногда не полностью, а частично, а ответ, тем не менее, выходил правильный, использовались некоторыми благонамеренными образованными людьми, в частности, епископом Беркли, для доказательства существования Бога, что, как и всякая благоглупость, лишь компрометировало и ту цель, ради которой это делалось, и те средства, которые при Хотя поскольку аксиома Архимеда, говорящая, что для любых двух x, y > 0 найдется такое n, что уже была осознана в то время, казалось бы, очевидно, что, сказав A, необходимо сказать и B: принять существование бесконечно больших натуральных чисел. Но в жизни (и в науке тоже) нежелательные следствия, сколь бы очевидны они ни были, почему-то очень долго не замечаются.

этом использовались. Естественно, что критически мыслящие математики в конце концов больше не захотели “приносить строгость в жертву успеху”, и в начале XIX в. началось движение за изгнание бесконечно малых и замену их т. н. “ формулировками”, которыми мучают нынешних студентов на I курсе7. Эта реформация часто связывается с именем французского математика Коши, который, как выяснилось в результате анализа его работ, на самом деле использовал старые и новые методы вперемежку, но, правда, не стеснялся передоказывать новыми методами утверждения, ранее доказанные им старыми способами.

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