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

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

Теперь рассмотрим аргументы, показывающие, почему практически невероятно как-либо обойти теорему Гёделя о неполноте и нельзя никаким образом ‘конечнозначно’ проинтерпретировать ее, скажем, так:

Любая формула либо доказуема, либо опровержима, либо неразрешима.

Обобщим теорему Гёделя в форме Россера следующим образом. Возьмем произвольное перечислимое множество чисел X. Тогда имеется формула AX (x), такая, что доказуемо A(n) тогда и только тогда, когда Рассмотрим теперь следующий вопрос. Пусть даны два непересекаn X.

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

Пусть формула A(n, m) такова, что она арифметически разрешима и y A(n, y) n X. Наличие такой формулы следует из аксиомы перечислимости. Аналогично, пусть B(n, m) обладает таким же свойством для Y. Построим теперь по образу Россера формулу Содержательно данная формула означает отсутствие доказательства C(n) при n X и ¬ C(n) при n Y. Рассуждениями, аналогичными теореме Россера, получаем, что в любом непротиворечивом расширении арифметики невыводимо x, y DR(x, n, y) при n X и его отрицание при n Y.

Из усиленной формы конструкции Россера следует, что не существует алгоритмической расширяющейся последовательности теорий Thn, таких, что x, y DR(x, n, y) для каждого n разрешимо хотя бы в своей Thf (n). В самом деле, тогда мы могли бы любую вычислимую функцию доопределить до всюду определенной, чего не может быть.

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

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

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

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

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

Теперь рассмотрим идеи следующей группы результатов. Поскольку сами теории поставляют нам примеры неразрешимых утверждений, они же должны поставлять и способы своего собственного пополнения, так, чтобы эти неразрешимые утверждения были решены. Первый из таких способов пополнения нашел сам Гёдель. Он заметил, что его рассуждения в доказательстве теорем неполноты могут быть проведены в самой теории Th, если к ней добавить формулу, выражающую непротиворечивость этой теории. Следовательно, Теорема 13.7. (Теорема Гёделя о непротиворечивости) Непротиворечивость достаточно сильной теории не может быть доказана внутри нее самой.

Но тогда утверждение о непротиворечивости Th является способом пополнения Th, причем таким, который использует лишь неявно имевшиеся в виду при построении Th предположения (кто же намеренно использует противоречивую теорию в математике?)23.

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

На самом деле ситуация намного тоньше. Если взять другое кодирование утверждения о непротиворечивости, идеей которого является повторять конъюнктивно A и дизъюнктивно ее отрицания столько раз, какова длина рассматриваемого доказательства A, то непротиворечивость арифметики можно доказать в самой арифметике. Другое дело, что это кодирование неявно включает в себя непротиворечивость арифметики. Словом, нигде в окрестностях теоремы Гёделя не надейтесь на простые и однозначные рецепты и истолкования. Поэтому практически все популярные философские комментарии к этой теореме неверны. Все вышеизложенное можно суммировать следующим образом: не верьте никаким философским комментариям к теореме Гёделя, кроме изложенных в книге [14] (но и этим тоже не верьте!).

';

понятно, что простой вычислимой последовательности здесь недостаточно, поскольку результаты Подниекса интуитивно предвосхищались многими крупными логиками с момента осознания теоремы Гёделя. Но почему не продолжать построение по ординалам?

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

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

Это правило имеет бесконечное число посылок — для всех стандартных натуральных чисел. Естественно, если рассматривать другую теорию со стандартной моделью, то посылки правила должны пробегать по всему универсу данной модели. Карнап считал очевидным, что такого правила достаточно для полноты теории, но эта очевидность оказалась столь глубокой теоремой, что была в чуть более слабом виде доказана лишь в 50-х гг., а последние штрихи поставил в начале 70-х гг. А. Г. Драгалин.

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

Итак, формальное правило Карнапа заменяет бесконечное число выводов на доказательство выводимости при произвольном x. Непротиворечивость самой Th легко выводится однократным применением правила

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Карнапа для доказательств внутри Th. Доказано, что добавление формального правила Карнапа позволяет вывести многие формулы, не выводимые из непротиворечивости24. Доказано, что для любой истинной формулы арифметики имеется некоторое кодирование ординалов до, такое, что в трансфинитной последовательности теорий, начинающейся с Th0 = PA и определяемой правилами где n — возрастающая последовательность ординалов, определяющая при данном кодировании предельный ординал, найдется теория, в которой выводима данная формула. Но, конечно же, при любом фиксированном кодировании ординалов можно доходить и до 0, и до более страшных ординалов, применяемых лишь специалистами по теории доказательств, а полноты все равно не будет.

И наконец, рассмотрим вопрос о фрагментах арифметики. Очевидно, что уже они неполны. Но есть еще один любопытный эффект неполноты, связанный с тем, что каждый фрагмент арифметики, где индукция ограничена формулами вида где R — разрешимое отношение, Ki — кванторы, существенно слабее всей арифметики, а именно, непротиворечивость такого фрагмента доказывается в следующем. Поэтому в 50-е гг. была доказана теорема, названная парадоксом изобретателя.

Теорема 13.8. (Ван Хао, 1955) Для каждого n найдется формула вида x R(x) с разрешимым предикатом R, для доказательства которой в арифметике понадобится индукция по формулам с не менее чем n кванторами.

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

Заметим, что принцип рефлексии (13.3) является частным случаем правила Карнапа.

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

Еще одна иллюстрация к необходимости идеальных объектов и сложных формализмов при открытии ‘простых’ теорем.

Упражнения к § 13. 13.5.1. Докажите, что если система n формул A1,..., An такова, что ни одна из конъюнкций где каждое из i есть пустое слово либо знак отрицания, неразрешима, то булева комбинация этих формул выводима ттт, когда она является тавтологией (такую систему назовем независимой, аналогично независимой системе множеств).

13.5.2. Постройте независимую систему формул.

13.5.3. Постройте формулу A(x), такую, что при любом n система A(0),..., A(n) независима.

ФОРМАЛИЗАЦИЯ НЕФОРМАЛИЗУЕМЫХ

ПОНЯТИЙ

§ 13.6.

Итак, даже в математике достаточно сложные понятия невозможно формализовать. Тем не менее мы вовсю пользуемся их формализациями. Более того, компьютеризация всех сфер человеческой деятельности приводит к (слишком часто неосознанной) формализации и тех понятий, которые всегда трактовались как неформальные. Эта сторона была впервые ярко подчеркнута Дж. Вейценбаумом26 в его книге [9]. Ведь Дж. Вейценбаум — один из ярчайших (но отнюдь не самых преуспевших) представителей направления, известного под названием ‘искусственный интеллект’. В середине 60-х годов он создал программу ELIZA (названную по имени героини пьесы Б. Шоу «Пигмалион»), которая имитировала диалог между психоаналитиком и пациентом. Она не пыталась понять человеческий язык (что было в принципе невозможно на том уровне развития компьютеров и информатики), а просто на основе формальных знаний о синтаксисе фраз возвращала человеку его собственные утверждения в виде вопросов

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

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

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

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

