Теоремы Гёделя

[Vladimir Pliassov]

Как, наверное, справедливо было замечено, следовало бы начать с теоремы о полноте, потому что она как будто проще для понимания (до нее тоже надеюсь добраться), но так получилось, что я начал с теоремы о неполноте, и тут, конечно, возникло много вопросов.

1.

Понять, что такое гёделево число довольно просто, поэтому перейдем сразу к тому, что между множеством $\mathbb N$ натуральных чисел и множеством всех строк одной конкретной формальной системы задано взаимно-однозначное соответствие.

Под "строкой" понимается любой набор символов алфавита системы, в том числе терм, атомарная формула, сложная формула, доказательство, целая теория, роман, ресторанный прейскурант и даже случайный, бессмысленный набор символов.

Среди строк, как я понял, есть так называемые правильно составленные -- с этим еще надо разобраться, но во всяком случае, к ним относятся доказательства.

Доказательство это правильно составленное построение (которое и само считается строкой), последней строкой которого является то, что доказывается.

2.

Формулу $F(x)$ (безотносительно к ее гёделеву числу) можно озвучить как "терм $x$ имеет свойство $F$". Свойство может быть любым, например, "быть синим", но применение к формулам и числам этого свойства требует некоторого уровня абстракции, хотя и не исключено.

Свойства "быть четным" и "быть простым" имеют понятный содержательный смысл в отношении чисел, но в отношении формул представляет для нас сейчас мало интереса.

В отношении формул нас в нашем исследовании интересуют такие свойства как "быть истинным/ложным" и "быть доказуемым/ недоказуемым".

В отношении чисел как чисел эти свойства нас здесь не интересуют, но они интересуют нас в том плане, что каждая формула имеет свой (гёделев) номер, который можно считать ее именем, так что если мы скажем что число $s$ имеет свойство "быть недоказуемым", мы -- условно -- можем иметь в виду, что та формула, которая ему сопоставлена, является недоказуемой (но не само это число).

3.

Пусть $W$ это свойство "быть доказуемым". Тогда высказывание "$x$ недоказуемо", или "ни одно $p$ не является доказательством для $x$", в символах запишется как $\forall p \neg W(x,p)$.

Надо сказать, что это высказывание упорно делается для каждого $x$, то есть для каждой строки, и в каких-то случаях оно является истинным, а в каких-то ложным.

4.

Сама формула $\forall p \neg W(x,p)$ имеет гёделев номер, обозначим его $w$. Если подставим его вместо $x$, получим новую формулу $\forall p \neg W(\overline w,p)$ (здесь вместо натурального числа пишется его нумерал $\overline w$).

Эту формулу можно (условно) читать как "формула $\forall p \neg W(x,p)$ недоказуема".

5.

Важно понять, что здесь нет того, чтобы какая-то формула ($\forall p \neg W(x,p)$ или $\forall p \neg W(\overline w,p)$) говорила о себе: "Я недоказуема", это не парадокс лжеца, который сам о себе говорит: "Я лгу". Здесь одна формула, а именно $\forall p \neg W(\overline w,p)$, говорит о другой формуле, а именно о $\forall p \neg W(x,p)$: "Она недоказуема."

6.

То, что о формуле $\forall p \neg W(x,p)$ говорится: "она недоказуема", не может вызывать протеста, так как эта формула представляет собой шаблон, трафарет, формулу со свободной неизвестной. Это то, что у Куратовского, Мостовского в "Теории множеств" называется высказывательной функцией: пока в ней вместо свободной неизвестной не подставлено конкретное значение, она не является высказыванием.

Возьмем трафарет $F(x)=x<0$ ("$x$ имеет свойство быть меньше нуля"). Пусть его гёделев номер равен $f$, тогда имеем высказывание $F(f)=f<0$ (которое, очевидно, ложно, так как $f$ -- натуральное число).

7.

Но теперь возьмем не $\forall p \neg W(x,p)$, а другой трафарет $\forall p \neg W\big(Sub (x),p\big)$. В нем вместо $x$ берется функция $Sub (x)$, которая является ключевой в идее Гёделя.

