Формализм в математике

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

История

Предпосылки возникновения

К концу XIX века в математике накопился ряд парадоксов и противоречий, связанных с теорией множеств и основаниями анализа. Кризис оснований, вызванный, в частности, парадоксом Рассела (1901), показал, что наивная теория множеств Георга Кантора приводит к логическим противоречиям. В ответ на это возникли три основных философских подхода к обоснованию математики: логицизм (Готлоб Фреге, Бертран Рассел), интуиционизм (Лёйтзен Брауэр) и формализм.

Программа Гильберта

В 1920-е годы Давид Гильберт предложил программу, целью которой было доказательство непротиворечивости всей математики с помощью конечных (финитарных) методов. Основные идеи программы:

1. Формализация: вся математика должна быть представлена в виде формальной аксиоматической системы, где все утверждения записываются на точном символическом языке.
2. Метаматематика: изучение свойств формальных систем (непротиворечивость, полнота, разрешимость) должно проводиться с помощью содержательных, но финитарных рассуждений.
3. Доказательство непротиворечивости: предполагалось, что с помощью метаматематики можно доказать, что в формальной системе невозможно вывести противоречие (например, утверждение A и его отрицание ¬A).

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

Теоремы Гёделя и крах программы

В 1931 году австрийский логик Курт Гёдель опубликовал две теоремы о неполноте, которые нанесли сокрушительный удар по программе Гильберта:

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

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

Развитие после Гёделя

Несмотря на крах исходной программы, формализм не исчез. В 1930-е — 1960-е годы были разработаны методы, позволяющие доказывать непротиворечивость отдельных систем с помощью более сильных (нефинитарных) средств. Например, Герхард Генцен в 1936 году доказал непротиворечивость арифметики Пеано, используя трансфинитную индукцию до ординала ε₀. В современной математике формализм остаётся влиятельным подходом, особенно в области математической логики, теории доказательств и информатики.

Основные принципы

Формальная система

Центральное понятие формализма — формальная система, которая состоит из:

• Алфавита: конечного набора символов (буквы, цифры, знаки операций, скобки).
• Грамматики: правил построения правильно построенных формул (термов, выражений).
• Аксиом: конечного набора формул, принимаемых за истинные без доказательства.
• Правил вывода: правил, по которым из одних формул можно получать другие (например, modus ponens).

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

Непротиворечивость

Формальная система называется непротиворечивой, если в ней нельзя вывести одновременно формулу и её отрицание. Непротиворечивость — ключевое требование формализма, поскольку противоречивая система позволяет доказать любое утверждение (принцип взрыва).

Полнота

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

Разрешимость

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

Критика

Интуиционизм

Интуиционисты (Л. Брауэр, А. Гейтинг) возражали против формализма, утверждая, что математические объекты существуют только как конструкции человеческого разума, а не как формальные символы. Они отвергали закон исключённого третьего в бесконечных контекстах и требовали конструктивных доказательств.

Логицизм

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

Платонизм

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

Практические ограничения

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

Применение

Математическая логика и теория доказательств

Формализм является основой современной математической логики. Формальные системы используются для изучения свойств логических исчислений, доказательств и алгоритмов. Теория доказательств (proof theory) занимается анализом формальных выводов, их структурой и сложностью.

Информатика и программирование

Формальные методы широко применяются в информатике:

• Формальная верификация: проверка корректности программ и аппаратного обеспечения с помощью формальных спецификаций и доказательств.
• Теория типов: формальные системы типов в языках программирования (например, Haskell, Agda, Coq).
• Автоматическое доказательство теорем: программы, которые ищут формальные доказательства (например, Isabelle, Z3).

Основания математики

Формализм остаётся важным инструментом для исследования оснований математики. Хотя программа Гильберта не была реализована полностью, её идеи привели к созданию теории доказательств, теории моделей и теории рекурсии.

Интересные факты

• Давид Гильберт в 1930 году, за год до теорем Гёделя, заявил: «Мы должны знать — мы будем знать» (Wir müssen wissen — wir werden wissen). Эти слова высечены на его могиле.
• Курт Гёдель, будучи платонистом, считал, что формализм не может объяснить природу математической истины, но признавал его полезность для логического анализа.
• В 1970-е годы американский логик Харви Фридман разработал программу «обратной математики», которая изучает, какие аксиомы необходимы для доказательства тех или иных теорем, что является развитием формалистского подхода.
• Формализм лёг в основу системы доказательств Coq, которая используется для верификации критически важного программного обеспечения, включая ядро операционной системы Microsoft Windows и компилятор языка C.
• В 2010-е годы формальные методы стали применяться в математике для проверки сложных доказательств, например, доказательства теоремы о четырёх красках (1976) и теоремы Ферма (1994).

Источники

• Гильберт Д., Бернайс П. Основания математики. — М.: Наука, 1979.
• Гёдель К. О формально неразрешимых предложениях Principia Mathematica и родственных систем. — В кн.: Математическая логика и её применения. — М.: Мир, 1965.
• Клини С. К. Введение в метаматематику. — М.: Иностранная литература, 1957.
• Френкель А. А., Бар-Хиллел И. Основания теории множеств. — М.: Мир, 1966.
• Детловс В. К. Формализм в математике // Новая философская энциклопедия. — М.: Мысль, 2010.