Пожалуй, первым открыто заговорил о формализации неформализуемых понятий новосибирский логик Н. В. Белякин. Он воспользовался ситуацией, возникшей вокруг теоремы Гёделя о неполноте, для представления гуманитарных понятий.

либо замечаний. Некоторые из правил переформулировки были весьма остроумны, например, на утверждения типа «Никто меня не любит» мог последовать вопрос: «Кого конкретно Вы имеете в виду?».

Эта программа послужила эффектным экспериментальным опровержением теста Тьюринга (см. примечание на стр. 356): люди воспринимали программу как вполне разумного и доброжелательного собеседника.

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

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

Основная идея Белякина следующая. Гуманитарное понятие (например, любовь, дружба, честь) разъясняется на прецедентах и получает неявное алгоритмическое определение. Но деятели культуры специализируются на том, что каждый раз, когда такое определение становится почти фиксированным и общепринятым (когда возникает формализация), придумывают прецеденты, не подходящие под данное определение28. С алгоритмической точки зрения это можно уточнить следующим образом. В каждый данный момент формализация представляет из себя разрешимое подмножество некоторого идеального образа понятия, не являющегося даже перечислимым множеством. Каждая формализация алгоритмически порождает прецедент, входящий в идеальное множество, но не подходящий под нее саму. Более того, таким свойством обладает и каждая вычислимая последовательность формализаций. Значит, хотя в некотором смысле формализации неформализуемого понятия по Белякину и стремятся к идеальному пределу, но любой реальный предел сам себя помогает опровергнуть (точно так же, как любая непротиворечивая теория сама помогает построить пример неразрешимого в ней истинного утверждения).

Строго определить систему формализаций неформализуемых понятий можно, базируясь на теореме Гёделя о неполноте и результатах теории алгоритмов и теории доказательств. В самом деле, поскольку понятия неформализуемы, они должны иметь не просто расходящиеся, а прямо противоречащие друг другу формализации. Далее, поскольку содержательные понятия тесно взаимосвязаны друг с другом, есть смысл рассматривать их совместную формализацию. И наконец, подмеченный Н. В. Белякиным эффект диагонализации должен, конечно же, иметь место. Таким образом, приходим к следующим принципам, которые естественно принять как постулаты теории неформализуемых понятий.

Принцип 1. Понятия могут описываться лишь в их взаимосвязи. Совокупность взаимосвязанных понятий может быть описана как сигнатура (называемой в гуманитарных исследованиях тезаурус)29.

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

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

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

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

Принцип 2. Объем понятия является производным от его содержания и взаимосвязей с другими понятиями30.

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

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

Принцип 5. Имеется оператор альтернативы, выдающий по каждой паре уточнений (0, 1 ), где 1 расширяет 0, новое уточнение 2, расширяющее 0, но несовместимое с Принцип 6. Имеются абсолютно общепризнанные соотношения между понятиями (трюизмы), но они — самые бесполезные из всех соотношений.

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

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

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

Н. В. Белякин.

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

Если ты — светский человек, не дай чувству ревности проявиться наружу!

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

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

Принцип 7. В каждый данный момент для данной конкретной цели взаимоотношения понятий описываются как классическая теория T h. Эта теория называется ипостасью системы неформализуемых понятий.

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

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

Принцип 8. Среди этих теорий есть теория T h0, являющаяся подтеорией любой T h.

Принцип 9. Имеется вычислимая функция, строящая по каждой паре теорий T h T h, теорию T h(,), расширяющую T h, но несовместимую с T h.

Таким образом, каждое расширение теории имеет альтернативу.

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

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

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

Принцип 10. Пересечением множества теорем всех теорий, расширяющих T h, являются теоремы самой T h.

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

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

Определение 13.6.1. Высказывание A называется псевдопроблемой относительно ипостаси T h, входящей в систему формализаций неформализуемых понятий, если ни в какой ипостаси, являющейся расширением T h, ни A, ни ¬ A не являются теоремами.

Предложение 13.6.1. Метод критики оснований. Если A — псевдопроблема, B не является псевдопроблемой, B неразрешимо в T h и в теории T h доказано A B, то можно подобрать формулу D, не являющуюся псевдопроблемой, такую, что D A и A D — не теоремы T h, а D B — ее теорема.

Доказательство. Пусть для определенности B доказывается в некоторых формализациях. Тогда имеется теория T h, расширяющая T h, в которой доказывается B. Но тогда есть конечный список D1 аксиом T h, из которого выводится B в T h. Значит, D1 B является теоремой T h. Поскольку T h имеет альтернативу T h(,), усилим D до списка аксиом D, опровергаемого в данной альтернативе. Поскольку A — псевдопроблема, то ни она, ни ее отрицание не выводимы ни в T h, ни в T h(,). Отсюда получаем, что четыре импликации невыводимы в T h и, соответственно, D — искомое независимое от A основание.

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

Понятие псевдопроблемы появилось в работах Венской школы позитивизма в 20-х годах. Псевдопроблемами называли пышно звучащие философские вопросы типа Что первично: материя или сознание?

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

С другой стороны, данный результат имеет отношение к давно известному в логике примеру логической ошибки. В жизни слишком часто мы считаем, что отвергли выводы человека, если сумели опровергнуть посылки, на которых он базируется. Например, отвергнув посылку об изначальном равенстве способностей всех людей, мы отвергаем целесообразность равенства их прав. Это еще со времен Аристотеля квалифицировалось как логическая ошибка: единственный способ опровергнуть предложение — временно принять его. Критика оснований может лишь показать, что декларированное утверждение не обосновано. Мы показали, что в реальной ситуации критика оснований может быть еще более сильным аргументом, если мы обнаруживаем в основаниях не ложное утверждение, а псевдопроблему. Допустим, опора на существование Бога в научном исследовании полностью уничтожает силу приводимых аргументов. На любое утверждение нужно опираться в своем месте и по соответствующему поводу. Религии и так нанесли слишком большой ущерб излишне благонамеренные ученые, очень хотевшие научно доказать существование Бога и делавшие при этом легко обнаруживаемые ошибки.

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

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

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

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

Ни одна достаточно богатая теория не может быть полна.

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

Неразрешимые утверждения бывают разных типов, в том числе и такие, которые не зависят не только от теории, но Пополнение теории правилом, позволяющим переходить от доказуемости A(n) при произвольном n к истинности x A(x) весьма сильно расширяет возможности теории.

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

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

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

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

Выражаясь несколько метафорически, классическая логика — логика конкретного знания и веры, а неклассическая — логика построения, изменения знания и сомнения.

