ГЕДЕЛЬ, ЭШЕР, БАХ: эта бесконечная гирлянда.

Мощь пар доказательства.

Для конкретности предположим, что мы имеем дело с системой MIU. Вы, наверное, помните строчку, которую мы назвали МУМОН'ом. На одном из уровней эта строчка интерпретировалась как утверждение «MU — теорема системы MIU.» Можно показать, как МУМОН выражается в ТТЧ с помощью формулы, выражающей понятие пар доказательства в MIU. Давайте сократим эту формулу, в существовании которой нас уверяет Основной Факт 2, следующим образом:

ПАРА-ДОКАЗАТЕЛЬСТВА-MIU{а, а'}.

Поскольку это — свойство двух чисел, оно представлено формулой с двумя свободными переменными. (В этой главе мы будем пользоваться строгой версией ТТЧ и нам надо будет различать между переменными а, а', а'' и т. д.) Чтобы сказать: «MU — теорема системы MIU», нам придется взять изоморфное высказывание «30 — число-теорема системы MIU» и перевести его в нотацию ТТЧ. Это несложно, если призвать на помощь наше условное сокращение (вспомните главу VIII, в которой, чтобы указать замену каждого а' на, символ числа, слева от этого символа мы писали «/а'»):

Еа: ПАРА-ДОКАЗАТЕЛЬСТВА-MIU{a,SSSSSSSSSSSSSSSSSSSSSSSSSSSSSS0/a'}.

Посчитайте С: их 30 штук. Заметьте, что это — закрытое высказывание ТТЧ, поскольку одна свободная переменная квантифицированна, а другая заменена на символ числа. То, что мы здесь проделали, весьма интересно. Благодаря Основному Факту 2 мы получили возможность говорить о парах доказательства: теперь мы выяснили, как мы можем говорить о числах-теоремах: для этого нужно всего лишь добавить в начале квантор существования! Более точным переводом данной выше строчки было бы «существует некое число а, которое составляет пару доказательства с 30 в качестве второго элемента».

Предположим, что мы захотели бы проделать нечто похожее в ТТЧ — например, выразить высказывание «0=0 — это теорема ТТЧ». Мы можем сократить существующую (согласно Основному Факту 2) формулу аналогичным образом (опять с двумя свободными переменными):

ПАРА-ДОКАЗАТЕЛЬСТВА-ТТЧ{а, а'}.

(Эта сокращенная формула ТТЧ читается так: «Натуральные числа а и а' являются парой доказательства».) Следующим шагом является перевод нашего высказывания в теорию чисел, следуя модели МУМОН. Получается высказывание «существует некое число а, которое составляет пару доказательства с 666,111,666 в качестве второго элемента». Это выражается следующей формулой ТТЧ:

Ea:ПАРА-ДОКАЗАТЕЛЬСТВА-ТТЧ{a, SSSSS … SSSSS0/а'}.

.                                                         |________|

.                                 (Очень много S - целых 666,111.666!).

Это — закрытое высказывание ТТЧ. (Давайте назовем его Джошу — скоро узнаете, почему.) Мы убедились, что возможно говорить не только о примитивно рекурсивном понятии пар доказательства ТТЧ, но и о родственном, хотя и более сложном понятии чисел-теорем ТТЧ.

Чтобы убедиться, насколько хорошо вы поняли эти идеи, попробуйте перевести в ТТЧ следующие высказывания мета-ТТЧ:

(1) 0=0 не является теоремой ТТЧ.

(2) ~0=0 — теорема ТТЧ.

(3) ~0=0 не является теоремой ТТЧ.

Каким образом решения отличаются от примеров, данных выше, и друг от друга? Вот еще несколько упражнений на перевод:

(4) ДЖОШУ — теорема ТТЧ. (Получившуюся строчку ТТЧ назовите МЕТА-ДЖОШУ.).

(5) МЕТА-ДЖОШУ — теорема ТТЧ. (Получившуюся строчку ТТЧ назовите МЕТА-МЕТА-ДЖОШУ.).

(6) МЕТА-МЕТА-ДЖОШУ — теорема ТТЧ.

(7) МЕТА-МЕТА-МЕТА-ДЖОШУ — теорема ТТЧ.

(И т. д., и т. п.).

Пример (5) показывает, что высказывания мета-мета-ТТЧ могут быть переведены в нотацию ТТЧ; пример (6) показывает то же самое для мета-мета-мета-ТТЧ, и т. д.

Важно помнить о разнице между выражением свойства, и его представлением. Например, свойство численно-теоремности ТТЧ выражено следующей формулой:

Еа: ПАРА-ДОКАЗАТЕЛЬСТВА-ТТЧ {а, а'}.

Перевод: «а' — число-теорема ТТЧ». Однако у нас нет гарантии того, что эта формула действительно представляет данное понятие, поскольку у нас нет гарантии того, что это свойство примитивно рекурсивно — на самом деле, у нас есть некоторые основания полагать, что это не так! (Наши подозрения вполне обоснованы. Свойство являться числом-теоремой ТТЧ — НЕ примитивно рекурсивно, и такой формулы ТТЧ, которая могла бы его выразить, не существует!) С другой стороны, свойство являться парой доказательства, являясь примитивно рекурсивным, одновременно выразимо и представимо с помощью формулы, данной выше.