Эта функция на входе принимает гёделев номер некоторого трафарета (формулы со свободной неизвестной), а на выходе дает гёделев номер формулы, которая получается, если в этом трафарете вместо свободной неизвестной подставить его гёделев номер.

(Иногда вместо функции $Sub (x)$ от одного неизвестного берется функция $Sub (x, y)$, где $y$ это гёделев номер трафарета, а $x$ свободная неизвестная в этом трафарете, но поскольку $x$ и $y$ принимают в доказательстве теоремы одно и то же значение, вместо $Sub (x, y)$ можно брать $Sub (x)$.)

В нашем случае в трафарете $\forall p \neg W\big(Sub (x),p\big)$ вместо $x$ подставим номер этого трафарета -- пусть он будет равен $d$ -- получим формулу $\forall p \neg W\big(Sub (d),p\big)$.

8.

Если не придавать содержательного смысла формуле $\forall p \neg W\big(Sub (d),p\big)$, то ее смысл (формальный) в том, что "для всякого $p$ пара натуральных чисел $\big(Sub (d), p\big)$ обладает свойством $\neg W$".

Если придать этому свойству смысл "быть доказуемым", то получим: "для всякого $p$ число $p$ не является доказательством числа $Sub (d)$". Смысла все еще недостаточно.

Но теперь примем в внимание, что $Sub (d)$ это номер формулы $\forall p \neg W\big(Sub (d),p\big)$, а $p$ это номер ее доказательства (которое, как утверждается в этой же формуле, не существует), то -- условно -- получим следующий содержательный смысл:

формула $\forall p \neg W\big(Sub (d),p\big)$ утверждает собственную недоказуемость (самореференция).

9.

И вот тут начинаются вопросы.

Как сказано, это утверждение предполагает условность, а именно, в формуле $\forall p \neg W\big(Sub (d),p\big)$ мы имеем не саму эту формулу и не ее доказательство, а, соответственно, числа $Sub (d)$ и $p$. Поэтому прямо говорить, что она что-то утверждает о себе, мы не можем (она утверждает, что никакое число $p$ не является доказательством числа $Sub (d)$).

Вот если бы мы, вместо номера этой формулы и номера ее доказательства -- в нарушение правил синтаксиса -- взяли саму формулу и само доказательство, то у нас получилось бы, что она утверждает собственную недоказуемость.

Для этого нам пришлось бы переопределить функцию $Sub (x)$:

пусть она на входе принимает сам шаблон (а не его номер), а на выходе дает саму формулу, которая получается, когда в этом шаблоне вместо $x$ подставляется этот шаблон (а не номер этой формулы).

То есть возьмем формулу $\forall p \neg W\big(Sub (x),p\big)$, в ней вместо $x$ подставим ее саму, получим

$$\forall p \neg W\big(Sub [\forall p \neg W\big(Sub (x),p\big)],p\big)\eqno (1)$$

Учитывая, что $Sub [\forall p \neg W\big(Sub (x), p\big)]$ равно всей формуле (1), имеем

$$\forall p \neg W\Big(\forall p \neg W\big(Sub [\forall p \neg W\big(Sub (x), p\big)], p\big), p\Big)$$

.
Но, учитывая опять-таки, что $Sub [\forall p \neg W\big(Sub (x), p\big)]$ равно всей формуле (1), имеем

$$\forall p \neg W\Bigg(\forall p \neg W\Big(\forall p \neg W\big(Sub [\forall p \neg W\big(Sub (x),p\big)],p\big), p\Big), p\Bigg)$$

Мы видим, что наша формула все разрастается, и конца этому нет.

Кроме того, при этом мы не можем освободиться от "шаблонности": даже если бы мы завершили это бесконечное разрастание формулы, она по-прежнему имела бы в себе свободную переменную $x$. А если бы мы после этого заменили в получившейся бесконечной формуле $x$ на саму эту формулу и снова получили бы бесконечную формулу, в ней так бы и оставалась свободная переменная $x$.

Вообще, когда мы подставляем в шаблон вместо свободной переменной шаблон (пусть даже и не тот же самый), мы снова получаем шаблон. Поэтому говорить о недоказуемости полученной формулы, конечно, можно, но малоинтересно -- потому что то, что шаблон недоказуем, это и так ясно.

