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

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

${\displaystyle {\begin{aligned}&(elg^{2}+\alpha -(b-xy)q^{2})^{2}+(q-b^{5^{60}})^{2}+(\lambda +q^{4}-1-\lambda b^{5})^{2}+\\&(\theta +2z-b^{5})^{2}+(u+t\theta -l)^{2}+(y+m\theta -e)^{2}+(n-q^{16})^{2}+\\&((g+eq^{3}+lq^{5}+(2(e-z\lambda )(1+xb^{5}+g)^{4}+\lambda b^{5}+\lambda b^{5}q^{4})q^{4})(n^{2}-n)+\\&(q^{3}-bl+l+\theta \lambda q^{3}+(b^{5}-2)q^{5})(n^{2}-1)-r)^{2}+\\&(p-2ws^{2}r^{2}n^{2})^{2}+(p^{2}k^{2}-k^{2}+1-\tau ^{2})^{2}+\\&(4(c-ksn^{2})^{2}+\eta -k^{2})^{2}+(r+1+hp-h-k)^{2}+\\&(a-(wn^{2}+1)rsn^{2})^{2}+(2r+1+\phi -c)^{2}+\\&(bw+ca-2c+4\alpha \gamma -5\gamma -d)^{2}+\\&((a^{2}-1)c^{2}+1-d^{2})^{2}+((a^{2}-1)i^{2}c^{4}+1-f^{2})^{2}+\\&(((a+f^{2}(d^{2}-a))^{2}-1)(2r+1+jc)^{2}+1-(d+of)^{2})^{2}+\\&(((z+u+y)^{2}+u)^{2}+y-K)^{2}=0\end{aligned}}}$

не має розв'язків у невід'ємних цілих числах, але цей факт не може бути доведено в теорії 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 натуральних чисел таким чином:

N∈K ≡ ¬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], то матиме місце ¬q∈K, тобто Bew[R(q);q] буде істинним. Отже, [R(q);q] разом зі своїм запереченням буде вивідним, що знову є неможливим.

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

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

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