6.2: Лемма самовідліку

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

Ви неодмінно (!) нагадаємо з розділу 5.9, що у нас є представлена функція\(\text{Num} : \mathbb{N} \rightarrow \mathbb{N}\) така, що\(\text{Num} \left( n \right) = \ulcorner \bar{n} \urcorner\). У нас є\(\Delta\) -формула\(Num \left( x, y \right)\), яка представляє представлене відношення\(\text{Num}\). Ми хотіли б знати, що\(N\) це досить сильний, щоб довести, наприклад,\(\mathcal{L}_{NT}\) -формулу

\[Num \left( \bar{3}, y \right) \leftrightarrow y = \overline{\text{Num} \left( 3 \right)}.\]

Полова: Ви не були збентежені використанням\(\text{Num} \left( 3 \right)\), чи не так? Це може бути заплутаним, оскільки\(\text{Num}\) це набір, і\(\text{Num} \subseteq \mathbb{N}^2\). Але ми знаємо, що\(\text{Num}\) це функція і так річ, яка називається\(\text{Num} \left( 3 \right)\) є унікальним елементом\(y\) codomain\(\mathbb{N}\) такі, що впорядкована пара\(\left( 3, y \right) \in \text{Num}\). Це було очевидно, чи не так?

На жаль, хоча бажання, щоб відображувана еквівалентність була\(N\) доказовою, надзвичайно розумно, ми не можемо цього зробити. Проблема в тому, що\(Num\) наша формула не досить хитра. Лема, яку ми скажемо, дасть цей результат для будь-якої представленої функції, тому ми будемо констатувати її в цій загальності. Однак для наших цілей достатньо буде знати, що це стосується представлених функцій\(\text{Num}\) та\(\text{Sub}\) розділу 5.9.

лема 6.2.1.

Припустимо, що\(\text{R} \subseteq \mathbb{N}^{n+1}\) це представлене множина, представлене (in\(N\)) за допомогою\(\mathcal{L}_{NT}\) -формули\(R\). Якщо\(\text{R}\) є функцією з доменом\(\mathbb{N}^n\) і кодоменом\(\mathbb{N}\), то існує\(Rf\) така формула, що

1. \(Rf\)представляє\(\text{R}\), і
2. для будь-якого\(a_1, \ldots, a_n \in \mathbb{N}\),
   \[N \vdash \left( Rf \left( \bar{a}_1, \ldots, \bar{a}_n, y \right) \leftrightarrow y = \overline{\text{R} \left( a_1, \ldots, a_n \right)} \right).\]

доказ

Щоб поліпшити читабельність, ми припускаємо, що\(n = 1\). Нехай відношення\(\text{R}\) буде функцією з доменом\(\mathbb{N}\), і нехай формула\(Rf\) буде визначена

\[Rf \left( x, y \right) : \equiv R \left( x, y \right) \land \left( \forall i < y \right) \left[ \neg R \left( x, i \right) \right].\]

Спочатку доведемо (1), що\(Rf\) представляє множину\(\text{R}\). Як ми вже знаємо, що\(R\) представляє\(\text{R}\), достатньо, щоб це довести\(N \vdash R \left( \bar{a}, \bar{b} \right) \iff N \vdash Rf \left( \bar{a}, \bar{b} \right)\).

Припустимо, що\(N \vdash Rf \left( \bar{a}, \bar{b} \right)\). Потім ми маємо\(N \vdash R \left( \bar{a}, \bar{b} \right)\) за нашим правилом умовиводу (ПК).

Для зворотного, припустимо, що\(N \vdash R \left( \bar{a}, \bar{b} \right)\). Оскільки\(\text{R}\) це функція, у нас є\(\left( a, i \right) \not\in \text{R}\) для всіх\(i < b\). Таким чином, оскільки\(R\) представляє\(\text{R}\), ми маємо

\[N \vdash \neg R \left( \bar{a}, \bar{0} \right) \land \neg R \left( \bar{a}, \bar{1} \right) \land \ldots \land \neg R \left( \bar{a}, \overline{b-1} \right).\]

