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

У Вікіпедії є статті про інші значення цього терміна: Теореми Геделя.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Кожному примітивному символові, виразу і послідовності виразів деякої формальної системи S поставмо у відповідність певне натуральне число. Математичні поняття і твердження таким чином стають поняттями і твердженнями про натуральні числа, і, отже, їх самі може бути виражено в символізмі системи 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 натуральних чисел таким чином:

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

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

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

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

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

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

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

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

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

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

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

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

Примітки

1. Іноді згадується як друга теорема Геделя «про доведення несуперечливості», «про неповноту», «про неповноту арифметики».
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.  (рос.)
5. Известия Академии наук СССР 50: 1140. 1986.  (рос.)
6. Кліні, 1957, с. 187.
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.

Література

• Gödel Kurt. On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I. — 1931. в книзі Davis, Martin (ed.). The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. — New York : Raven Press, 1965. — С. 6-8. (англ.)
• Kleene, Stephen Cole (1952). Introduction to Metamathematics. New York - Toronto: D. van Nostrand Company, Inc.  (англ.)
  • Клини Стефен Коул. Введение в метаматематику. — Москва : «Издательство иностранной литературы», 1957. — 526 с. (рос.)
• Kleene, Stephen Cole (1967). Mathematical Logic. New York - London - Sydney: John Wiley & Sons, Inc.  (англ.)
  • Клини Стефен Коул. Математическая логика. — Москва : «Мир», 1973. — 480 с. (рос.)
• Mendelson, Elliott (1964). Introduction to Mathematical Logic. van Nostrand.  (англ.)
  • Мендельсон Эллиот. Введение в математическую логику. — Москва : «Наука», 1971. — 320 с. (рос.)
• Davis, Martin (ed.). The Undecidable: Basic Papers On Undecidable Propositions, Unsolvable Problems And Computable Functions. — New York : Raven Press, 1965. — 440 с. (англ.)
• Heijenoort, Jean van (ed.). From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931. — Cambridge, Massachusetts : Harvard University Press, 1967. — 660 с. (англ.)
• В. А. Успенский^[ru]. Теорема Гёделя о неполноте. — Москва : Наука, 1982. — 110 с. (рос.)
• Академик Ю. Л. Ершов^[ru] , программа А. Гордона от 16 июня 2003 года (рос.)
• А. Б. Сосинский. Теорема Геделя // летняя школа «Современная математика». — Дубна, 2006. (рос.)
• П. Дж. Коэн. Об основаниях теории множеств // Успехи математических наук. — 1974. — Т. 29, № 5(179). — С. 169–176. — MR386990. (рос.)
• М. Кордонский. Конец истины. — ISBN 5-946448-001-04. (рос.)
• В. А. Успенский^[ru]. Теорема Гёделя о неполноте и четыре дороги, ведущие к ней // летняя школа «Современная математика». — Дубна, 2007. (рос.)
• Ершов Ю.Л.^[ru], Палютин Е.А. Математическая логика. — Москва : Наука, 1987. — 336 с. (рос.)
• Бирюков Б.В.^[ru], Тростников В. Н. Жар холодных чисел и пафос бесстрастной логики. Формализация мышления от античных времен до эпохи кибернетики. — Москва : Едиториал УРСС, 2004. — 232 с. — ISBN 5-354-00310-5. (рос.)

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

• 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.

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

• Hirzel, Martin, +2000, On formally undecidable propositions of Principia Mathematica and related systems I. [ 16 вересня 2004 у Wayback Machine.]. Сучасний переклад Марина Херцеля.

• +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.

Див. також

• Теорема Геделя про повноту
• Парадокс брехуна
• Недовідні твердження
• Теорема Льоба
• Теорема Тарського про невиразимість істини^[en]
• Теорема Хайтіна про неповноту^[en]
• Натуральні числа
• Формальна теорія
• Теорема Гудштейна
• Антиномія
• Му (заперечення)^[en]
• Gödel, Escher, Bach
• Непредикативність (математика)