Перейти до вмісту

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

Матеріал з Вікіпедії — вільної енциклопедії.

Теорема Геделя про неповноту і друга теорема Геделя[~ 1] (англ. Gödel's incompleteness theorems) — дві теореми математичної логіки про принципові обмеження формальної арифметики і, як наслідок, будь-якої формальної системи, в якій можливо визначити основні арифметичні поняття: натуральні числа, 0, 1, додавання та множення.

Перша теорема стверджує, що, якщо формальна арифметика є несуперечливою, то в ній існує невивідна і неспростовна формула.

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

Обидві ці теореми було доведено Куртом Геделем 1930 року (опубліковано 1931 року), вони мають безпосередній стосунок до другої проблеми[en] зі знаменитого списку Гільберта.

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

[ред. | ред. код]

У початковій формі

[ред. | ред. код]

У своєму формулюванні теореми про неповноту Гедель використовував поняття ω-несуперечливої формальної системи — сильніша умова, ніж просто несуперечливість. Формальна система називається ω-несуперечливою, якщо для будь-якої формули A(x) цієї системи неможливо одночасно вивести формули А(0), А(1), А(2), … і ∃x¬A(x) (іншими словами, з того, що для кожного натурального числа n виведено формулу A(n), випливає невивідність формули ∃x ¬A(x)). Легко показати, що ω-несуперечливість спричиняє просту несуперечливість (тобто, будь-яка ω-несуперечлива формальна система є несуперечливою)[6].

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

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

Формулу A іноді називають геделевою нерозв'язною формулою[7].

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

[ред. | ред. код]

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

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

[ред. | ред. код]

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

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

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

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

[ред. | ред. код]

В стандартній інтерпретації[~ 3] формула B означає «якщо існує виведення формули B, то існує виведення формули ¬B». Згідно ж теореми Геделя у формі Россера, якщо формальна система S є несуперечливою, то формула B в ній є невивідною; тому, якщо система S є несуперечливою, то формула B є правильною в стандартній інтерпретації[11].

Узагальнені формулювання

[ред. | ред. код]

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

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

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

Поліноміальна форма

[ред. | ред. код]

Після того, як Юрій Матіясевіч довів діофантовість будь-якої ефективно зліченної множини і було знайдено приклади універсальних діофантових рівнянь, з'явилася можливість сформулювати теорему про неповноту в поліноміальному (або діофантовому) вигляді[13][14][15][16]:

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

Степінь даного рівняння можливо знизити до 4 ціною збільшення кількості змінних.

Начерк доведення

[ред. | ред. код]

Детальніші відомості з цієї теми ви можете знайти в статті Начерк доведення першої теореми Геделя про неповноту[en].

У своїй статті Гедель дає начерк основних ідей доведення[17], який наведено нижче з незначними змінами.

Кожному примітивному символові, виразу і послідовності виразів деякої формальної системи[~ 4] S поставмо у відповідність певне натуральне число[~ 5]. Математичні поняття і твердження таким чином стають поняттями і твердженнями про натуральні числа, і, отже, їх самі може бути виражено в символізмі системи S. Можливо показати, зокрема, що поняття «формула», «виведення», «вивідна формула» може бути визначено всередині системи S, тобто можливо відновити, наприклад, формулу F(v) в S з однієї вільної натурально-числової змінної v таку, що F(v), в інтуїтивній інтерпретації, означає: v — вивідна формула. Тепер побудуймо нерозв'язне речення системи S, тобто речення A, для якого ані A, ані не-A невивідні, таким чином:

Формулу в S з рівно однією вільної натурально-числовою змінною назвімо клас-виразом. Впорядкуймо клас-вирази в послідовність будь-яким чином, позначмо n-й через R(n), і зауважмо, що поняття «клас-вираз», також як і відношення впорядкування R, можливо визначити в системі S. Нехай α — довільний клас-вираз; через [α;n] позначмо формулу, яка утворюється з клас-виразу α заміною вільної змінної символом натурального числа n. Тернарне відношення x = [y;z] теж виявляється визначним в S. Тепер визначмо клас K натуральних чисел таким чином:

NK ≡ ¬Bew [R(n);n]    (*)

де Bew x означає: x — вивідна формула[~ 6]. Оскільки всі визначальні поняття з цього визначення можливо виразити в S, то це ж правильно і для поняття K, яке з них побудовано, тобто є такий клас-вираз C, що формула [C;n], інтуїтивно інтерпретована, позначає, що натуральне число n належить K. Як клас-вираз, C ідентичний деякому певному R(q) в нашій нумерації, тобто

C=R(q)

виконується для деякого певного натурального числа q. Тепер покажімо, що речення [R(q);q] нерозв'язне в S. Так, якщо припускається, що речення [R(q);q] є вивідним, то воно виявляється істинним, тобто, відповідно до сказаного вище, q буде належати K, тобто, відповідно до (*), буде виконано ¬Bew [R(q);q], що суперечить нашому припущенню. З іншого боку, якщо припустити вивідність заперечення [R(q);q], то матиме місце ¬qK, тобто Bew[R(q);q] буде істинним. Отже, [R(q);q] разом зі своїм запереченням буде вивідним, що знову є неможливим.

Зв'язок з парадоксами

[ред. | ред. код]

В стандартній інтерпретації[~ 3] геделева нерозв'язна формула A означає «не існує виведення формули A», тобто стверджує свою власну невивідність в системі S. Таким чином, A є аналогом парадоксу брехуна. Міркування Геделя в цілому дуже схожі на парадокс Рішара[en]. Більше того, для доведення існування невивідності тверджень може бути використано будь-який семантичний парадокс[17].

Слід зазначити, що виражене формулою A твердження не містить порочного кола, оскільки спочатку стверджується тільки те, що деяка конкретна формула, явний запис якої отримати нескладно (хоч і громіздко), є недовідною. «Тільки згодом (і, так би мовити, з волі випадку) виявляється, що ця формула — саме та, якою виражено саме це твердження»[17].

Друга теорема Геделя

[ред. | ред. код]

У формальній арифметиці S можливо побудувати таку формулу, яка в стандартній інтерпретації[~ 3] є істинною в тому і тільки в тому випадку, коли теорія S є несуперечливою. Для цієї формули виконується твердження другої теореми Геделя:

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

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

Начерк доведення

[ред. | ред. код]

Спочатку будується формула Con, яка змістовно виражає неможливість виведення в теорії S якоїсь формули разом з її запереченням. Тоді твердження першої теореми Геделя виражається формулою ConG, де G — геделева нерозв'язна формула. Всі міркування для доведення першої теореми може бути виражено і проведено засобами S, тобто в S є вивідною формула ConG. Звідси, якщо в S є вивідною Con, то в ній є вивідною й G. Проте, згідно першої теореми Геделя, якщо S є несуперечливою, то G в ній є невивідною. Отже, якщо S є несуперечливою, то в ній є невивідною й формула Con.

Історичні відомості

[ред. | ред. код]

23 жовтня 1930 року результати Геделя було представлено Віденській академії наук Гансом Ганом. Основну статтю було отримано для публікації 17 листопада 1930 року і опубліковано на початку 1931 року[18].

Примітки

[ред. | ред. код]
  1. Іноді згадується як друга теорема Геделя «про доведення несуперечливості»[1], «про неповноту»[2][3][4], «про неповноту арифметики»[5].
  2. а б Формальна система, що містить нерозв'язну, тобто невивідну і неспростовну формулу, називається неповною.
  3. а б в г Інтерпретація формул теорії S називається стандартною, якщо її областю є множина невід'ємних цілих чисел, символ 0 інтерпретується числом 0, функціональні символи ', +, • інтерпретуються додаванням одиниці, додаванням і множенням відповідно, предикатний символ = інтерпретується відношенням тотожності.
  4. Гедель використовував систему Principia Mathematica Уайтхеда і Рассела із застереженням, що міркування застосовні до широкого класу формальних систем
  5. Подібне зіставлення формул і натуральних чисел називається арифметизацією математики, її було здійснено Геделем вперше. Ця ідея згодом стала ключем до розв'язання багатьох важливих задач математичної логіки. Див. Геделева нумерація
  6. «Bew» — скор. від нім. Beweisbar — доказовий, вивідний

Джерела

[ред. | ред. код]
  1. Кліні, 1957, с. 513.
  2. чл.-корр. РАН Лев Дмитриевич Беклемишев в «Введении в математическую логику» [Архівовано 21 березня 2009 у Wayback Machine.] (рос.)
  3. Толковый словарь по вычислительным системам. — Машиностроение, 1991. — 560 с. — ISBN 5-217-00617-X., стор. 205 (рос.)
  4. Доклады Академии наук СССР. 262: 799. 1982. {{cite journal}}: Пропущений або порожній |title= (довідка) (рос.)
  5. Известия Академии наук СССР. 50: 1140. 1986. {{cite journal}}: Пропущений або порожній |title= (довідка) (рос.)
  6. а б Кліні, 1957.
  7. Мендельсон, 1971, с. 165.
  8. Це міркування запозичено з Мендельсон, 1971, с. 160
  9. Див., наприклад, Кліні, 1957, с. 188
  10. Мендельсон, 1971, с. 162.
  11. Мендельсон, 1971, с. 162-163.
  12. Мендельсон, 1971, с. 176.
  13. Jones JP, Undecidable diophantine equations (англ.)
  14. Martin Davis, Diophantine Equations & Computation [Архівовано 24 травня 2010 у Wayback Machine.] (англ.)
  15. Martin Davis, The Incompleteness Theorem [Архівовано 4 березня 2016 у Wayback Machine.] (англ.)
  16. К. Подниекс, Теорема Геделя в диофантовой форме [Архівовано 10 вересня 2017 у Wayback Machine.] (рос.)
  17. а б в Гедель, 1931.
  18. Heijenoort, 1967, с. 592.

Література

[ред. | ред. код]

Бібліографія — статті Геделя

[ред. | ред. код]
  • 1931 Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173—198.
  • 1931 Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. and On formally undecidable propositions of Principia Mathematica and related systems I in Solomon Feferman[en], ed., 1986. Kurt Gödel Collected works, Vol. I. Oxford University Press: 144—195.

Оригінальний німецький текст з паралельним англійським перекладом, з елементарним введенням, написаним Стівеном Кліні.

  • +1951, Some basic theorems on the foundations of mathematics and their implications in Solomon Feferman[en], ed., 1995. Kurt Gödel Collected works, Vol. III. Oxford University Press: 304—323.

Див. також

[ред. | ред. код]