Программа формализма

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

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

1. Признать, что значительная часть математических абстрактных объектов — это идеальные конструкции, не имеющие точной интерпретации во внешнем мире и вводимые, прежде всего, как интеллектуальные инструменты для работы с реальными объектами. Более того, не все математические высказывания о реальных объектах могут считаться реальными. Назначение идеальных объектов и высказываний — перебросить мост от одних реальных высказываний к другим.
2. Точно и до конца формализовать допустимые методы работы с идеальными конструкциями, с тем, чтобы исключить здесь обращения к интуиции и апелляции к содержательному смыслу. Таким образом, математика должна быть превращена в исчисление.
3. Создать метаматематику, которая должна иметь дело с частным случаем реальных объектов — математическими формализмами, и строго обосновать при помощи как можно более простых, интуитивно ясных и не вызывающих сомнения у конструктивистов методов (финитных методов) принципиальную возможность устранения идеальных объектов и высказываний из доказательств реальных утверждений. Математическую теорию, развитую для потребностей метаматематики, Гилберт назвал «теорией доказательств». В качестве метода такого обоснования предполагалось доказать непротиворечивость, а по возможности и полноту, математических формализмов.

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

Воспользовавшись достижениями логицизма, в частности фундаментальным трудом «Princіріа Mathematica» А. Н. Уайтхеда и Б. Рассела (1910–1913), школа Гилберта (П. Бернайс, В. Аккерман, Г. Генцен и другие) уже в 1920-е годы точно сформулировала формальное исчисление для арифметики и стимулировала работы по формальной аксиоматизации теории множеств. Интенсивно велись исследования в направлении непротиворечивости и полноты построенного арифметического исчисления. Действуя под сильным влиянием формализма, А. Тарский и Р. Карнап определили понятие истины и вместе с Л. Витгенштейном сформулировали наиболее важные понятия верифицируемости и фальсифицируемости, связывающие идеальные высказывания с реальными. Философская суть их состоит в том, что любое утверждение должно допускать прямую либо косвенную процедуру подтверждения или опровержения. Утверждения, которые не могут быть проверены даже косвенно, — псевдопроблемы.

Парадоксальным образом одним из первых теоретических конструктов (см. Конструкт), проверенных при помощи формалистских методов, явилась сама программа Гилберта. Теорема К. Гёделя о неполноте показала, что цель-максимум её недостижима, а его же (Гёделя) теорема о недоказуемости непротиворечивости показала, что фальсифицируется и предложенное Гилбертом средство. Таким образом, была показана принципиальная ограниченность концепции формализма. Несмотря на защиту Л. Э. Я. Брауэром, который в других случаях резко критиковал его, но соглашался с целями программы Гилберта, научная общественность восприняла результаты Гёделя как крах программы Гилберта.

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

Вместе с тем, дальнейшее развитие подтвердило скорее точку зрения Брауэра, чем большинства. Теория доказательств стала приносить позитивные результаты. В 1936 году Г. Генцен опубликовал доказательство непротиворечивости арифметики, в котором единственным неформализуемым в арифметике шагом была трансфинитная индукция до ε₀, которая, безусловно, косвенно верифицируема и фальсифицируема содержательными полностью финитными методами и конструктивно приемлема. Ещё раньше, в 1934 году, он опубликовал доказательство теоремы нормализации, из которого следовала возможность устранения промежуточных идеальных высказываний из логических выводов реальных высказываний. В 1939 году П. С. Новиков установил, что из классического арифметического доказательства существования объекта, удовлетворяющего разрешимому условию, следует возможность построить такой объект. Тем самым реальные утверждения, доказуемые в арифметике, оказались обоснованными. В дальнейшем были получены оценки роста длины вывода при устранении идеальных понятий, подтвердившие прозрение Гилберта о необходимости идеальных объектов и понятий для практического получения реальных результатов.

Обращают на себя внимание философские и методологические достижения программы формализма, вошедшие в основу современной науки (см. Наука). Методами формализма были исследованы неклассические, в первую очередь интуиционистские (см. Интуиционизм), системы, что позволило показать совместимость идей Брауэра о творящем субъекте и намеренном незнании с более традиционными идеальными математическими понятиями. Различение идеальных и реальных объектов проложило путь к таким новым по своей методологии разделам математики, как нестандартный анализ, в котором действительная ось либо другая структура пополняются объектами более высокой степени идеальности таким образом, чтобы сохранялись все выразимые в формальном языке свойства. Разделение на язык и метаязык оказалось плодотворным не только в логике и философии, но и в таких новых дисциплинах, как когнитивная наука и информатика. Четыре уровня метаязыкового описания используются, в частности, в практической системе построения моделей сложных систем UML. Было отброшено ограничение Гилберта о финитности метаязыка, и ныне метаязыком может служить любая система. Применение таких методов формализма в физике позволило оценить глубину прозрения И. Канта об априорности математических понятий по отношению к физическим. Выяснилось, что вся современная физика логически следует из решения измерять величины действительными числами и в этом смысле оправдывает парадоксальное высказывание Канта, что «Разум диктует законы Природе».