10.

Как я понимаю, это разрастание формулы есть проявление парадокса лжеца, это самореференция путем подстановки формул в формулы вместо свободных переменных, и может быть смысл в том, чтобы ее запретить.

Но почему вообще всегда запрещена подстановка формул вместо свободных переменных, даже тогда когда нет самореференции?

В самом деле, возьмем фундаментальный запрет на формулу $F(F(x))$: нельзя в шаблон вместо свободной переменной подставлять формулу, можно только терм (например, число)!

А, собственно, почему? Чтобы избежать парадокса лжеца? Но пусть $L$ это свойство "быть ложным", тогда $L(x)$ это высказывание "$x$ ложно", а $L\big(L(x)\big)$ это высказывание "ложно, что $x$ ложно", а $L\Big(L\big(L(x)\big)\Big)$ это высказывание "ложно, что ложно, что $x$ ложно", то есть мы имеем цепь отрицаний $\neg \neg \neg x$, а не парадокс лжеца $L(x)\leftrightarrow \neg L(x)$, потому что в формуле $L(x)$ нет самореференции.

11.

А есть ли в формуле $\forall p \neg W\big(Sub (d),p\big)$ самореференция? По-моему, нет. Есть то, что, как сказано, условно можно назвать самореференцией: повторюсь, прямо говорить, что она что-то утверждает о себе, мы не можем (она утверждает, что никакое число $p$ не является доказательством числа $Sub (d)$ -- что бы это ни значило).

Настоящая самореференция получается, как показано в п. 9, когда мы в шаблоне $\forall p \neg W\big(Sub (x),p\big)$ (в нарушение правил синтаксиса) попытаемся вместо свободной переменной $x$ подставить сам этот шаблон.

12.

А что есть? Есть две формулы: $\forall p \neg W\big(Sub (d),p\big)$ -- правильно составленная, и $\exists p W\big(Sub (d), p\big)$ -- тоже, по-моему, правильно составленная, и являющаяся отрицанием первой формулы. Ясно, что в одной непротиворечивой формальной системе они не могут сосуществовать. Но почему приоритет отдается первой формуле, а не второй? Почему в формулировке теоремы говорится именно о недоказуемой (хотя и истинной) формуле?

Потому что если система непротиворечива, то первая формула -- которая утверждает свою недоказуемость, -- обязана быть недоказуемой в этой системе? Потому что, если бы она была доказуема, то она была бы ложной (ведь она говорит, что недоказуема)? А в непротиворечивой системе нельзя доказать ложь.

Но, как сказано, она ничего не утверждает о себе, она утверждает, что недоказуемо число $Sub (d)$.

И это еще, если принять, что $W$ это предикат доказуемости. А, может быть, $W$ может быть предикатом чего-нибудь другого (что требует участия $p$, но не в качестве доказательства)?

[warlock66613]

Vladimir Pliassov в сообщении #1732068 писал(а):

В отношении формул нас в нашем исследовании интересуют такие свойства как "быть истинным/ложным" и "быть доказуемым/ недоказуемым".

Таких свойств в теории нет. Утверждение, что некоторая формула является истинной или доказуемой — это утверждение метатеории, а не теории. (Мне показалось что вы уделили недостаточное внимание этому аспекту. Извините если это не так. Но мне показалось, что в вашем тексте вы не выделяете где формулы теории, а где утверждения метатеории (их можно, но не обязательно оформлять формулами), а это важно.)

[mihaild]

Vladimir Pliassov в сообщении #1732068 писал(а):

Пусть $W$ это свойство "быть доказуемым".

Так "быть доказуемым" или "второй аргумент - доказательство первого"?

Vladimir Pliassov в сообщении #1732068 писал(а):

Но почему вообще всегда запрещена подстановка формул вместо свободных переменных, даже тогда когда нет самореференции?

Потому что типы не сходятся. Пусть $F$ - это формула $\forall x: x + 1 = 1+x$, что вообще такое $F+1$?

[epros]

