Программа формализма: математика как конструирование формальных систем

В начале 20-х гг. XX в. немецкий математик Давид Гильберт (1862−1943), подталкиваемый собственными исследованиями, а также спорами с логицистами и интуиционистами, предложил новую программу обоснования классической математики, получившую название программа Гильберта. Другие названия этой программы, принятые в литературе, — теория доказательства, метаматематика. Ее целью были формализация всей математики в аксиоматической форме и доказательство определенными «финитными» методами, что полученная аксиоматизация непротиворечива. Кроме Гильберта, в разработке программы в разное время принимали активное участие такие логики и математики, как В. Аккерман, П. Бернайс, Г. Генцен, Дж. фон Нейман и Ж. Эрбран. Программа Гильберта включает следующие тезисы:

• • Ни классическая, ни логицистская, ни интуиционистская программы обоснования математики не предложили критерия, обосновывающего всю математику. Таким критерием может быть только ее непротиворечивость. Пока не будет разработан метод доказательства непротиворечивости всей математики, споры в этой области знания никогда не прекратятся.
• • Новый метод должен быть формально аксиоматическим, потому что содержательная аксиоматика апеллирует к интуитивной или опытной очевидности аксиом. Формальная аксиоматика тоже нуждается в очевидности, но особого рода, свойственной не отдельной конкретной области математической науки, а всей математике в целом.
• • Каждая теория — упрощающая идеализация, экстраполирующая свои базисные понятия за пределы наличных данных опыта. Поэтому для установления непротиворечивости теории недостаточно ссылки на ее совместимость с имеющимися данными. Необходимо иметь уверенность, что теория непротиворечива для всех объектов соответствующего вида.
• • Непротиворечивость математики не может быть установлена общепринятым методом интерпретации ее основных объектов посредством чисел и числовых систем, а основные отношения между ними — посредством равенств и неравенств. То, что годится для доказательства непротиворечивости, допустим, геометрии, не может быть перенесено на всю математику. Ибо в этом случае встает вопрос о непротиворечивости той математической теории — арифметики или анализа, с помощью которых доказывается непротиворечивость всех остальных частей математики.
• • Непротиворечивость всей математики не может быть дедуцирована из аксиом логики или данных интуиции. Все попытки вывести математику из логики оказались несостоятельны, потому что основаны на проблематичном представлении о натуральном ряде чисел как завершенной совокупности. Еще более проблематичными из-за очевидного субъективизма выглядят попытки обосновать непротиворечивость математики на априорной интуиции времени.
• • Доказательство непротиворечивости всей математики состоит из двух этапов. На первом формализуется базис математики — теория множеств, арифметика и анализ, т. е. строится формальная система, из аксиом которой с помощью четко определенных правил выводятся все теоремы, относящиеся к перечисленным разделам. Система должна быть формализованной до такой степени, чтобы во внимание принимались только вид и порядок символов и ничего более.
• • На втором этапе доказывается, что применение правил вывода к аксиомам построенной формальной системы никогда не сможет привести к противоречию вида 1 ф 1. В построенной формальной системе недопустимы не только противоречия, но и применение закона исключенного третьего к бесконечным совокупностям объектов, экзистенциальные утверждения на основании ложности общих утверждений, а также непредикативные определения.
• • Формализованный вариант классической математики должен быть свободен от ограничений, которые пытались на нее наложить интуиционисты.