Формалі́зм — один з підходів у філософії математики, згідно з яким математичні об'єкти розглядають як чітко задані послідовності символів, а дослідження цих об'єктів зводять до перетворень над цими символами за встановленими правилами.

Основна ідея формалізму полягає в тому, що математика спрямована на дослідження виключно формальних систем, а не абстракцій з реального світу, що протиставляється філософії інтуїціонізму. Наприклад, якщо для інтуїціоніста число 2 — це абстракція кількості, з якою ми маємо справу в повсякденному житті, то для формаліста число 2 — це лише певна послідовність символів як-то , позбавлена будь-якого сенсу.

Історія

Формалізм виник наприкінці XIX століття та набув бурхливого розвитку у XX столітті як основний з напрямів, спрямованих на вирішення кризи основ математики.

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

Основоположником формалізму в математиці вважають німецького математика Давида Гільберта та його школу, до якої входили його учні Вільгельм Аккерман, Пауль Бернайс, Джон фон Нейман. Програма Гільберта мала на меті побудову повної та несуперечливої аксіоматики всієї математики.

Учень Гільберта Отто Блументаль у своєму біографічному нарисіBlumenthal, Otto (1935). David Hilbert. У: Hilbert, David. Gesammelte Abhandlungen. Bd. III. Berlin: Springer. С. 403. наводить одну з цитат свого вчителя, яка яскраво демонструє суть ідеї формалізму:

Теореми Геделя про неповноту

Філософія формалізму зазнала серйозного удару після публікації Куртом Геделем у 1931 році теорем про неповноту. Ці результати показали принципову обмеженість усіх достатньо сильних формальних систем. Зокрема, якщо формальна арифметика несуперечлива, то в ній існують формули, які неможливо ані довести, ані спростувати.

Ніколя Бурбакі

Відома група французьких математиків-формалістів під колективним псевдонімом Ніколя Бурбакі, створена у 1935 році, поставила за мету написати серію книг, яка б покрила усю сучасну на той час математику. У їхніх працях, зокрема в базовій книзі «Теорія множин», простежуються риси крайнього формалізму.

У працях Бурбакі усі математичні об'єкти (терми та співвідношення) записуються як послідовності деяких символів (серед них, наприклад, ¬, ∨, τ, □, ∈) та зв'язків між ними, причому ці послідовності навіть для достатньо «простих» об'єктів є надзвичайно довгими. Наприклад, щоб записати означення числа 1 через елементарні символи, потрібно порядку символів та стільки ж зв'язків між ними, що не вміститься на жодному носії інформації.

Бурбакі істотно вплинули на розвиток ідей формалізму. Вони ввели в широкий ужиток позначення порожньої множини та числових множин , які зараз є стандартними позначеннями.

Сучасний стан

У кінці XX та на початку XXI століття формалізм посів центральне місце в математичній практиці, що пов'язано зі стрімким розвитком інформаційних технологій, а також штучного інтелекту останніми роками. Формалізація математичних об'єктів та тверджень необхідна для того, щоб комп'ютери мали змогу зберігати та обробляти таку інформацію. Зокрема, це необхідно для перевірки та автоматичного пошуку доведень.

Серед сучасних інструментів формалізації можна виділити Lean. Ця система використовує свою однойменну мову програмування для означення математичних понять, формулювання та доведення математичних тверджень. Lean автоматично перевіряє коректність доведень, записаних у вигляді коду.

Велика кількість математиків-ентузіастів працює над проєктом mathlib — проєктом з формалізації основних розділів сучасної математики: алгебра, аналіз, теорія ймовірностей та ін.

Примітки

Джерела

Bourbaki, Nicolas. Elements of the History of Mathematics. Berlin: Springer, 1994. ISBN 978-3-540-57311-2.