Формалізована аксіоматична теорія натуральних чисел

Однак результати К. Геделя початку 30-х р. XX ст. призвели до краху основних надій, що зв'язувалися з цією програмою. К. Гедель показав наступне.

1. Усяка природна, несуперечлива  формалізація S арифметики або будь-якої іншої математичної теорії, яка містить арифметику (напр., теорії множин), неповна і непоповнювана в тому розумінні, що: а) у S містяться (змістовно істинні нерозв'язні формули, тобто такі формули А, що ні А, ні заперечення А не виводимі у S (неповнота формалізованої аріфметики); б) хоч би якою скінченною множиною додаткових аксіом (напр., нерозв'язними в S формулами) розширювати систему S, у новій, посиленій таким чином формальній системі неминуче з'являться свої нерозв’язні формули (непоповнюваність; див. також Геделя теорема про неповноту).

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

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

Усе це ставить певні границі  можливстям А. м. у тому його вигляді, який він набув у рамках гільбертовського формалізму. Однак і в цих границях він відіграв і продовжує відігравати  важливу роль у основах математики. Так, напр., уже після описаних результатів  К. Геделя ним же в 1938-40 рр., а потім П. Коеном у 1963 р. на основі аксіоматичного підходу із застосуванням методу інтерпретацій були отримані фундаментальні результати про сумісність (тобто відносну несуперечливість) і незалежність аксіоми вибору і континуум-гіпотези в теорії множин. Що стосується такого основного питання основ математики, як проблема несуперечливості, і після результатів К. Геделя стало ясно, що для його розв’язування, очевидно, не обійтися без інших, відмінних від фінітистських, засобів та ідей. Тут виявились можливими різні підходи, з огляду на існування різних поглядів на припустимість тих чи інших логичних засобів.

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

 

2. Поняття про формалізовану аксіоматичну теорію натуральних чисел

 

Загальна схема  побудови формальної системи  .

Розглянемо коротко відомості  про формальну систему , яка є формалізованою аксіоматичною теорією натуральних чисел. Формальна система відрізняється від змістовної аксіоматичної теорії натуральних чисел рядом особливостей. По-перше, в явно представлені і використовуються засоби логічних доведень теорем арифметики. По-друге, аксіома індукції в не повністю відповідатиме аксіомі індукції в змістовній аксіоматиці натуральних чисел. Крім того, сам процес побудови теорії має більш формальну, абстрактну (і значно громіздкішу) форму.

Побудову формальної системи  здійснюватимемо засобами мови  L. Для нього в алфавіті  А мови  L здійснимо такі зміни: вилучимо всі предикатні і функціональні символи, замість них введемо один предикатний індивідуальний символ «» («менше»), три індивідуальні символи алгебраїчних операцій: «'» (унарна операція «слідування»), «+» (бінарна операція додавання), «•» (бінарна операція множення), залишимо одну індивідуальну константу «1 ».  В результаті цих змін дістали алфавіт системи .

Далі до множини и    аксіом мови  L приєднуємо множину аксіом Пеано (позначимо її через ) і множину аксіом порядку (позначимо її через ).

Аксіоми Пеано формулюються так, як і в змістовній аксіоматиці, аксіома індукції подається такою  формулою: , де - одномісний предикат.

Аксіоми порядку

або ((x<y)(y<z)⇒(x<z) )

