Властивості формальних теорій

 

Означення14.11. Інтерпретація формальної теорії S в області інтерпретації M називається функція I: S ® M, яка кожній формулі формальної системи S однозначно зіставляє деяк змістовне висловлювання відносно об’ єктів множини M. Це висловлювання може бути істинним або хибним (або не мати значення істинності). Якщо відповідне висловлювання є істинним, то кажуть, що формула виконується в даній інтерпретації.

 

Означення14.12. Інтерпретація I називається моделлю множини формул N, якщо всі формули цієї множини виконуються в інтерпретації I. Інтерпретація I називається моделлю формальної теорії S, якщо всі теореми цієї теорії виконуються в інтерпретації I (тобто всі формули що виводяться є істинними в даній інтерпретації).

 

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

 

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

 

Таким чином, формальна теорія підходить для опису тих множин, які є її моделями. Модель для формальної теорії S існує тоді й тільки тоді, коли S семантично несуперечлива.

 

Означення14.14. Формальна теорія S називається формально несуперечливою, якщо в ній не виводяться одночасно формули A та Ø A. Теорія S формально несуперечлива тоді й тільки тоді, коли вона семантично несуперечлива.

 

Означення14.15. Нехай множина M є моделлю формальної теорії S. Формальна теорія S називаєтьсяповною(абоадекватною),якщо кожному істинному висловлюванню M відповідає теорема теорії S.

 

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

 

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

 

Означення14.16. Якщо для множини M існує формальна повна несуперечлива теорія S, то M називається такою, що формалізується.

 

Означення14.17. Система аксіом формально несуперечливої теорії S називається незалежною, якщо жодна з аксіом не виводиться з решти за правилами виведення теорії S.

 

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

 

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

 

Етап формально-аксіоматичного обґрунтування. Геометричні дослідження, розпочаті Лобачевським, привели до того, що на початку ХХ ст. було сформульоване фундаментальне поняття сучасної математики – поняття (математичного або геометричного) простору як деякої сукупності однорідних об’єктів довільної природи (точок, векторів, фігур, функцій, явищ, станів і т.п.), взаємні відношення між якими задовольняють тій чи іншій системі аксіом. Фактично, різні математичні простори є моделями тих чи інших аксіоматичних теорій, побудованих на відповідних системах аксіом. Таке розуміння дозволило геометричним ідеям проникнути у різні галузі математики, фізики та інших наук. При цьому і сама геометрія стала розгалужуватись все ширше, математика ставала все більше єдиною наукою, а межі її різноманітних галузей, в тому числі і геометрії, ставали все менш чіткими. Цементним розчином, який з’єднував міцними зв’язками основи всіх галузей математики, була в ХХ ст. математична логіка. З її допомогою був досліджений сам процес доведення, процес виведення теорем з аксіом. Тим самим аксіоматичний метод одержав подальший свій розвиток і досяг в певному розумінні вершини. Аксіоматичні теорії стали точними математичними об’єктами, названими формальними системами, і почали вивчатись математичними методами (методами математичної логіки), почала будуватись теорія таких математичних теорій (теорія формальних систем), що називається метатеорією. Цей напрям був розпочатий в роботах Гільберта і одержав назву методу формалізації в обґрунтуванні математики. В рамках метатеорії геометрії були доведені несуперечливість, категоричність, повнота аксіоматичної теорії евклідової геометрії, а також неевклідових геометрій. Можна сказати, що в ХХ ст. відбувся третій етап розвитку аксіоматичного обґрунтування геометрії і розвитку аксіоматичного методу взагалі – етап формально-аксіоматичного обґрун тування.

 

Теорема Гьоделя про неповноту будь-якої формальної аксіоматичної теорії.

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

У своїй формулюванні теореми про неповноту Гедель використовував поняття ω-несуперечливої ​​формальної системи — більш сильне умова, ніж просто несуперечливість.

Формальна система називається ω-несуперечливої ​​, якщо для всякої формули A (x) цієї системи неможливо одночасно вивести формули А ('0'), А ('1'), А ('2'), … і ∃x A (x) (іншими словами, з того, що для кожного натурального числа n виведена формула A ('n'), слід невиводимість формули ∃x A (x)).

Легко показати, що ω-несуперечність тягне просту несуперечність (тобто, будь-яка ω-несуперечлива формальна система несуперечлива).

 

У процесі доведення теореми будується така формула A арифметичної формальної системи S, що:

Якщо формальна система S несуперечлива, то формула A невиведені в S;

якщо система S ω-несуперечлива, то формула A невиведені в S. Таким чином, якщо система S ω-несуперечлива, то вона неповна[~ 2] і A служить прикладом нерозв'язною формули.

 

Формулу A іноді називають гёделевой нерозв'язною формулою

 

Інтерпретація нерозв'язною формули

 

У стандартній інтерпретації[~ 3] формула A означає «не існує виведення формули A», тобто стверджує свою власну невиводимість в S. Отже, по теоремі Геделя, якщо тільки система S несуперечлива, то ця формула і справді невиведені в S і тому істинна в стандартній інтерпретації. Таким чином, для натуральних чисел формула A вірна, але в S невиведені.

У формі Россера

 

У процесі доведення теореми будується така формула B арифметичної формальної системи S, що:

Якщо формальна система S несуперечлива, то в ній невиведені обидві формули B і B; інакше кажучи, якщо система S несуперечлива, то вона неповна[~ 2], і B служить прикладом нерозв'язною формули.

 

Формулу B іноді називають россеровой нерозв'язною формулою. Ця формула трохи складніше гёделевой.

 

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

Всяка досить сильна рекурсивно аксіоматізіруемая несуперечлива теорія першого порядку неповна.

 

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

 

 

Саме формулювання теореми:

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