Можливості і межі формалізації (філософський зміст теорем Геделя, Тарського)

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

Давид Гільберт (1862-1943), засновник формалістичної школи в математики, припускав, що все наше знання, і перш за все математичне, може бути повністю формалізовано.Ідеї Гільберта взяли багато талановитих математики, серед яких П. Бернайс (1888-1977), Дж. Гербрандта (1908-1931), В. Аккерман (1898-1962), Дж. фон Нейман (1903-1957).

Однак у 1931 р. Курт Гедел у статті «Про формально нерозвязних пропозиціях« Principia Mathematica »і споріднених систем» довів відому теорему про неповноту формалізованої арифметики. Він довів, що в системі «Principia Mathematica» і в будь-який інший формальної системи, здатної виразити арифметику натуральних чисел, є нерозвязні (тобто недоведені і разом з тим незаперечні в даній системі) пропозиції. Теорема Геделя свідчить про те, що арифметика натуральних чисел включає зміст, який не може бути виражена виключно на основі логічних правил освіти і перетворення відповідної формальної системи. Більш того, формула логічного числення, здатного формалізувати елементарну арифметику, бездоказова як формула, що виражає її послідовність. Таким чином, несуперечності не можна досягти, використовуючи інструменти, що належать до тієї ж формальної системі. Це було справжнє поразку програми Гільберта.

Неповнота формалізованих систем, що містять арифметику, означає, що у змістовній математичної теорії завжди можна знайти справжнє пропозиція, яку не можна довести за допомогою аксіом формальної теорії, формалізує змістовну цю теорію. Крім того, у більш багатої формальної системі, до якої недоведені пропозиція приєднано як аксіоми, його можна тривіально довести, але тим не менше і в новій системі є можливість побудувати аналогічне недоказово пропозицію і, таким чином, завжди залишається певний «формалізації залишок». Ця теорема показала неможливість дати у рамках формальної побудови підставу всій як сьогоднішній, так і майбутньої математіке251. Гедель показав нездійсненність в цілому програми Гільберта, яка передбачала повну формалізацію істотної частини математики. Вона обмежила саму ідею, яка виходить від робіт Лейбніца, про формалізацію всій раціональної думки у вигляді синтаксичних структур і розумінні мислення як ігри символів безвідносно їх значення. Тому теорема Геделя часто розглядається як досить суворе обгрунтування принципову неможливість повної формалізації наукових міркувань і наукового знання в цілому.

Таким чином, Гедель дав строго логічне обгрунтування нездійсненності ідеї Р. Карнапа про створення єдиного, універсального, формалізованого «фізикалістськи» мови науки. Тобто з геделевской теореми "про неповноту» випливає, що точна формалізована система, яка виступає як мова науки, не може вважатися абсолютно адекватною системі обєктів, бо деякі змістовно істинні пропозиції не можуть бути отримані засобами даного формалізму, а це означає, що формалізація мови науки не знижує, а навпаки, припускає змістовні моменти в побудові мовної системи.

Результати робіт Геделя викликали інтенсивні дослідження обмеженості формальних систем (роботи А. Черча, С. Кліні, Тарського та ін.) Теореми Альфреда Тарського (1902-1984) про формалізації поняття істини для досить багатих формалізованих теорій виявили обмеженість дедуктивних і виразних можливостей формалізмів. Тарський довів внутрішню обмеженість виразних можливостей формалізованих теорій - неможливість строго формальними методами передати все те пізнавальне зміст, який виражається досить багатими змістовними науковими теоріями, що зазнали формалізації. Таким чином, так звані обмежувальні Черча теореми, Тарського і Геделя переконливо показують, що зі складу математики та формальної логіки не можна виключити пропозиції, які через певні змістовних мотивів, не можна не визнати дійсними, але які тим не менш неможливо розвязати на основі правил побудови відповідних формальних систем.

У філософському плані ці теореми означали затвердження принципову неможливість повної формалізації наукового знання. Застосування аксіоматичних і формальних методів дослідження має свої межі.