Vladimir Pliassov, из этой длинной простыни очень сложно выцепить, в чём именно заключаются Ваши вопросы. Вас беспокоят какие-то "самореференции" в первой теореме Гёделя о неполноте? Их там нет и не может быть по синтаксическим причинам. Гёделевское недоказуемое предложение $G$ - это всего лишь арифметическая формула, которая утверждает, что не существует некоторого натурального числа. И только метатеория знает, что это число - гёделевский номер доказательства этого самого предложения $G$. Далее идёт метатеоретическое рассуждение: $G \to \neg (\Tau \vdash G)$ (из $G$ следует недоказуемость $G$ в теории $\Tau$). Если теория $\Tau$ непротиворечива, то метатеория может принять всю её аксиоматику и таким образом считать, что все доказываемые ею утверждения - "истинные": $(\Tau \vdash G) \to G$. Из второго и первого следует $(\Tau \vdash G) \to \neg (\Tau \vdash G)$, т.е. предположение о доказуемости $G$ противоречиво, значит $G$ недоказуемо в $\Tau$, значит в метатеории $G$ доказано. Поэтому Гёдель писал о "недоказуемом истинном утверждении". Это, конечно, не совсем точно, потому что истинность определяется интерпретацией языка, которые могут быть разными. Но если считать за "стандартную" такую интерпретацию, в которой А) все аксиомы теории $\Tau$ принимаются за истину и Б) истинно утверждение о непротиворечивости $\Tau$, то так можно сказать.

[Vladimir Pliassov]

warlock66613 в сообщении #1732069 писал(а):

Vladimir Pliassov в сообщении #1732068 писал(а):

В отношении формул нас в нашем исследовании интересуют такие свойства как "быть истинным/ложным" и "быть доказуемым/ недоказуемым".

Таких свойств в теории нет. Утверждение, что некоторая формула является истинной или доказуемой — это утверждение метатеории, а не теории. (Мне показалось что вы уделили недостаточное внимание этому аспекту. Извините если это не так. Но мне показалось, что в вашем тексте вы не выделяете где формулы теории, а где утверждения метатеории (их можно, но не обязательно оформлять формулами), а это важно.)

Нет, вы совершенно правы: я до последнего времени имел смутное представление о том, что вообще есть теория, а есть метатеория, и необходимо их разделять (у меня они смешивались в одну кучу), и спасибо Вам большое за то, что Вы обратили на это мое внимание!

Насчет того, что "утверждения метатеории ... можно, но не обязательно оформлять формулами", мне кажется, что лучше оформлять, чтобы было как можно больше определенности и ясности.

mihaild в сообщении #1732093 писал(а):

Vladimir Pliassov в сообщении #1732068 писал(а):

Пусть $W$ это свойство "быть доказуемым".

Так "быть доказуемым" или "второй аргумент - доказательство первого"?

Вероятно, Вы имеете в виду, что в формуле $W(x,p)$ не хватает квантора, должно быть: $\exists p W(x,p)$?

mihaild в сообщении #1732093 писал(а):

Vladimir Pliassov в сообщении #1732068 писал(а):

Но почему вообще всегда запрещена подстановка формул вместо свободных переменных, даже тогда когда нет самореференции?

Потому что типы не сходятся. Пусть $F$ - это формула $\forall x: x + 1 = 1+x$, что вообще такое $F+1$?

Спасибо! Теперь понял.

epros в сообщении #1732095 писал(а):

Vladimir Pliassov, из этой длинной простыни очень сложно выцепить, в чём именно заключаются Ваши вопросы. Вас беспокоят какие-то "самореференции" в первой теореме Гёделя о неполноте? Их там нет и не может быть по синтаксическим причинам. Гёделевское недоказуемое предложение $G$ - это всего лишь арифметическая формула, которая утверждает, что не существует некоторого натурального числа. И только метатеория знает, что это число - гёделевский номер доказательства этого самого предложения $G$.

Как я понимаю, в формуле $\forall p \neg W\big(Sub (d),p\big)$ нет самореференции, во всяком случае, если ее рассматривать, не раскрывая смысла символа $W$. Тогда она утверждает, что для каждого $p$ числа $Sub (d)$ и $p$ (в означенном порядке) не находятся в отношении $W$ (что бы это ни значило).

