Формализм (математика)

Эта статья — о течении в философии математики. Другие значения термина «формализм» см. на соответствующей странице.

Формализм — один из подходов к философии математики, пытающийся свести проблему оснований математики к изучению формальных систем. Наряду с логицизмом и интуиционизмом считался в XX веке одним из направлений фундаментализма в философии математики.

История

Давид Гильберт

Формализм возник в начале XX века в математической школе Гильберта в рамках попытки свести в единую систему строгие обоснования различных областей математики. Развивался сотрудниками (учениками) Гильберта Аккерманом, П. Бернайсом, фон Нейманом.

В отличие от логицизма, формализм не претендовал на построение единой для всей математики формальной теории, наподобие теории множеств или теории типов. В отличие от интуиционизма, формализм не отказывался от построения теорий с «сомнительными» с точки зрения интуиции основаниями, лишь бы в них правила вывода теорем были строго обоснованы. Формалисты полагали, что математика должна изучать как можно больше формальных систем.

Критика

Формально-аксиоматические теории, построенные на основе классической логики, имеет смысл рассматривать лишь при отсутствии в них противоречий, поскольку в противном случае «доказанным» оказывается любое суждение теории. Если в такой формальной системе удаётся доказать логическую ложь, то она находится противоречивой и «выбраковывается», что обесценивает любые доказанные в рамках данной системы теоремы. Разумеется, математиков волновал вопрос, можно ли каким-то образом доказать непротиворечивость теории. К досаде формалистов, было показано, что вопрос о противоречивости теории не имеет адекватного разрешения внутри любой из употребительных в математике формальных систем.

Ничто не мешает изучать одну формальную теорию при помощи другой; такой подход называется метаматематическим. Однако, он вынуждает использовать для построения метатеорий наиболее надёжные основания, каковыми формалисты рассматривали, опять-таки, классическую логику и формальную арифметику.

Современное состояние

С начала 90-х годов XX века интерес к формализму (в более прикладном смысле) снова возрос в связи с задачами автоматического доказательства теорем (см. напр. en:QED manifesto).