ГЛАВА 13. НЕПОЛНОТА И НЕФОРМАЛИЗУЕМОСТЬ

Введение в неклассические Глава 14. Основы -исчисления Язык -конверсий является сейчас одним из важнейших выразительных средств в логике, информатике, математической лингвистике, искусственном интеллекте и когнитивной науке. Начнем с синтаксических аспектов -конверсий и их использования как формального языка.

ОСНОВЫ -ЯЗЫКА

§ 14.1.

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

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

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

Американский логик Черч (A. Church) предложил обозначения, позволяющие трактовать функциональные и смешанные выражения столь же последовательно, как и обычные математические. Квантор функциональности x. t(x), где t(x) — терм, образует выражение, интерпретируемое как функция, аргументом которой является x, а результатом — значение t(x). Это выражение само рассматривается как терм, к которому можно применять преобразования и о свойствах которого можно говорить, x становится связанной переменной, подстановки производятся по тем же правилам, что и обычно, чтобы избежать коллизий. Так что с точки зрения -языка утверждение, что производная ex в точке 0 есть записывается четко и ясно:

Здесь D — оператор дифференцирования, применяемый к функции x. ex (заметим, что традиционное dx становится просто ненужным; аргумент функции однозначно определяет, по какой переменной берется производная). D применяется к функции действительной переменной и в результате дает также функцию действительной переменной. Видно, что результат применения оператора D к функции x. ex применяется далее к числу 0.

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

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

То, что математику можно построить не на базе чисел и множеств, а на базе понятия функции, если разрешить свободно использовать функции как аргументы и результаты1 других функций, заметили практически одновременно великий венгерский математик Я. фон Нейман и российский логик М. И. Шейнфинкель. Фон Нейман стремился в тот момент действовать как можно более традиционно, поэтому он создал теорию, которая выглядит как перевод теории множеств на язык функций, и, как недостаточно безумная, она оказалась забыта. Зато Шейнфинкель выделил минимальный базис колоссальной общности и необычности, который был развит другими. Операции, применяемые к функциям, осознанно использовались в математике и до Шейнфинкеля. Они назывались операторами (если результат — функция) либо функционалами Последнее требование не выполняется в общеупотребительных языках программирования, а в тех академических языках, где выполняется, обычно реализовано так, что приводит к безнадежной неэффективности вычислений.

(если результат — объект). Сейчас они чаще всего называются функционалами (высших типов). В -языке и те, и другие чаще всего называются просто функциями. Но лишь М. И. Шейнфинкель и Х. Б. Карри (H. B. Curry) начали разработку их систематической теории. И сразу же они натолкнулись на важное преобразование, позволяющее уменьшить количество сущностей.

Для описания функций многих переменных хочется ввести многоместный квантор типа x1... xn. t(x1,..., xn ). Карри2 подметил исключительно важное преобразование, базирующееся на том, что у нас функции систематически трактуются как значения. Вместо f (x, y) он рассмотрел функционал f, перерабатывающий x в функцию от y:

f (x)(y) = f (x, y). Таким образом, без ограничения общности достаточно рассматривать функции от одного аргумента. Такое преобразование называется преобразованием Карри (Currying). Оно соответствует также представлению x1... xn в форме x1... xn. (Проверьте!) Преобразование Карри имеет важные аналогии в программировании. Оно соответствует частичной параметризации процедур. Если имеется процедура P(x1, x2,..., xn), а известно лишь значение x1 = a, можно тем не менее проделать внутри P вычисления, зависящие лишь от x1, и получить частичную процедуру P1(x2,..., xn) = P(a, x2,..., xn).

Если не требовать оптимизации частичной процедуры, то частичная параметризация становится удобным, легко реализуемым и не портящим эффективность программ методом программирования, который, к несчастью, был осознан вскоре после того, как было фиксировано определение наиболее популярных языков программирования — C и Pascal. У себя в примерах будем обозначать частичную параметризацию P (a,..., z).

Отметим один тонкий момент. Пусть дана процедура P(x, y). Произведя частичную параметризацию P (a, b), мы с точки зрения программирования получаем не значение P(a, b), а процедуру без параметров, вычисляющую это значение.

Упражнения к § 14. 14.1.1. Пусть f (x, y) — функция, вычисляющая расстояние между двумя действительными числами. Что такое x. f (0, x)?

14.1.2. Запишите определенный интеграл f (x) dx на -языке.

На самом деле это преобразование рассматривалось еще Шейнфинкелем и фон Нейманом.

14.1.3. Если f (x, y) = ex sin(y), то что такое xy. f (y, /2 x)?

14.1.4. Вычислить x. Dy (y 3 x + y)(1)(3).

14.1.5. Студентка Тупицына спросила: « А зачем вообще все многочисленные кванторы? Почему не писать, например, x A(x) вместо x A(x), где понимается как логическая операция над функциями с логическими значениями, и обходиться одним квантором ?»

Ваше отношение к этому предложению: приносит ли оно какие-то удобства либо неудобства, либо совсем некорректно, и почему?

14.1.6. Студентка Примерная записала утверждение 14.1.7. Прокомментируйте запись x Max(a, b, f (x)) f (x), где Max — функционал нахождения максимума функции на отрезке [a, b].

14.1.8. Студент Чудаков предложил по аналогии с распространенным в математике обозначением множеств в стиле {f (x, y) | A(x, y)} использовать -обозначения типа (x2 + y 2 ). {sin(x) cos(y)}. Что можно сказать по данному поводу?

§ 14.2.

Пожалуй, впервые общие свойства и преобразования пространств некоторых частных видов операторов и функционалов начали исследоваться в линейной алгебре. Матрицы были введены как представления пространства линейных преобразований; еще более фундаментальное наблюдение было сделано при рассмотрении пространств линейных функционалов из конечномерного пространства в скаляры. Это пространство оказалось имеющим столько же измерений, и векторы исходного пространства могут рассматриваться как линейные функционалы на этом сопряженном пространстве. В выражении f x = c возникает двойственность между функциями и аргументами, которая является краеугольным камнем при развитии -языка: можно считать функцией f, а x — ее аргументом, можно и наоборот3.

Двойственность не означает возможность путать аргументы и функции. Она означает лишь право сделать глобальную замену функций и аргументов друг на друга. А уж Шейнфинкель предложил подчеркнуть двойственность следующей системой обозначений. Операция применения функции к аргументу записывается (f x), а не f (x), как обычно. Здесь важно то, что при помощи преобразования Карри все функции могут быть сделаны одноместными функционалами. Черч предложил важное упрощение языка Карри, которое сейчас и принято называть языком -исчисления.

Определение 14.2.1. -сигнатура — множество констант. -термы сигнатуры задаются следующим индуктивным определением:

1. Константа сигнатуры есть -терм.

2. Переменная есть -терм.

3. Если t и u — -термы, то (tu) — -терм.

4. Если x — переменная, t — -терм, то x. t — -терм.