3. ((x<y)
4. .

Таким чином, формальна система    містить 13  логічних аксіом і 15  спеціальних, а саме: 4 аксіоми рівності, 7 аксіом Пеано і 4 аксіоми порядку, разом 28 аксіом. Правила виведення такі самі, що й у мові L.

Приклад доведення  в  системі .

Домовимось про такі позначення. Вираз  «А В» читатимемо:  «А позначає (є назвою для)  В». Наприклад, вираз означає: «буквою F позначаємо формулу ». Символом підстановку елемента  b замість a. В дужках подаватимемо коротке обґрунтування утворених вивідних формул.

Зміст теорем К. Геделя

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

Перш ніж описати зміст  і значення теорем Геделя, розглянемо деякі поняття, які фігурують  у цих теоремах.

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

По-друге, у цих теоремах фігурує поняття формально нерозв’язної формули, тобто такої (як правило, замкненої) формули Ф даної формальної системи, яку засобами цієї системи не можна  ні довести, ні спростувати (тобто, довести ). Якщо засобами даної ф. а. т. можна довести формулу Ф або , то таку формулу називають формально розв’язною (скорочено ф. р. ф.).

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

Ф. а. т. називають формально  повною, якщо кожна її  формула  є ф. р. ф., і формально неповною в противному випадку.

Сформулюємо теореми Геделя. Позначимо через  ф. а. т., яка містить арифметику натуральних чисел.

Теорема (1) .  Якщо , то вона формально неповна.

У 1936 р. американський математик  Д. Б. Россер показав, що в цій теоремі  можна обійтися без поняття .

Теорема (у формі  Россера). Якщо ф. а. т. формально несуперечлива, то вона формально неповна.

Формальна нерозв'язність  якої-небудь формули ф. а. т. не означає, що ця теорія неспроможна виявити (певними  засобами) змістовну істинність чи хибність цієї формули. Наприклад, формула, яку будує Гедель у процесі  доведення теореми (1), формально  нерозв’язна, але змістовно істинна.

Йдеться про те, що не кожне  змістовно істинне твердження, виражене формулою у ф. а. т., може бути в ній  доведене.

Теорема (1) має принципове гносеологічне і методологічне  значення: з неї випливає, що дедуктивні можливості будь-якої досить багатої  ф. а. т. обмежені, зокрема змістовну  арифметику повністю формалізувати  не можна.

Було також доведено, що система аксіом формальної арифметики не поповнювана: якщо до даної системи  аксіом приєднати нерозв’язну (але  змістовно істинну) формулу, то в арифметиці з поповненою системою аксіом знову знайдеться нерозв’язна (і змістовно істинна) формула і т. д.

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

Теорема (2). Якщо ф. а. т. несуперечлива, то довести її несуперечливість засобами, які можна в ній формалізувати, неможливо.

Ця теорема є наслідком  теореми (1) про неповноту. Її іноді  називають теоремою про несуперечливість. З теореми (2) випливає, що довести  несуперечливість формалізованої класичної  математики принципово неможливо, і  план Гільберта щодо обґрунтування  основ математики на шляху повної формалізації аксіоматичного методу не можна повністю реалізувати. З цієї теореми також випливає, що для  доведення несуперечливості системи  формалізованої арифметики треба використати інші засоби, які не можна формалізувати в самій ф, а. т. . Так, німецький математик Г. Генцен у 1936 р., використовуючи так званій метод трансфінітної індукції, довів несуперечливість ф. а. т.. Проте не всі математики визнають це доведення. Згодом аналогічно виконали доведення несуперечливості Аккерман (1940), Лоренц (1951), Шютте (1951), Хлодовський (1959).

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

Аксіома індукції у формальній 1 змістовній теоріях  натуральних чисел. Підсумки.

Система аксіом формалізованої арифметики натуральних чисел (системи ) містить два індивідуальних предикати «=» і «<» і невизначений предикат в аксіомі індукції.

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

Підведемо короткий підсумок про властивості аксіом у змістовній і формалізованій аксіоматичних  теоріях натуральних чисел.

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

З несуперечливості і категоричності змістовної аксіоматичної теорії випливає її повнота в тому розумінні, що всі  істинні твердження інтуїтивної  арифметики можна мати в змістовній аксіоматичній теорії.

Формалізована теорія,  як уже зазначалося раніше, неповна, і провести абсолютне доведення  її несуперечливості принципово неможливо.

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

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

 

1.3. Можливості і межі формалізації

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

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

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

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

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