Если же раскрыть этот смысл, то получим утверждение: "никакое число $p$ не является доказательством числа $Sub(d)$".

Оба эти утверждения могут принадлежать теории $T$, то есть арифметике (если считать, что она включает в себя логику 1 порядка), хотя оба они абстрактны (не имеют содержательного смысла).

Но вот если мы примем во внимание, что $p$ и $Sub(d)$ это номера формул, и захотим работать не с номерами формул, а с самими формулами, то нам придется перейти из теории $T$ в метатеорию. Потому что в самой теории мы не можем работать с ее формулами (синтаксис не позволяет, а он, как я понимаю, взят не с потолка).

При этом формулы теории будут термами в метатеории, мы сможем о них рассуждать, например, выводить их друг из друга $(\vdash)$, оценивать их истинность ($\vDash$) и, вообще, строить метатеоретические формулы, термами в которых будут формулы теории.

Мы берем метапредикат «выводимо в теории $T$» $(\text {значок}\vdash)$. Он требует на вход два предмета: теорию и формулу. Мы подставляем их и получаем строгую формулу метатеории: $T\vdash A$.

Мы берем метапредикат «истинно на модели» (значок $\vDash $). Он требует на вход модель и формулу. Получаем формулу метатеории: $\mathcal{M} \vDash A$.

При этом в метатеоретических рассуждениях, как я читал, можно употреблять все связки: $\neg, \wedge, \vee, \to$, -- которые используются в теории, но в метатеории, чтобы не путать символы внутри теории и символы снаружи, метатеоретические связки часто пишут обычными словами («не», «и», «следовательно») или используют стрелки другого вида: $\Rightarrow, \Leftrightarrow$.

Я думаю, мой эксперимент в п. 9 первого сообщения темы с подстановкой шаблона $\forall p \neg W\big(Sub (x),p\big)$ в самого себя показал, во всяком случае, одно из оснований, по которому самореференция синтаксически запрещена: формула, которую я попытался получить, стала фрактально разрастаться до бесконечности.

epros в сообщении #1732095 писал(а):

Далее идёт метатеоретическое рассуждение: $G \to \neg (T \vdash G)$ (из $G$ следует недоказуемость $G$ в теории $T$). Если теория $T$ непротиворечива, то метатеория может принять всю её аксиоматику и таким образом считать, что все доказываемые ею утверждения - "истинные": $(T \vdash G) \to G$. Из второго и первого следует $(T \vdash G) \to \neg (T \vdash G)$, т.е. предположение о доказуемости $G$ противоречиво, значит $G$ недоказуемо в $T$, значит в метатеории $G$ доказано. Поэтому Гёдель писал о "недоказуемом истинном утверждении". Это, конечно, не совсем точно, потому что истинность определяется интерпретацией языка, которые могут быть разными. Но если считать за "стандартную" такую интерпретацию, в которой А) всё аксиомы теории $T$ принимаются за истину и Б) истинно утверждение о непротиворечивости $T$, то так можно сказать.

В этом постараюсь еще разобраться.

[epros]

Vladimir Pliassov в сообщении #1732293 писал(а):

Как я понимаю, в формуле $\forall p \neg W\big(Sub (d),p\big)$ нет самореференции, во всяком случае, если ее рассматривать, не раскрывая смысла символа $W$

Вы с самого начала запутались со своими $W$ и $x$, последний является высказыванием, но в то же время каким-то непонятным образом подставляется в качестве аргумента $W$. А потом продолжили путаться с $Sub(x)$, которая тоже непонятно принимает в качестве аргумента то ли число, то ли формулу. Вы уж определитесь, когда имеете дело с формулами теории, а когда с утверждениями метатеории.

Функция подстановки $\text{subst}(x, v, y)$ вычисляет гёделев номер формулы, которая получается, если в формуле с номером $x$ заменить свободную переменную с номером $v$ на терм с номером $y$. Это арифметическая функция (терм), она имеет аргументами три числа и значением - число. Формула $F(x)$ - это $\neg \text{Bew}(\text{subst}(x, v, x))$, где формула $\text{Bew}(x)$ выражает доказуемость формулы с гёделевским номером $x$ (существование конечной последовательности формул, являющейся её доказательством). Это всё арифметические формулы, никакие формулы в качестве их аргументов подставляться не могут. Берём гёделев номер этой формулы $n = \ulcorner F(x) \urcorner$ и подставляем его вместо аргумента $x$ самой формулы $F(x)$, в итоге и получаем это самое $G$.