Пример 14.2.1. Если D, f и 0 — константы, изображающие оператор дифференцирования, функцию одной переменной и ноль, то значение dx (0) изображается ((Df )0).

Так же, как в логике предикатов, для -термов определяются понятия свободной и связанной переменной и подстановки. Через подстановку определяется важнейшее из преобразований над -термами — конверсия. Оно состоит в символьном вычислении результата вызова функции x. t(x). Одинарная стрелка читается “за один шаг переходит в”. Большая стрелка читается “преобразуется в”.

Это преобразование называется -конверсией.

Пример 14.2.2. x. x есть тождественная функция. В самом деле, для любого t. Обозначив терм x. x через I, можем записать это как (I t) t. В частности, (I I) I.

насколько она будет странно выглядеть, другое дело.

-термы позволяют определить предельно общее4 исчисление символьных вычислений функциональных выражений. Оно называется исчислением -конверсий. В этом исчислении выводятся выражения вида r t. Аксиомы его — (14.4), переписанная через :

Правила вывода следующие.

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

Пример 14.2.3. Рассмотрим -термы По -конверсии преобразуется в Итак, конвертируется сам в себя.

Отметим взаимосвязь с парадоксом Расселла. Рассмотрим множество всех множеств, являющихся собственными элементами: Z = {x|x Общее не значит, что туда запихали все, что можно и нельзя. Это означает предельно простое выражение широко применимой идеи, которое может быть легко конкретизировано для частных случаев.

x}. Тогда Z Z Z {x|x x} Z Z. Хотя здесь мы и не получили грубого противоречия, мы высветили логическую основу парадокса Расселла, парадокса лжеца и многих других парадоксов: ударяясь в абстракции, слишком легко определить понятия, не содержащие ничего, кроме самих себя5. Карри дал интересную переформулировку таких “рефлексивных парадоксов”. Пусть A = {x|x x A}. Тогда A A следует A. Но (A A A) A A. Следовательно, A A.

Но A A A. Значит, A. Итак, имея неограниченные абстракции и пользуясь ими в рассуждениях, можно доказать все, что угодно. В конверсиях объекты, подобные, относительно безобидны (в точности в той же степени, что “зацикливание” в программах).

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

-конверсия является определением вызова процедуры, принятым в большинстве языков программирования. Транзитивность означает возможность выполнить целую последовательность вычислений. Единственное разумное ограничение на нее — исчерпание ресурсов, которое обычно игнорируется в семантике алгоритмического языка. Практически нечего возразить и на правило преобразования аргумента. А вот преобразование функции уже несколько более сомнительно. Оно чаще всего просто избегается в языках программирования за счет того, что функция не является полноправным значением. Правило не может быть просто проигнорировано, поскольку любой приличный язык включает описания процедур, но такое преобразование чаще всего прямо запрещается в семантике языков программирования. В самом деле, чаще всего процедура содержит операторы, рассчитанные на разные значения аргумента, и при конкретном значении аргумента выполняются (за счет операторов типа if, case, while, repeat) лишь некоторые из них. Попытка же вычислять, не разобравшись со значением аргумента, вполне может привести к ошибке. Например, если процедура для положительного x вычисляет его квадратный корень, а для отрицательного действует подругому, то попытка слишком рано вычислить x приведет к ошибке.

Таким образом, анализ правила привел нас к выявлению ограничений на частичные вычисления в обычных языках программирования. Даже Некоторые философы и богословы определяли Бога как “то, что является причиной самого себя”. Анализ парадоксов показывает, что это довольно плоско: причина самой себя скорее ничто, чем Бог.

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

Определение 14.2.2. -терм с дырой. Пусть символ обозначает дыру.

2. Если t — -терм, r — -терм с дырой, то (t r) и (r t) — -термы 3. Если x — переменная, r — -терм с дырой, то x. r — -терм с Через t[r] обозначим результат замены дыры в -терме t с дырой на терм r.

Предложение 14.2.1. 1. В -терме с дырой ровно одна дыра.

2. Если t — -терм с дырой, r — -терм, то t[r] — -терм.

3. Если r — подтерм -терма s, то найдется терм с дырой t, такой, 4. Если t — -терм с дырой, r и s — -термы, r s, то t[r] t[s].

Доказательство. Пункты 1 и 2 тривиально доказываются индукцией по построению терма с дырой. Пункт 3 опирается на единственность дерева построения -терма и усиливает ее до следующей леммы.

Лемма о подтермах. Если r — вхождение подтерма в -терм t, то дерево порождения r является поддеревом дерева t.

И, наконец, пункт 4. Действуем индукцией по длине терма с дырой, используя пункт 1. Если терм состоит из одной дыры, то все очевидно.

В противном случае дыра находится в одном из его подтермов, который сам, согласно 3, является -термом с дырой. Рассмотрим три возможных случая. Если t имеет вид x t1, то, по предположению индукции, t1 [r] t1 [s]. Но тогда по правилу t[r] t[s].

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

означает графическое равенство выражений.

Рассмотрим некоторые конструкции -языка. Пусть f и g — функции. Тогда (f (gx)) применяет f к результату вычисления g на x, и терм x. (f (gx)) выражает функцию, являющуюся композицией f и g. С другой стороны, ((f x)y), если принять во внимание преобразование Карри, выражает применение функции f к двум аргументам, а, соответственно, ((f g)y) — применение функционала f к функциональному аргументу g и обычному x7.

Исходя из содержательного смысла конверсий как символьных вычислений, можно определить равенство -термов t и r как существование такого s, что t s, r s. Но обосновать такое определение не слишком просто: ведь прежде всего отношение равенства должно быть отношением эквивалентности; рефлексивность и симметричность нашего определения очевидны, но с транзитивностью дело обстоит не так просто. Если t1 s1, t2 s1, t2 s2, t3 s2, то откуда следует, что найдется такое s, что t1 s, t3 s? Тем не менее временно примем такое сомнительное определение, которое обосновывается теоремой Черча-Россера, доказываемой в следующей главе.

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

Предложение 14.2.2. (Лемма о неподвижной точке) Для любого терма F найдется такой -терм X, что X = (F X).

Доказательство. Определим W как x. (F (xx)), и пусть X есть (W W ).

Тогда легко показать самим, что X конвертируется в (F X)8.

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

