Когда я был маленький, я думал, что математика - это очень формальная наука. Как бы не так! Когда о нас, математиках, говорят как о сухарях — это ложь! (с) 17 мгновений весны.
Приглашаю вас в путешествие по 6 уровням вселенной математики - от полностью формального до философско-поэтического, и заодно мы ответим на вопрос, является ли теорема Геделя теоремой или мета-теоремой.
1 уровень - логика первого порядка
Начнем с сухих формальных теорем - например, x(y+z) = xy + xz. Это простое выражение является арифметической (и алгебраической) теоремой и легко доказывается в формальной арифметике. Это самый простой случай.
Однако не все так просто, если мы возьмем, например, Великую теорему Ферма, которую можно записать формально вот так:
Кстати
Интересно что с точки зрения теории сложности, где сложность считается по числу перемежающихся кванторов общности и существования, великая теорема Ферма является очень простой: в ней есть только кванторы общности. В частности, можно написать машину Тьюринга, которая будет перебирать все варианты и остановится, только если теорема неверна.
Вы конечно же знаете, что великая теорема Ферма доказана.в 1994 году. Однако методы, используемые в этом доказательстве, далеко выходят за рамки формальной арифметики. То есть теорема сама арифметическая, а вот доказательство - нет. Можно ли доказать эту теорему, оставаясь внутри арифметики - неизвестно. Но эта тема (какой минимальной силы теории достаточно, чтобы доказать эту уже доказанную теорему) - основной мотив обратной математики.
Если для теоремы Ферма неизвестно, можно ли ее доказать арифметически, то для теоремы Гудстейна, тоже арифметической, достоверно известно, что арифметического доказательства не существует. Зато она довольно тривиально доказывается даже в очень слабых версиях теории множеств.
Бывают и другие проблемы с доказательствами, например, доказательство теоремы четырех цветов не было сразу принято всеми математиками, потому что было сгенерировано компьютером. А доказательство abc-теоремы действует только на территории Японии. Однако, существуют компьютерные системы для автоматической верификации доказательств, так что на этом, самом первом уровне, все будет хорошо.
2 уровень - теории второго порядка
Объяснить отличие теории второго порядка для программиста очень легко: надо задуматься, какого типа переменная может стоять после квантора. Если это число (или иной простой объект, если теория не о числах, но мы пока отталкиваемcя от арифметики) - то это теория первого порядка.
Если переменная имеет тип 'любое выражение', то это теория второго порядка. Когда в школе нас учили анализу и произносили 'для любой фунцкии...', то это как раз был второй порядок. Сила теорий второго порядка значительно, значительно превышает силу теорий первого, но их основание, как мы увидим, немного более зыбко. Вообще, чем выше мы полезем, тем больше все будет ходить ходуном.
Имеется еще промежуточный уровень по силе, monadic 2nd order, где выражения в кванторах указывать нельзя, зато можно указывать множества.
Как правило, выражения обозначаются uppercase:
В данном случае X - это выражение, а если вы узнали в записи выше принцип математической индукции, то вы большой молодец. Секундочку... Но ведь принцип математической индукции используется и в формальной арифметике первого порядка! Но как - ведь по своей сути это типичное правило второго порядка!
Ответ такой: regexp. Да, да, именно он. В арифметике первого порядка принцип математической индукции выражается бесконечным количеством аксиом, подходящим под regexp. Немножко некрасиво, но работает.
Мы пока не говорили про теорему Геделя, но для теорий второго порядка она не работает. Возможно, есть какие-то аналоги. Но вообще с теориями второго порядка надо осторожнее - недаром арифметику второго порядка называют теорией множеств в овечей шкуре:
Теория множеств сравнивается с "волком" за число парадоксов, безумное число версий и вариантов теории, что может сравниться лишь с деревом вариантов *Unix. Впрочем, теория множеств - это теория первого порядка, и то, что она может успешно имитировать большинство (не все) аспекты теории второго говорит об ее чудовищной силе.
3 уровень - мета теоремы
Здесь мы добрались до Теоремы Геделя (их несколько), первая из которых утверждает, что в формальной арифметике существует выражение W, которое истинно, но недоказуемо:
Здесь PA - Peano Arithmetics. Мета теорема Геделя доказывается с помощью придания второго смысла математическим выражениям, а затем с помощью диагонального метода формируется выражение W, которое имеет дополнительный смысл: "я недоказуемо"
Запись
Означает, что утверждение E может быть доказано в теории T, и как раз этот момент и выводит нас на третий уровень логики, так как понятие "может быть доказано" не выразимо в логиках ни первого, ни второго порядков (хотя теорема Геделя и связывает доказуемость со свойствами чисел)
Интересно, что выражение W можно записать явно (мета теорема Геделя конструктивна). Я видел картинку с очень длинной формулой для W, но сейчас отыскать ее не смог. Может кто-нибудь из читателей сможет?
Я как то имел спор с человеком, который утверждал, что теорема Геделя - это арифметическая теорема, потому что выражение W выразимо в арифметике. Однако даже в этом случае доказательство производится на мета уровне и в арифметике не выразимо. Кроме того, теоремой Геделя мы называем утверждение о существовании недоказуемых утверждений в PA, а не длинное и лишенное, на первый взгляд, особого смысла длиннющее выражение W.
Если вас интересует, есть ли в арифметике более короткие недоказуемые утверждения, то да - теорема Гудстейна, которую я уже упоминал.
4 уровень - кванторы по теориям
Есть расширения теоремы Геделя, которые иногда неряшливо тоже называют теоремой Геделя. Между тем, это новый, более высокий мета уровень. Рассмотрим эти расширения:
Первое обобщение теоремы Геделя: если в PA добавить недоказуемое утверждение W в качестве новой аксиомы, то получившаяся новая теория (PA+W) все равно содержит новое недоказуемое утверждение W1, и так далее. То есть это системный баг, его не пофиксить, добавив новые аксиомы
Вы заметили квантор по теориям?
Второе обобщение теоремы Геделя: любая непротиворечивая теория, в которой выразима формальная арифметика, неполна, то есть к ней применим вариант теоремы Геделя (дополнительно требуется, чтобы система аксиом либо была конечной, либо все regexp были алгоритмически разрешимы)
Тут квантор совсем уж явен.
На этом же мета-мета уровне, теории о теориях, находится теория моделей. Она изучает, а какие же наборы объектов удовлетворяют теориям? Из интересных выводов этой теории:
Теории первого порядка не способны контролировать мощность своих моделей: если есть бесконечная модель, то есть и другие модели любой бесконечной мощности.
То есть формальная арифметика описывает не только натуральные числа (их счетное количество), но другие наборы фишек (например, мощности континуума), которые удовлетворяют всем правилам игры в арифметику! Такие модели называются нестандартными.
В другую сторону это тоже работает: теория вещественных чисел (коих континуум) имеет счетную модель (what???). Теория множеств ZFC имеет тоже счетную модель, хотя в этой модели некоторые фишки удовлетворяют формуле 'это множество несчетно'. Этот парадокс называется парадоксом Скулема.
Теории второго порядка, кстати, способны контролировать мощность своих моделей, поэтому они не сводимы к теориям первого порядка с помощью разных трюков.
Меня заинтересовал такой вопрос: модель теории - это множество объектов, которые могут этой теории удовлетворять, но какую версию теории множеств мы используем на этом уровне? Ответы математиков несколько путаны и противоречивы. В любом случае тут здание шатается уже очень сильно, того и гляди наступишь на грабли противоречивой 'наивной' теории множеств. А сделать это легче легкого: например, в альтернативной теории множеств New Foundations существует 'множество всех множеств', не создавая противоречия.
5 уровень - кванторы по логикам
Что может быть еще более абстрактного, чем кванторы по теориям? Теории, как правило, все таки полагаются на общие логические правила. Но не всегда: существует интуиционисткая логика, отрицающая принцип исключенного третьего. Она тесно связана с конструктивной математикой, где нельзя доказать существование чего-либо 'от противного', объект обязательно надо 'предъявить'. Возможны и другие версии логик.
Вот пример рассуждения на этом уровне отсюда: здесь доказывается, что из AC (знаменитой аксиомы выбора) следует правило исключенного третьего, а значит, конструктивная математика и AC несовместимы, если вы не готовы на другие жертвы:
we note that in deriving Excluded Middle from ACL1 essential use was made of the principles of Predicative Comprehension and Extensionality of Functions[18]. It follows that, in systems of constructive mathematics affirming AC (but not Excluded Middle) either the principle of Predicative Comprehension or the principle of Extensionality of Functions must fail.
The principle of Extensionality can easily be made to fail by considering, for example, the predicates P: rational featherless biped and Q: human being and the function K on predicates which assigns to each predicate the number of words in its description. Then we can agree that P≈Q but KP=3 and KQ=2.
6 уровень - философия
Да, здесь уже чистая философия, правда, замешанная на математике.
Вот например: Как относиться к тому, что разные математические теории могут давать разные, зачастую диаметрально противоположные выводы? Математики придерживаются разных убеждений: формалисты просто говорят: это игра. Мы задали разные правила, и получили разные результаты. Чему удивляться?
Платонисты же видят некую реальность за формулами, ведь теории придуманы не просто так. Например, теория множеств NF (New Foundations) построена на совершенно других принципах, чем классическая ZFC, но почему-то повторяет ее выводы о недостижимых мощностях. В NF, где есть universal set, правда, не работает AC, но это происходит и в ZFC для очень больших мощностей... Совпадение? Или подсказка, что за формулами что-то есть?
