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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

[[Категорія:Статті, що потребують вичитки з грудня 2015]]

Теорема Геделя про неповноту і друга теорема Геделя [~ 1] — дві теореми математичної логіки про принципові обмеженнях формальної арифметики і, як наслідок, всякої формальної системи, в якій можна визначити основні арифметичні поняття: натуральні числа, 0, 1, додавання і множення.

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

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

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

Теорема Геделя про неповноту[ред.ред. код]

У початковій формі[ред.ред. код]

У своїй формулюванні теореми про неповноту Гедель використовував поняття ω-несуперечливої ​​формальної системи — більш сильна умова, ніж просто несуперечливість. Формальна система називається ω-несуперечливою​​, якщо для всякої формули 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 ціною збільшення кількості змінних.

Начерк докази[ред.ред. код]

У своїй статті Гедель дає начерк основних ідей докази[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' 'є аналогом парадоксу брехуна. Міркування Геделя в цілому дуже схожі на парадокс Рішара. Більше того, для доказу існування невиводимість тверджень може бути використаний будь семантичний парадокс[18].

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

Друга теорема Геделя[ред.ред. код]

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

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

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

Начерк докази[ред.ред. код]

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

Історичні відомості[ред.ред. код]

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

Примітки[ред.ред. код]

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

Джерела[ред.ред. код]

  1. Кліні 1957 с.513
  2. чл.-кор. РАН Лев Дмитрович Беклемішев в «Запровадження в математичну логіку»
  3. Тлумачний словник з обчислювальних систем - Page 205
  4. Доповіді Академії наук СРСР, Volume 262 - Page 799 (1982)
  5. Известия Академії наук СРСР, Volume 50 - Page 1 140 (1986)
  6. а б Кліні 1957 с.187
  7. Мендельсон 1 971 с.165
  8. Це міркування запозичене з Мендельсон тисячі дев'ятсот сімдесят одна с.160
  9. Див., Наприклад, Кліні тисяча дев'ятсот п'ятьдесят сім с.188
  10. Мендельсон 1971 с.162
  11. Мендельсон тисяча дев'ятсот сімдесят одна с.162-163
  12. Мендельсон 1971 с.176
  13. Jones JP, Undecidable diophantine equations
  14. Martin Davis, Diophantine Equations & Computation
  15. Martin Davis, The Incompleteness Theorem
  16. /gram6.htm#glava65 К. Поднієкс, Теорема Геделя в Диофантова формі
  17. Gödel, Kurt. On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I. — 1931. в книзі Davis, Martin (ed.) {{{Заголовок}}}. — New York : Raven Press, тисяча дев'ятсот шістьдесят п'ять. — С. 6-8.
  18. а б Гедель 1931
  19. Heijenoort +1967 p.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, ed., 1986. Kurt Gödel Collected works, Vol. I . Oxford University Press: 144—195.

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

Див. також[ред.ред. код]