В самом деле, поскольку создатели -языка с самого начала отдавали себе отчет в его универсальности (он годится для выражения любого функционала, встречающегося в математике, естественно, при подхоНа самом деле нигде не сказано, что g — функция, а x — предмет. Занимаясь исчислением, необходимо помнить, что функция может быть подставлена в любом месте.

Здесь есть единственная, но ехидная тонкость: не (F X) преобразуется в X, а X в него!

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

Рассмотрим функцию натуральных чисел = n n + 1. Она не имеет неподвижной точки, посколь- (14.10) Здесь на помощь приходит то, что в -исчислении имеется, в частности, терм, конвертирующийся сам в себя и не имеющий значения. ( ) просто не имеет значения, так же как и само, и как + 1. И, соответственно, нет ничего удивительного в том, что ( ) = = + 1.

Поскольку приведенное нами преобразование, очевидно, само выражается в -языке, то имеется комбинатор неподвижной точки Y, который можно определить, например, как Y не является ни единственным, ни даже наилучшим из комбинаторов неподвижной точки, но используется он чаще всего. В частности, не имеет места (почему?).

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

Упражнения к § 14. 14.2.1. Покажите, что (F ) (F (F )).

14.2.2. (Klop) Пусть

$ = (ЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪЪ)

Показать, что $ — комбинатор неподвижной точки.

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

14.2.4. Построить комбинатор A, такой, что (Af x) = (f x).

ТЕОРЕМА ЧЕРЧА-РОССЕРА

§ 14.3.

Важнейшим из известных приятных свойств систем преобразований является свойство конфлюэнтности, либо свойство квадрата: если a преобразуется как в b, так и в c, то имеется такое d, что b преобразуется в d и c преобразуется в d. Это означает, что, какими путями ни вести преобразование, придем к одному и тому же результату. Докажем это свойство для -конверсий.

Теорема Черча-Россера. Если t r, t s, то найдется такое q, что Доказательство. Пользуясь идеей Мартин-Лефа, определим вспомогательное отношение конверсии, в котором -конверсия к каждому подтерму применяется не более одного раза.

Лемма 14.3.1. Если t r, то t r.

Лемма 14.3.2. является транзитивным замыканием.

Лемма 14.3.3. Если x t r, то r также начинается с x.

Лемма 14.3.4. Если (t r) s, то либо s есть (qv), где t q, r v, либо t есть x. q, s есть q1[s|r1], где q q1, r r1.

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

Лемма 14.3.5. Если t r, s q, то t[x|s] r[x|q].

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

Лемма 14.3.6. Отношение обладает свойством конфлюэнтности.

Доказательство леммы. Индукцией по длине преобразования t в r.

Если t есть само r, то достаточно взять s в качестве q.

Если t есть x. (t1 t2 ), a r есть r1 [x|r2 ], где t1 r1, t2 r2, то s есть одно из двух.

1. x (s1 s2 ), где t1 s1, t2 s2. Тогда, по предположению индукции, для r1, s1 можно найти q1 и, соответственно, для r2, s2 общее q2. По лемме 14.3.5 в качестве q можно взять q1 [x|q2 ].

2. s1 [x|s2 ]. Непосредственно применяем предположение индукции и Если теперь t есть (t1 t2 ), а r есть (r1 r2 ), то опять возникают два подслучая.

1. (s1 s2 ). Непосредственно применяем предположение индукции.

2. t есть x. (t11 t2 ), s есть s1 [x|s2 ], где t11 s1, t2 s2. Тогда по предположению индукции, t11 и r1, t2 и r2 попарно приводятся к общему терму. Применяем лемму 14.3.5.

А теперь, поскольку конверсия — транзитивное замыкание, а конфлюэнтно, теорема доказана.

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

Упражнения к § 14. 14.3.1. Студент Талантов предложил следующее расширение -конверсий. Ввести термы вида [x y z] со следующими правилами конверсии: [f aa] (f a)(f a); [f ga] (f a)(ga). Прокомментируйте это предложение.

14.3.2. Студентка Невинная предложила следующий вариант -конверсий для кортежей. Вводятся термы вида [t1... tn ] вместе со следующими правилами конверсии:

Ваше мнение об этом предложении: разумно ли оно с точки зрения истолкования и сохраняет ли оно свойство локальности конверсий и свойство конфлюэнтности?

§ 14.4.

Исчислению -конверсий соответствует исчисление равенств термов, конвертируемых в одно и то же выражение, которое обычно называется -исчислением либо комбинаторной логикой. Языком этого исчисления служат равенства -термов t = u. Аксиомы и правила вывода — следующие семь.

x. (t r) = Subst(t, x, r) (аксиома -конверсии) Теорема 14.1. Формула t = u выводима в комбинаторной логике тогда и только тогда, когда существует такой терм v,что t v, u v.

Доказательство. Индукцией по построению вывода. Аксиома равенства порождает диаграмму Во второй аксиоме левая часть равенства просто конвертируется в правую. Транзитивность равенства соответствует диаграмме Остальные случаи разбираются еще легче.

Следствие 14.4.1. Отношение выводимости t = u является отношением эквивалентности на множестве термов. Если t = u, то термы (ts) и (rs) одновременно либо имеют нормальную форму, либо не имеют ее, и в случае нормализуемости их значения равны.

Обратное свойство — если ts = rs при всех s, то t = r, — не всегда выполнено. Чтобы обеспечить его, достаточно добавить еще одну аксиому равенства x (f x) = f, но тогда разрушается теорема 14.1.

логик

КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

В ТРАДИЦИОННОЙ ЛОГИКЕ

§ 15.1.

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

Первые три из данных законов восходят к Аристотелю. Правда, Аристотель никогда их явно не выделял, но повторил их в своих работах [1], [2], [3], [4], [5] столько раз и в столь разнообразных вариантах, что было очевидно их первостепенное значение.

15.1.1. Закон тождества Как и другие законы, он был упомянут им во множестве вариантов, самый выразительный из которых, пожалуй [4, кн. 4, гл. 4]:

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

Его содержательная формулировка Один и тот же термин в одном и том же рассуждении должен употребляться в одном и том же отношении, в одном и том

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

же смысле и применительно к одному и тому же месту и Более краткая формулировка данного закона следующая:

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

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

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

Схоласты упростили формулировку закона тождества до лапидарной:

Закон 15.1 (Тождества). A есть A.

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

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

15.1. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК В ТРАДИЦИОННОЙ ЛОГИКЕ Пример 15.1.1. Рассмотрим случай, когда с целью повышения качества некоторых товаров, ставших вредными для потребителей, вносится предложение о создании службы их сертификации и проверки качества. Тогда вполне естественно задать вопрос человеку, вносящему данное предложение: что будет проверять эта служба на самом деле? Будет ли она проверять качество товаров или же пункты ею самою разработанной инструкции и зачастую с целью содрать с продавца либо взятку, либо штраф?

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

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

Например, в софизме подменяется собирательный и разделительный смысл слова ‘взвод’.

Это — ошибка “От смысла собирательного к смыслу разделительному”.

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

15.1.2. Закон непротиворечия Закон Непротиворечия считается вторым из основных законов Логики, сформулированных Аристотелем. Оригинальная аристотелевская формулировка данного утверждения следующая [4, кн. 4, гл. 3]:

Закон 15.2 (Непротиворечия). Невозможно, чтобы одно и то же в одно и то же время было и не было присуще одному и тому же в одном и том

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

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

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

Пара высказываний A и ¬ A называется прямым противоречием.

Закону Непротиворечия соответствует метод рассуждений, известный в традиционной логике как приведение к абсурду (reductio ad absurdum). Чтобы доказать ¬ A, т. е. чтобы опровергнуть A, наоборот, временно принимается A, и данное предположение приводится к абсурду, т. е.

из него выводится противоречие. Ему соответствует косвенное правило естественного вывода Обычно в современной логике Закон Непротиворечия формулируется в виде математического утверждения ¬(A & ¬ A). Но у него имеется другая математическая формулировка, которая более адекватно выражает его смысл. Это — требование непротиворечивости теории:

A и ¬ A не могут быть одновременно теоремами данной теории.

Выражением математического Закона Непротиворечия в логике можно считать правило, установленное средневековыми схоластами и имеющее в традиционной логике название: “Из лжи следует все что угодно” (“ex falso quodlibet”):

Закон Непротиворечия с самого начала осознавался как ограничеB ние, аналогичное Закону Тождества. Естественно, каждый из нас, кто жив сейчас, через некоторое время будет мертв, а некоторое время назад он еще не жил. Поэтому в законе непротиворечия оба члена противоречия должны рассматриваться в одном и том же контексте и в одно и то же время, и все прочее, как и подчеркивал Аристотель. Очевидно, что одни и те же предметы в одно и то же время не могут обладать отрицающими друг друга свойствами. Например, никто не может быть в 15.1. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК В ТРАДИЦИОННОЙ ЛОГИКЕ одно и то же время выше 2 метров и не выше 2 метров, женат и холост.

Тем не менее в жизни мы часто встречаем нарушение данного закона. В частности, женщина вполне может утверждать:

Все мужчины — подонки, а мой муж — хороший человек.

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

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

Закон Непротиворечия принципиально отвергался в логике джайнов и буддистов, поскольку они отрицали наличие объективных понятий в нашем мире, и поэтому утверждение “A есть и B, и не-B” рассматривалось ими как вполне допустимое.

В современной логике Закон Непротиворечия отвергается, в частности, для формализаций понятий, заложенных в базу знаний, поскольку любое знание специалиста в достаточно сложной предметной области оказывается противоречивым по форме. Поэтому в настоящее время интенсивно развиваются паранепротиворечивые логики, в которых, во всяком случае, отвергается принцип ex falso quodlibet. Основоположником европейской паранепротиворечивой логики можно считать Н. А. Васильева. Интенсивно развиваться стала она после трудов Ньютона Да Косты.

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

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

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

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

Закон 15.4 (Исключенного третьего). Оба утверждения A и ¬ A не могут опровергаться одновременно2.

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

Эта формулировка в последнее время подменяется еще более узкой, сразу привязанной к одной из формализаций логики:

Именно формулировка (15.7) чаще всего понимается под законом исключенного третьего в современной математической логике. И именно она чаще всего подвергается пересмотру в неклассических логиках.

15.1.4. Закон достаточного основания Последний закон был, насколько известно, сформулирован Г. Лейбницем намного позже (на 2 тысячелетия, согласно традиционной хронологии, и уж ни в коем случае не менее чем на 500 лет) остальных.

Закон 15.5 (Достаточного основания). Никакое высказывание A не может утверждаться без достаточного основания.

Этот закон часто называют по-латыни: tertium non datur.

15.1. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК В ТРАДИЦИОННОЙ ЛОГИКЕ Только благодаря этому закону стало возможным развитие математической логики. Его часто используемая жесткая формулировка:

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

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

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

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

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

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

Алгебраические законы логики — соотношения между формулами, характеристические для алгебры логики. Обычно в их число включают следующие:

Вышеперечисленные тождества гарантируют существование естественного частичного порядка на множестве логических значений и то, что операции конъюнкции и дизъюнкции дают пересечение и объединение значений. Таким образом, в этом случае логические значения образуют решетку. Данные алгебраические тождества выполняются почти во всех логиках, за исключением линейных конструктивных логик, введенных Ж.-И. Жираром. В них A & A сильнее A, поскольку требует за наши ресурсы3 построить две реализации A.

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

Рассмотрим тождества формулировки отрицаний (4.41–4.48). Они выведены для классической логики, но область их применения намного шире. Правила формулировки отрицаний столь привлекательны, что дают стимул для изменения логики не в сторону их нарушения, а в сторону их восстановления, если они почему-то оказались нарушенными. Более В естественной интерпретации линейной логики — за наши деньги.

15.1. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК В ТРАДИЦИОННОЙ ЛОГИКЕ того, они могут использоваться для введения отрицания в те логики, в которых его не было сначала.

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

Упражнения к § 15. Разобрать следующие рассуждения. Корректны ли они? Если некорректны и опираются на некоторые законы логики, то за границы применимости каких законов они выходят?

15.1.1. Тот, кто ест меньше, более голоден. Тот, кто более голоден, ест больше. Значит, тот, кто ест меньше, ест больше.

15.1.2. Тому, кто хочет учиться, поощрение не нужно. Тому, кто не хочет учиться, оно бесполезно. Значит, поощрять учащихся бесполезно.

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

15.1.4. Тот, кто хочет что-то изучить, не знает этого. Незнающий невежествен. Таким образом, лишь невежественные люди желают 15.1.5. То, что ты не потерял, у тебя есть. Ты не терял рогов. Значит, у 15.1.6. Все коммунисты — атеисты, материалисты и сторонники государственного контроля за обществом. Иван Масонов — атеист, материалист и государственник. Значит, он — коммунист.

15.1.7. В утверждении 15.4, как утверждают многие, на самом деле нет внутреннего противоречия. Объясните, почему? (Как понимают ‘все’ в обыденной жизни?)

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

СИЛА И НЕДОСТАТКИ КЛАССИЧЕСКОЙ ЛОГИКИ

§ 15.2.

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

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

Положение 1. Классическая логика основывается на предположении, что значение сложного предложения зависит лишь от значений его компонент, а не от их смысла. Формально такое предположение выражается как правило замены эквивалентных:

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

Положение 3. Классическая логика является истинностнозначной, т. е. может быть описана через фиксированную алгебру логических значений {0, 1}.

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

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

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

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

Положение 8. Классическая логика может подвести нас тогда, когда мы стремимся использовать доказанные утверждения вида x A(x) как основу для алгоритмических построений.

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

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

Положение 11. Выражаясь несколько метафорически, классическая логика — логика конкретного знания и веры, а неклассическая — логика построения, изменения знания и сомнения.

ИСПОЛЬЗОВАНИЕ ДОКАЗАТЕЛЬСТВ

§ 15.3.

Центральным понятием, введенным математикой, явилось доказательство. Само его появление коренным образом видоизменило стиль мышления значительной части людей и положило начало тому, что сейчас называют рациональным научным мышлением. Не зря на дверях платоновской Академии, по слухам, была надпись: «Не знающим геометрии вход запрещен»4.

Как определил Аристотель:

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

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

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

Даже расширение класса слов выражениями формализованного языка не всегда достаточно, см., например, диаграммы Венна в § 5.2.

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

Другое содержательное определение доказательства было дано нами в первой части книги:

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

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

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

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

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

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

Ответ, на который скатываются даже многие математики, удрученные выявившейся относительностью математических знаний: математическое доказательство устанавливает лишь то, что утверждение выведено по общепринятым и закрепленным традицией правилам игры из утверждений, ранее признанных в соответствии с этими правилами доказанными. Но тогда остается необъяснимой ‘порою фантастическая эффективность математики в других науках’6. На самом деле здесь деЭта характеристика принадлежит Н. Бурбаки.

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

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

15.3.1. Сведение новой задачи к уже решенным Чистые математики занимаются тем, что решают задачи. Откуда берутся задачи, уже немного рассматривалось в первой части (§ 23). А вот что значит решить задачу — важный вопрос.

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

Рассмотрим пример.

Пример 15.3.2. Одна из простейших геометрических теорем — утверждение о возможности деления отрезка пополам. Разберем доказательство этого утверждения. Вначале из каждой из вершин отрезка радиусом равным, скажем, длине этого отрезка проводится окружность. Находятся две точки пересечения этих двух окружностей. Через эти две точки проводится прямая, пересечение которой с исходным отрезком дает его середину.

Тут мы свели данную задачу к следующим, предполагающимся уже решенными:

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

Найти две точки пересечения двух пересекающихся окружностей;

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

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

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

Далее, по двум полученным точкам пересечения можно провести прямую (опять постулат Евклида, опять исходное построение). Эта прямая пересекается с исходным отрезком, и мы опять-таки ссылаемся на результат, что высота, медиана и биссектриса равнобедренного треугольника совпадают, тем самым обосновав корректность проведенного построения.

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

Математику задали вопрос:

— Как приготовить чай?

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

— А если у нас уже есть чайник с кипятком?

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

Именно так и действует хороший математик, решая задачу.

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

Пример 15.3.3. Допустим, мы знаем, что некоторая характеристика x f (x) физического процесса непрерывно изменяется на отрезке [0, 1] Евклид строго различал аксиомы (истинные утверждения) и постулаты (исходные построения, исходные задачи, предполагающиеся решенными).

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

Обозначим текущий отрезок X (т. е. вначале X = [0, 1]). На его концах функция f принимает значения разных знаков. Выделенное утверждение сделаем инвариантом построения. Выпишем его явно:

Функция f непрерывна на отрезке X и принимает на его концах значения разных знаков.

Разделим X пополам. В его середине a могут оказаться три возможности.

1. f (a) = 0. Тогда мы точно нашли корень.

2. f (a) имеет тот же знак, что и f (X.low), где X.low — нижняя граница отрезка X. Тогда возьмем в качестве нового значения X отрезок [a, X.up], где X.up — верхняя граница отрезка X.

3. f (a) имеет тот же знак, что и f (X.up). Тогда в качестве нового значения X берем [X.low, a].

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

Казалось бы (как и утверждается в большинстве учебников по программированию), мы получили построение корня с любой наперед заданной точностью. Но рассмотрим чуть подробнее имеющийся у нас разбор случаев. Любая самая маленькая ошибка в вычислении f (a) может повлечь за собой выбор неправильной половины интервала и большие ошибки в вычислении корня. Итак, на самом деле корень мы не вычисляем. А что же нам гарантирует данное доказательство? Не так уж мало. Если мы достаточно потрудимся, мы с гарантией найдем такую точку x0, что f (x0 ) 0 в пределах точности вычислений f. Итак, мы находим не корень, а точку, где значение достаточно мало.

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

Последний шаг самый важный! Повторяем еще раз, что на практике почти ни одна

ГЛАВА 15. КОРНИ НЕКЛАССИЧЕСКИХ ЛОГИК

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

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

Предложение 15.3.1. Если функция f непрерывна и меняет знаки на концах отрезка [a, b], где a < b, то для любого > 0 имеется отрезок [a1, b1 ] [a, b] длины не больше, в котором есть корень f.

А теперь запишем то, что у нас получилось в результате доказательства, в виде паскалеподобной процедуры:

function DivHalfe(f:function(x:real):real, var a1,b1,c: real; begin a1:=a; b1:=b;

DivHalfe:=lim a1 from end;

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

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

В рассмотренном примере ярко проявилась особенность математических построений: полное пренебрежение реально требуемыми ресурсами, работа с бесконечными процессами и сведение новых построений к предыдущим (в данном случае — к пределу последовательности).

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

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

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

СОЗДАНИЕ ИНТУИЦИОНИСТСКОЙ ЛОГИКИ

§ 16.1.

16.1.1. Брауэр: идея конструктивности К началу XX века математика столкнулась с кризисом оснований, проявлявшимся как в грубых парадоксах типа противоречий (например, парадокс Рассела в ч. 1, § 1.7), так и в том, что понятия, изначально считавшиеся тождественными, стали заметно расходиться.

Вернемся к парадоксу института математики из § 244 и напомним его логическую суть.

Предложение 16.1.1. Если классическая теория Th неполна и имеются обозначения для всех элементов универса (эти термы будем называть конкретными), и мощность универса не меньше 2, то имеется такая Но вспомните семантику булевых алгебр из первой части.

формула A(x), что доказано x A(x), но ни при каком конкретном u не может быть доказано A(u).

Доказательство. Пусть G — неразрешимая в Th замкнутая формула.

Пусть 0 и 1 — два различных элемента универса, которые имеются по определению. В качестве A(x) возьмем x A(x) доказывается разбором случаев G и ¬ G. Но если бы при какомто u было доказано A(u), то заодно была бы разрешена и проблема G, которая неразрешима по предположению.

Мы видим, что парадокс института математики зависит лишь от теоремы Гёделя о неполноте и от логического принципа A ¬ A.

В начале XX века теорема Гёделя о неполноте могла лишь присниться в страшном сне, но математики уже заметили, что понятия ‘существовать’ и ‘быть построенным’ стали заметно различаться. Появилось понятие чистых теорем существования, в которых нет построения объекта, чье существование доказывается2. Козел отпущения, на которого можно было свалить ответственность за чистые теоремы существования, нашелся сравнительно быстро: аксиома выбора3 (§ 32).

Но молодой голландский ученый Л. Э. Я. Брауэр уже в 1908 г. опубликовал на голландском языке статью под вызывающим названием:

“О недостоверности логических принципов”.

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

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

Упомянутая выше его диссертация также была прежде всего философским трудом.

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

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

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

вокупностями устойчивых во времени объектов. Затем они были незаконно перенесены на оперирование с бесконечно большими совокупностями и стали, соответственно, неадекватны. Эта неадекватность не осознавалась длительное время и в конце концов завела математику в громадный тупик, из которого не выберешься пересмотром отдельных аксиом. Нужно либо полностью отказаться от бесконечных совокупностей объектов, либо перейти к другой логике, либо перестать придавать какой-то содержательный смысл математическим утверждениям, признав их чисто абстрактными, идеальными. Далее, математика полностью игнорирует незавершенность человеческого знания и незавершенность, как говорил Брауэр — становящийся характер многих математических объектов. В частности, действительное число рассматривается как уже существующая бесконечная десятичная дробь, а не как процесс получения все более и более точных приближений.

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

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

Брауэр прекрасно понимал, что математическое построение — сущность весьма высокого уровня и для его обоснования недостаточно ссылки на практику, тем более что в те времена точного понятия алгоритма, которое математически мыслящему человеку соблазнительно взять в качестве формализации расплывчатого понятия вычисления, еще не суЗдесь не зря мы добавили прилагательное к задаче. Как говорилось в § 15.3.1, математическая задача отнюдь не обязательно включает построение, вспомните, что значит ее решить?

ществовало. Поэтому оставалось ссылаться в качестве первоисточника математики на Идеи, но уже не считая математику прямым воплощением Идей. Поскольку понятий для выражения новых ипостасей Идей, которые осознал Брауэр, в европейской науке еще не было выработано, Брауэр ссылался на интуицию как инструмент их понимания. Поэтому он назвал предлагаемую обновленную логику и математику интуиционистской. Иногда он употреблял и другое название, связанное с центральной ролью конструкций в предлагаемой модификации математики и логики, — конструктивная логика и математика. Исторически в дальнейшем эти два термина разошлись. Названия ‘интуиционизм’ и ‘интуиционистская логика’ остались за системами, идущими напрямую от оригинальных брауэровских рассмотрений. ‘Конструктивизм’ и ‘конструктивная логика’ стали более общими терминами, характеризующими весь класс математик и логик, ставящих на первое место понятие задачи и конструкции, а не истины и обоснования5.

16.1.2. Интуиционизм и программа Гильберта Надо сказать, что при всей радикальности исходных принципиальных позиций Брауэр подошел к задаче реформирования логики и математики исключительно осторожно, пытаясь сохранить все, что не противоречит исходным принципам конструктивности.6 Чтобы проделать это максимально квалифицированно, он даже пошел на период стратегического отступления и, продекларировав необходимость замены математики, занялся вначале традиционной (как ее сегодня называют, классической) математикой. Он получил первоклассные результаты и завоевал настолько большой авторитет, что его ввели в редакцию ведущего в то время в мире математического журнала “Mathematische Annalen” (председателем редакционного совета которого был сам Давид Гильберт7 ).

Одна из его теорем вошла в золотой фонд математики:

В советской, а зачастую и в мировой, научной литературе термином ‘конструктивная математика’ или ‘конструктивное направление в математике’ порою называют конкретную ее разновидность, развивавшуюся в 50-е – 70-е гг. в СССР под руководством А. А. Маркова.

Это стало особенно ясно после появления гораздо более радикальных программ, в частности, узкого конструктивизма Н. А. Шанина.

Давид Гильберт считается одним из самых выдающихся математиков, когда-либо живших на Земле. Он получил принципиальные результаты в самых разных разделах математики, в том числе и в логике. Но еще важнее, чем его результаты, была формуГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА Теорема 16.1. (Теорема Брауэра о неподвижной точке) Любое непрерывное отображение n-мерного шара в себя имеет неподвижную точку.

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

Работы и декларации Брауэра вызвали раздражение у Гильберта, который считал, что Брауэр выплескивает вместе с водой и ребенка8. Но Гильберт не мог игнорировать критики Брауэра и поэтому предложил свою программу спасения классической математики, в которой был ряд важнейших мировоззренческих моментов.

1. Необходимо четко осознать, что подавляющее большинство математических объектов и теорем никаких прообразов в реальном мире не имеют. Реальными являются лишь утверждения типа 2 = 4, а число и теорема Ферма — уже идеальные объект и высказывание. В принципе идеальные объекты и результаты нужны лишь как промежуточные стадии для получения реальных результатов и в данном смысле не являются необходимыми9.

2. Тем не менее математика не может существовать без идеальных объектов, поскольку иначе мы не могли бы практически получить лировка им 20-ти проблем математики на I международном конгрессе математиков.

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

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

В данном пункте Гильберт полностью признал обоснованность критики Брауэра.

многих реальных результатов. Таким образом, идеальные объекты необходимы для эффективности нашего мышления10.

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

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

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

Хотя взаимодействие между Брауэром и Гильбертом привело к формулировке Гильбертом весьма разумной программы (более разумной, чем В данном пункте Гильберт предвосхитил результаты о потрясающей сложности (либо даже невозможности) устранения объектов и утверждений высших уровней из математических доказательств. См., например, в § 11.8. Другое дело, что Гильберт, видимо, не предвидел парадокса изобретателя (теорема 13.8) в столь сильной форме.

Ничего не возразишь! Даже Брауэр заявил, что после такого обоснования он бы снял все возражения против классической математики, лишь бы сами математики классического направления перестали говорить о реальном смысле, кроющемся за идеальными объектами и утверждениями.

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

И после десятилетия попыток в данном направлении, когда Гильберт неоднократно объявлял, что искомые доказательства почти получены, остались лишь несколько незначительных частных случаев — теорема Гёделя о неполноте! Она произвела впечатление атомной бомбы, полностью уничтожившей программу Гильберта, и все, сконцентрировавшись на предложенных Гильбертом средствах, забыли его основную цель — пункт 3.

А средства ведь не только что не необходимы, но иногда даже не достаточны для главной цели! Сам Гильберт пытался заметить, да и Гёдель говорил, что опровергнуты лишь конкретные средства достижения цели, но их никто уже не слушал.

ГЛАВА 16. ИНТУИЦИОНИСТСКАЯ ЛОГИКА

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

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

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

16.1.3. Формализация и первые интерпретации Брауэр неоднократно заявлял, что, в отличие от классической математики, интуиционистская принципиально не может быть формализована, но тем не менее поставил перед своим учеником А. Гейтингом задачу формализации интуиционистской логики, и Гейтинг ее успешно решил.

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

Как только появилась формализация интуиционистской логики, почти сразу же была дана и ее первая строгая интерпретация. Она осноСОЗДАНИЕ ИНТУИЦИОНИСТСКОЙ ЛОГИКИ вывалась на идее алгебр Линденбаума-Тарского и, в свою очередь, была подтверждением их силы как математического аппарата. Было сформулировано понятие псевдобулевой алгебры и дана интерпретация интуиционистской логики как логики со значениями в псевдобулевых алгебрах.

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

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