7. О доказательствах
В современной математике, в силу разделения её языка на синтаксическую и семантическую части, возникли два понятия следствия из посылок. Одно из этих понятий, которое мы будем называть логическим или дедуктивным, совпадает с понятием логической выводимости (доказуемости) предложения А из посылок Г, что обозначается обычно так: Г А. Второе понятие, которое мы назовём семантическим Традиционно за этим видом следствия закрепился термин «логическое», хотя на наш взгляд это не соответствует смыслу понятия «логический», что больше подходит к первому виду., связано с моделями множества Г и состоит в следующем. Предложение А является семантическим следствием множества предложений Г, если оно истинно в любой модели множества Г, что обозначается так: Г А. Поскольку логический вывод сохраняет истинность во всех интерпретациях, то ясно, что Г А влечёт Г А. Обратное далеко не столь очевидно, но оно следует из теоремы Гёделя о полноте. Таким образом, эти понятия оказываются равносильными, и следовательно, если Г - это система аксиом теории, то выводимость (доказуемость) формулы А из Г равносильна её семантической истинности в этой теории.
Теорема Гёделя о полноте утверждает, что всякое непротиворечивое множество формул (в языке предикатов первой ступени) имеет модель. Отсюда следует, что для любой замкнутой Формула называется замкнутой, если она не содержит свободных, т.е. не связанных кванторами переменных. формулы А, если Г А, то Г А. Действительно, предположим, что (Г А). Можно доказать, что тогда множество Г, А - непротиворечиво и потому по теореме Гёделя оно имеет модель, в которой формула А истинна, а это противоречит тому, что Г А. Поэтому (Г А), откуда по правилу контрапозиции, если Г А, то Г А. Отсюда же следует и семантическая полнота исчисления предикатов первой ступени.
Все доказательства предложений любой математической теории можно разделить на два вида. К первому виду отнесём такие доказательства, которые касаются только синтаксических свойств теории без ссылок на какую-либо интерпретацию. Таковыми, например, являются все формальные доказательства в формальных теориях, которые фактически являются выводами слов в языке теории из аксиом строго по логическим правилам. Будем называть такие доказательства синтаксическими. Второй вид - это доказательства, апеллирующие к каким-либо интерпретациям языка теории. Назовем их семантическими. Как уже было сказано выше, правильность формального синтаксического доказательства устанавливается алгоритмически, и следовательно, можно сказать, вполне надёжно. Согласно тезису Гильберта (см. п.3), всякое неформальное доказательство имеет формальный эквивалент и потому мы можем считать надёжным любое синтаксическое доказательство.
Доказательства второго вида содержат апелляцию к семантике, которая, как правило, не является аксиоматической теорией и не всегда может быть аксиоматизирована (как это имеет место для содержательной арифметики). Поэтому посылки таких доказательств черпаются из заранее не определённого множества содержательных предложений такой теории. Хотя для всякого семантического доказательства можно получить синтаксический аналог, если формализовать соответствующую содержательную теорию, однако последнее не всегда возможно по разным причинам. Тем не менее для каждого семантического доказательства существует возможность получить синтаксический эквивалент путём аксиоматизации не всей теории, а только её фрагмента, содержащего посылки доказательства. Такую возможность даёт теорема компактности (см., напр., [Мал], [Бар]), из которой следует, что для всякой теоремы А какой-либо теории Т существует конечно аксиоматизируемый фрагмент Т1 этой теории, в котором доказуема теорема А. Это утверждение верно как для формальных так и для неформальных теорий. Мы будем называть его принципом локальной формализации. Этот принцип имеет очень важное следствие: при оценке какого-либо семантического (содержательного) доказательства в неформальной теории можно выделить конечно аксиоматизированный фрагмент теории, содержащий синтаксический эквивалент этого доказательства. Этот процесс вполне эффективен (финитен). Таким образом, принцип локальной формализации позволяет оценку правильности семантического доказательства сводить к оценке синтаксического доказательства. Подчеркнём, что здесь речь идёт о проверке правильности доказательств, безотносительно к непротиворечивости всей теории.
8. Подробнее о непротиворечивости
Рассмотрим теперь вопрос о возможности надёжного доказательства непротиворечивости теорий. Как мы уже отмечали на примере арифметики, нужный результат может быть получен путем расширения логических средств доказательства дополнительными правилами. Другая возможность - доказательство непротиворечивости теории путем построения математической модели - может быть вполне убедительной, если непротиворечива сама модель и отображение теории в модель в сильном смысле конструктивно (финитно). Поскольку моделью как правило является содержательная математическая теория, то может показаться, что мы попадаем в безвыходную ситуацию: чтобы доказать непротиворечивость теории, нужно построить какую-либо её модель, которая в свою очередь принадлежит теории, непротиворечивость которой также должна быть доказана. Подчеркнём, что модель непременно должна принадлежать математической теории (не обязательно формальной), т.е. не должна апеллировать к каким-либо реальным понятиям. Практически такую ситуацию очень часто удается избежать путем построения в сильном смысле финитной модели, непротиворечивость которой невозможно подвергнуть сомнению. Наглядным примером этого является доказательство непротиворечивости логики предикатов первой ступени, которое мы рассмотрим в п.9.
Отмеченная нами надёжная правильность формальных доказательств, помимо прочего, основана на непротиворечивости формальной математической логики, что также требует доказательства. Каким образом вырваться из возникающего здесь круга, мы продемонстрируем в п.9. До этого непротиворечивость логики предикатов (первой ступени) примем как факт.
Вопрос о непротиворечивости теорий несравненно более трудный, чем вопрос о доказательствах. Для формальных теорий он несколько облегчается чёткостью постановки и существованием различных подходов, например, таких, как использованные для доказательства непротиворечивости арифметики (см. п.4.6). Если теория не формальная, то далеко не всегда удаётся найти прямое доказательство её непротиворечивости. В этом случае приходится апеллировать к непротиворечивости какой-либо её модели, в которой истинны все аксиомы теории или, по крайней мере, посылки рассматриваемого доказательства. Как правило, удаётся построить содержательно более простую модель, чем исходная теория, и таким образом упростить задачу.
Определённую уверенность в непротиворечивости содержательно построенных математических теорий создаёт распространённое (по крайней мере, среди математиков) мнение, что исходные понятия, лежащие в основе любой математической теории, имеют объективный характер и не являются только произвольным плодом свободной человеческой фантазии. Вопрос об объективности математических понятий, безусловно, выходит за рамки математики, однако, как показывает исторический опыт, большинство математиков и философов всегда считало и считает математические объекты принадлежащими в том или ином смысле реальному миру идей, который так же непротиворечив, как и материальный мир. В подтверждение этого мнения приведём одну цитату из [Бур]: «Каковы бы ни были философские оттенки, в которые понятие математических объектов окрашивалось у того или иного математика или философа, имеется по крайней мере один пункт, в котором они единодушны: это то, что эти объекты нам даны и не в нашей власти приписывать им произвольные свойства так же, как физик не может изменить какое-либо природное явление. … и даже сегодня не один математик, афиширующий непримиримый формализм, в глубине души охотно подписался бы под следующим признанием Эрмита: Я полагаю, что числа и функции Анализа не являются произвольным созданием нашего ума; я думаю, что они существуют вне нас с такой же необходимостью, как и предметы объективной реальности, и мы их встречаем или открываем и изучаем их так же, как физики, химики и зоологи».
Непротиворечивость мира идей нуждается в пояснении, поскольку существуют противоречащие друг другу идеи. Однако противоречивость каких-либо идей означает только их принадлежность разным мирам, подобно тому, как в математике существуют противоречащие друг другу теории, например, аксиоматики разных геометрий, непротиворечивые порознь, противоречивы в совокупности. Поэтому, как наличие противоречащих друг другу теорий не означает противоречивости всей математики, так и существование противоречащих друг другу миров не означает противоречивости мира идей. Впрочем, подобную картину можно наблюдать даже в физике, когда разные подходы приводили к противоречивым описаниям одного явления, что отнюдь не означает противоречивости реального мира.
Признав объективность исходных понятий, мы с необходимостью вынуждены будем признать и объективность их свойств, выраженных аксиомами теории. Это, конечно, ещё не доказывает непротиворечивость всякой математической теории, однако вселяет надежду на возможность такого доказательства, и даже - интуитивную уверенность в этом. Противники такой точки зрения обычно ссылаются на канторовскую теорию множеств, исходные объекты которой являются настолько простыми и естественными, что не вызывают никакого сомнения в их объективности. Однако, на наш взгляд возникающие там противоречия вызваны не характером исходных понятий и их свойств, а тем, что их язык оказывается настолько широким, что позволяет определять внутренне противоречивые ситуации и понятия, например такое, как «множество всех множеств» (см. п.2). Подобное явление присуще и естественному языку в силу его универсальности, что выражается в существовании различных «реальных» противоречий вроде «парадокса лжеца» и др. Надо сказать, что любую математическую теорию, путём введения новых понятий или чрезмерного расширения объёма её понятий можно сделать противоречивой. Поэтому введение новых понятий не только в формальную, но и в содержательную теорию должно сопровождаться тестом на непротиворечивость.
Вполне возможно, что гарантировать от противоречий такую универсальную теорию, как теория множеств, можно только путём её формализации. При этом получить единую формализацию, удовлетворяющую всевозможные потребности различных направлений математики, скорее всего не удастся, однако это означает только объективное многообразие логических возможностей в математике, но отнюдь не какую-то трагедию неопределённости, как это трактуется в книге [Кла].
Таким образом, резюмируя сказанное, мы можем определить понятие истинности предложений в математике как формальную доказуемость в непротиворечивой теории. Тем самым отнюдь не игнорируется семантическое понимание истинности теорем в той модели, для изучения которой предназначена данная теория, поскольку при непротиворечивой логике формальное доказательство теоремы гарантирует её истинность в модели. В следующем пункте в качестве примера мы рассмотрим одно из доказательств непротиворечивости логики предикатов первой ступени.
9. Непротиворечивость логики предикатов
Как уже говорилось, классом моделей логики предикатов первой ступени является множество всех алгебраических систем соответствующей сигнатуры, т.е. эта логика состоит из всех тех и только тех формул, которые истинны в любой алгебраической системе. В данном случае мы не можем рассчитывать на формальное доказательство, поскольку оно использует формальную логику, непротиворечивость которой нам нужно ещё доказать. Таким образом, уже на самом первом этапе построения формальной математики мы вынуждены прибегнуть к содержательным, т.е. интуитивно построенным доказательствам. К счастью, доказательство непротиворечивости исчисления предикатов первой ступени настолько просто реализуемо финитно, что не может вызвать никаких сомнений в его правильности. Для доказательства непротиворечивости этого исчисления достаточно рассмотреть одноэлементную модель, на которой все его формулы однозначно переходят (отображаются) в формулы так называемого исчисления высказываний (см. ниже). При этом все аксиомы переходят в тавтологии (тождественно истинные формулы), а правила вывода сохраняют тавтологичность формул (т.е., если посылки правила являются тавтологиями, то и заключение также тавтология). Таким образом, все доказуемые формулы исчисления предикатов в одноэлементной модели переходят в тавтологии. Поскольку легко привести пример формулы, не переходящей в тавтологию, то это означает существование недоказуемых формул, а значит и непротиворечивость исчисления предикатов. Таким образом, непротиворечивость логики предикатов первой ступени мы можем считать надёжно доказанной. (Разумеется, приведенные здесь рассуждения являются только схемой доказательства, но все необходимые детали описываются вполне финитно).
Логика высказываний (пропозициональная логика, булева алгебра) является важным фрагментом логики предикатов. Её основателем считается Дж.Буль (1815 - 1864). Множеством её объектов являются два логических значения - “истина” и “ложь”, обычно обозначаемые буквами 1 и 0. Её формулы строятся из этих констант и переменных с помощью тех же логических операций, что и формулы логики предикатов, за исключением кванторов. Собственно логика высказываний состоит из тавтологий - формул, которые при любой подстановке констант 1 и 0 вместо переменных принимают значение 1. Логика высказываний, представленная в виде аксиоматической системы называется исчислением высказываний. Его непротиворечивость легко доказывается вполне финитными средствами. Название “булева алгебра”, с одной стороны, указывает на её создателя, а с другой - на тот факт, что она совпадает (изоморфна) с двуэлементной алгеброй с так называемыми булевыми операциями. Булева алгебра является моделью исчисления высказываний, её операции умножения, суммы и дополнения интерпретируют логические операции конъюнкцию, дизъюнкцию и отрицание.