Vladimir Pliassov в сообщении #1732293 писал(а):

При этом в метатеоретических рассуждениях, как я читал, можно употреблять все связки: $\neg, \wedge, \vee, \to$, -- которые используются в теории

Это потому что метатеория использует ту же самую логику. Если Вы путаетесь с тем, где логическая связка употреблена как часть синтаксиса метаформулы, а где - как часть синтаксиса формулы рассматриваемой теории $\Tau$, то можете в метатеории пользоваться только словами естественного языка. Но вообще-то обычно это всегда понятно.

Vladimir Pliassov в сообщении #1732293 писал(а):

одно из оснований, по которому самореференция синтаксически запрещена: формула, которую я попытался получить, стала фрактально разрастаться до бесконечности.

Самореференция не как-то специально "запрещена" из-за "разрастания до бесконечности", она просто изначально синтаксически невозможна, потому что нельзя в качестве аргумента формулы подставить формулу. Это на естественном языке можно сказать: "В этом утверждении я лгу", но формализовать это утверждение синтаксически невозможно, потому что невозможно сформулировать, что такое "это утверждение".

[Vladimir Pliassov]

epros в сообщении #1732302 писал(а):

Самореференция не как-то специально "запрещена" из-за "разрастания до бесконечности", она просто изначально синтаксически невозможна, потому что нельзя в качестве аргумента формулы подставить формулу. Это в естественном языке можно сказать: "В этом утверждении я лгу", но формализовать это утверждение синтаксически невозможно, потому что невозможно сформулировать, что такое "это утверждение".

Я об этом думал -- о том, что в предложении "Я лгу" нет информации, о чем я лгу.

Это незавершенная языковая конструкция $L(x)$, в ней есть подлежащее и сказуемое, но нет необходимого в ее контексте дополнения, и она вследствие своей незавершенности не имеет того содержательного смысла, который может получить, если ее завершить.

Это высказывательная функция, которая превратится в высказывание, только когда в ней вместо $x$ будет подставлено его значение, например, "этот камень твердый": "Я лгу, что этот камень твердый (это халва)."

Поэтому, как мне кажется, фраза "Я лгу" не является парадоксом. Она считается парадоксом по недоразумению. Этой незавершенной конструкции $L(x)$ почему-то приписывается, будто бы в ней вместо $x$ подставлена она сама, затем в полученной конструкции снова вместо $x$ подставлена она сама и так далее, в результате чего получается бесконечный фрактал (бесконечная матрешка) $L(L(L(\dots)))$ ("Я лгу, что я лгу, что я лгу ...")

Но, как сказано, эта конструкция не завершена -- в ней вместо $x$ ничего не подставлено.

Если же говорить о самом по себе бесконечном фрактале "Я лгу, что я лгу, что я лгу ...", то он не является парадоксом, это просто бесконечная последовательность отрицаний: $\neg \neg \neg \dots $ , не создающая выражения вида $A \leftrightarrow \neg A$, поскольку, если мы начнем с $A$, то до последнего $\neg A$ не доберемся никогда.

[epros]

Vladimir Pliassov в сообщении #1733766 писал(а):

бесконечный фрактал (бесконечная матрешка) $L(L(L(\dots)))$

Vladimir Pliassov в сообщении #1733766 писал(а):

бесконечная последовательность отрицаний: $\neg \neg \neg \dots $

Ничего этого в формальном синтаксисе нет. Предложение - это конечная строка. Если это предложение метаязыка, то оно может говорить что-то о предложении предметного языка, но ни при каких условиях оно не может говорить что-то о самом себе. Это не случайно так придумали, а как раз чтобы аналитическая грамматика при распознавании предложения не попадала в бесконечную рекурсию. Т.е. требование к формальной грамматике - общерекурсивность. Неограниченные грамматики (по классификации Хомского) теоретически могут быть частично рекурсивными, но на практике таковыми никто не пользуется.