За слідством 5.3.12 це означає, що\(N \vdash \left( \forall i < \bar{b} \right) \left[ \neg R \left( x, i \right) \right]\). Тому\(N \vdash Rf \left( \bar{a}, \bar{b} \right)\), встановлюючи (1).

Тепер переходимо до доказу (2). Спочатку ми це доведемо\(N \vdash Rf \left( \bar{a}, y \right) \rightarrow y = \overline{\text{R} \left( a \right)}\). Оскільки\(\text{R}\) є функцією і\(R\) представляє\(\text{R}\), у нас є

\[N \vdash \neg R \left( \bar{a}, \bar{0} \right) \land \ldots \land \neg R \left( \bar{a}, \overline{\text{R} \left( a \right) - 1} \right).\]

(Будьте обережні з гарнітурою там - пам'ятайте різницю між формулою\(R\) і функцією\(\text{R}\).)

Знову ж таки Слідство 5.3.12, у нас є\(N \vdash \left( \forall y < \overline{\text{R} \left( a \right)} \right) \left[ \neg R \left( \bar{a}, y \right) \right]\). Таким чином, ми також маємо

\[N \vdash \left( y < \overline{\text{R} \left( a \right)} \rightarrow \neg R \left( \bar{a}, y \right) \right). \tag{i}\]

За (i) і (ПК), ми маємо

\[N \vdash \left( R \left( \bar{a}, y \right) \rightarrow \neg y < \overline{\text{R} \left( a \right)} \right). \tag{ii}\]

За логічними аксіомами ми знаємо, що

\[N \vdash \left[ \left( \forall i < y \right) \left[ \neg R \left( \bar{a}, i \right) \right] \rightarrow \left( \overline{\text{R} \left( a \right)} < y \rightarrow \neg R \left( \bar{a} \overline{\text{R} \left( a \right)} \right) \right) \right]. \tag{iii}\]

Крім того, оскільки формула\(R\) представляє функцію\(\text{R}\), ми маємо

\[N \vdash R \left( \bar{a}, \overline{\text{R} \left( a \right)} \right). \tag{iv}\]

За (iii), (iv) та (ПК) ми маємо

\[N \vdash \left( \left( \forall i < y \right) \left[ \neg R \left( \bar{a}, i \right) \right] \rightarrow \neg \overline{\text{R} \left( a \right)} < y \right). \tag{v}\]

За (ii), (v) і (ПК) ми маємо

\[N \vdash \left( R \left( \bar{a}, y \right) \land \left( \forall i < y \right) \left[ \neg R \left( \bar{a}, i \right) \right] \right) \rightarrow \left( \neg y < \overline{\text{R} \left( a \right)} \land \neg \overline{\text{R} \left( a \right)} < y \right). \tag{vi}\]

За (vi) і аксіомою N11 ми маємо

\[N \vdash \left( R \left( \bar{a}, y \right) \land \left( \forall i < y \right) \left[ \neg R \left( \bar{a}, i \right) \right] \right) \rightarrow y = \overline{\text{R} \left( a \right)},\]

тобто\(N \vdash \left( Rf \left( \bar{a}, y \right) \rightarrow y = \overline{\text{R} \left( a \right)} \right)\), який встановлює прямий напрямок нашого біумовного.

Щоб завершити доказ (2), нам також потрібно довести, що

\[N \vdash \left( y = \overline{\text{R} \left( a \right)} \rightarrow Rf \left( \bar{a}, y \right) \right).\]

Це залишається для читача як Вправа 1.

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

Лема 6.2.2: Геделя Самопосилання лема

\(\psi \left( v_1 \right)\)Дозволяти бути\(\mathcal{L}_{NT}\) -формула з тільки\(v_1\) безкоштовно. Тоді є пропозиція\(\phi\) таке, що

\[N \vdash \left( \phi \leftrightarrow \psi \left( \overline{ \ulcorner \phi \urcorner} \right) \right).\]

полова: Подивіться, наскільки це акуратно! Ви бачите, як\(\phi\) «говорить» \(\psi\)правда про мене? І ми можемо зробити це для будь-якої формули\(\psi\)! Яка класна ідея!

доказ

Ми явно побудуємо потрібне\(\phi\). Нагадаємо, що в розділі 5.9 ми визначили репрезентабельні функції\(\text{Num} : \mathbb{N} \rightarrow \mathbb{N}\) і\(\text{Sub} : \mathbb{N}^3 \rightarrow \mathbb{N}\) такі, що\(\text{Num} \left( n \right) = \ulcorner \bar{n} \urcorner\) і\(\text{Sub} \left( \ulcorner \alpha \urcorner, \ulcorner x \urcorner, \ulcorner t \urcorner \right) = \ulcorner \alpha_t^x \urcorner\). За Lemma 6.2.1 ми знаємо, що існують формули\(Numf\) і\(Subf\) такі, що

\[\begin{align} N &\vdash \left[ Numf \left( \bar{a}, y \right) \leftrightarrow y = \overline{\text{Num} \left( a \right)} \right], \: \text{and that} \\ N &\vdash \left[ Subf \left( \bar{a}, \bar{b}, \bar{c}, z \right) \leftrightarrow z = \overline{\text{Sub} \left( a, b, c \right)} \right]. \end{align}\]

полова: пам'ятайте,\(\text{Num}\) це функція і\(Numf\) є\(\mathcal{L}_{NT}\) -формула, яка представляє функцію! О, і тільки тому, що нам це потрібно,\(\ulcorner v_1 \urcorner = 8\).

Тепер припустимо,\(\psi \left( v_1 \right)\) що дано, як у твердженні леми. Нехай\(\gamma \left( v_1 \right)\) буде

\[\forall y \forall z \left[ \left[ Numf \left( v_1, y \right) \land Subf \left( v_1, \bar{8}, y, z \right) \right] \rightarrow \psi \left( z \right) \right].\]

Давайте розглянемо\(\gamma \left( n \right)\) трохи уважніше, припустимо, що\(n = \ulcorner \alpha \urcorner\). Якщо попередник\(\gamma \left( n \right)\) тримає, то перша частина попередня говорить нам, що

\ [y =\ текст {Num}\ ліворуч (n\ праворуч) =\ ulcorner\ бар {n}\ urcorner\)

а друга частина попередня стверджує, що

\[\begin{align} z &= \text{Sub} \left( n, 8, \ulcorner \bar{n} \urcorner \right) \\ &= \text{Sub} \left( \ulcorner \alpha \urcorner, \ulcorner v_1 \urcorner, \ulcorner \bar{n} \urcorner \right) \\ &= \ulcorner \alpha_{\bar{n}}^{v_1} \urcorner \\ &= \ulcorner \alpha_{\overline{\ulcorner \alpha \urcorner}}^{v_1} \urcorner. \end{align}\]

Так\(z\) само і число Геделя {\(\alpha\)з числом Ґеделя, яке\(\alpha\) підставляється для\(v_1\)}.

Ще один складний вибір приведе нас туди, куди ми хочемо піти. Нехай\(m = \ulcorner \gamma \left( v_1 \right) \urcorner\), і нехай\(\phi\) буде\(\gamma \left( \bar{m} \right)\). Звичайно,\(\phi\) це речення, тому ми будемо закінчені, якщо зможемо це показати\(N \vdash \phi \leftrightarrow \psi \left( \overline{\ulcorner \phi \urcorner} \right)\).

Давайте спочатку попрацюємо над невеликим розрахунком. Зауважте, що

\[\begin{align} \text{Sub} \left( m, 8, \ulcorner \bar{m} \urcorner \right) &= \text{Sub} \left( \ulcorner \gamma \left( v_1 \right) \urcorner, \ulcorner v_1 \urcorner, \ulcorner \bar{m} \urcorner \right) \\ &= \ulcorner \gamma \left( v_1 \right)_{\bar{m}}^{v_1} \urcorner \\ &= \ulcorner \gamma \left( \bar{m} \right) \urcorner \\ &= \ulcorner \phi \urcorner. \end{align}\]

Маючи це в руці, такі доказово еквівалентні в\(N\):

\[\begin{array}{lr} \phi & \\ \forall y \forall z \left[ Numf \left( \bar{m}, y \right) \rightarrow \left( Subf \left( \bar{m}, \bar{8}, y, z \right) \rightarrow \psi \left( z \right) \right) \right] & \text{logic} \\ \forall y \forall z \left[ y = \overline{\text{Num} \left( m \right)} \rightarrow \left( Subf \left( \bar{m}, \bar{8}, y, z \right) \rightarrow \psi \left( z \right) \right) \right] & \text{Lemma 6.2.1} \\ \forall y \forall z \left[ y = \overline{\ulcorner \bar{m} \urcorner} \rightarrow \left( Subf \left( \bar{m}, \bar{8}, y, z \right) \rightarrow \psi \left( z \right) \right) \right] & \text{calculation} \\ \forall z \left( Subf \left( \bar{m} \bar{8}, \overline{\ulcorner \bar{m} \urcorner}, z \right) \rightarrow \psi \left( z \right) \right) & \text{quantifier rules} \\ \forall z \left( z = \overline{\text{Sub} \left( m, 8, \ulcorner \bar{m} \urcorner \right)} \rightarrow \psi \left( z \right) \right) & \text{Lemma 6.2.1} \\ \forall z \left( z = \overline{\ulcorner \phi \urcorner} \rightarrow \psi \left( z \right) \right) & \text{calculation (6.2.16-19) above} \\ \psi \left( \overline{\ulcorner \phi \urcorner} \right) & \text{quantifier rules} \end{array} \notag\]

Отже\(N \vdash \phi \leftrightarrow \psi \left( \overline{\ulcorner \phi \urcorner} \right)\), в міру необхідності.

Зверніть увагу на цей доказ, що якщо\(\psi\) є a\(\Pi\) -формула,\(\phi\) то логічно еквівалентна a\(\Pi\) -речення. Змінюючи\(\gamma\) трохи, ми також можемо організувати, якщо\(\psi\) це\(\Sigma\) -формула,\(\phi\) логічно еквівалентна\(\Sigma\) -речення.

Вправи

1. Заповніть доказ претензії (2) Лемми 6.2.1, показавши, що
   \[N \vdash \left( y = \overline{\text{R} \left( a \right)} \rightarrow Rf \left( \bar{a}, y \right) \right).\]
2. Доказ Лемми 6.2.1 залежав від використання наслідку Леми Россера, Слідство 5.3.12. Щоб полегшити читання, ми припустили на доказ того\(n = 1\), що значно полегшило використання слідства. Попрацюйте над доказом Лемми 6.2.1, припускаючи\(n = 2\), що, будьте обережні щодо деталей.
3. Припустимо, що\(\psi \left( v_1 \right)\) є\(Formula \left( v_1 \right)\). За Lemma Self-Reference, є\(\phi\) таке речення, що\(N \vdash \left( \phi \leftrightarrow Formula \left( \overline{\ulcorner \phi \urcorner} \right) \right)\). Чи є\(N \vdash \phi\)? Чи є\(N \vdash \neg \phi\)? Обґрунтуйте свою відповідь. Що станеться, якщо ми використовуємо\(\psi \left( v_1 \right) = \neg Formula \left( v_1 \right)\) замість цього?
4. \(\psi \left( v_1 \right)\)Дозволяти бути\(Even \left( v_1 \right)\), і нехай\(\phi\) буде речення, що генерується, коли Lemma Self-Reference застосовується до\(\psi \left( v_1 \right)\). Чи є\(N \vdash phi\)? Чи є\(N \vdash \neg \phi\)? Як ви можете сказати?
5. Покажіть, що доказ самодовідкової леми все ще працює, якщо ми використовуємо Зробіть
   \[\gamma \left( v_1 \right) = \exists y \exists z \left[ Numf \left( v_1, y \right) \land Subf \left( v_1, \bar{8}, y, z \right) \land \psi \left( z \right) \right].\]
   висновок, що якщо\(\psi\) є\(\Sigma\) -формула, то\(\phi\) з самодовідкової леми можна вважати еквівалентним\(\Sigma\) реченню.