(2) m = 626,262,636,223,123,262,111.666,611,223.333,262,636123,262,111,666

     n = 223,333,262,636,123.262,111,666

Легко обнаружить, какая из этих дериваций настоящая, переведя их в традиционную нотацию и произведя стандартный анализ. При этом выясняется:

(1) является ли предполагаемая деривация, кодом которой является m, «законной»;

(2) если это так, то совпадает ли последняя строка деривации со строчкой, кодом которой является n.

Шаг (2) тривиален; шаг (1) тоже довольно прямолинеен, поскольку для него не нужен бесконечный поиск и в нем не спрятаны никакие петли. Вспомните примеры из системы MIU и просто мысленно замените правила MIU и ее аксиому на правила и аксиомы ТГЧ. В обоих случаях алгоритм один и тот же:

Следить за деривацией, переходя от строчки к строчке.

Отмечать строчки, являющиеся аксиомами.

Для каждой строчки, НЕ являющейся аксиомой, проверять, следует ли она из предыдущих строчек предполагаемой деривации.

Если все не-аксиомы следуют по правилам вывода из предыдущих строчек, значит, перед вами — законная деривация; в противном случае, перед вами — фальшивка.

На каждой ступени здесь совершается ограниченное число вполне определенных действий.

Я делаю такой упор на ограниченность петель потому, что, как вы могли догадаться, я собираюсь доказать

ОСНОВНОЙ ФАКТ 1: Свойство пара-доказательности — это примитивно рекурсивное свойство теории чисел; следовательно, оно может быть проверено на программе Блупа.

Необходимо отличать это свойство от его близкого теоретико-численного родственника: свойства числа-теоремы. Если мы говорим, что n — число-теорема, мы имеем в виду. что существует некое число m, такое, что оно составляет с n пару доказательства. (Кстати, это приложимо как к ТТЧ, так и к системе MIU; пожалуй, полезно иметь в виду обе системы, пользуясь MIU как прототипом.) Чтобы проверить, является ли n числом-теоремой, вам придется проверить всех потенциальных пара-доказательных «партнеров» m — и именно тут вы вполне можете запутаться в бесконечной петле. Невозможно определить, сколько вам придется искать, пока вы наткнетесь на число, составляющее пару доказательства с n. Эта проблема возникает во всех системах, сочетающих удлиняющие и укорачивающие правила; подобная комбинация сообщает системе некоторую непредсказуемость.

Нам может пригодиться сейчас пример Вариации Гольдбаха. Проверить является ли пара чисел (m, n) Черепашьей парой нетрудно; это значит, что как m так и n+m должны быть простыми числами. Эта проверка несложна, потому что свойство простоты — примитивно рекурсивно, то есть может быть обнаружено при помощи конечного теста. Но если мы хотим узнать, обладает ли n свойством Черепахи, тогда нам нужно ответить на вопрос «существует ли некое число m, формирующее вместе с n Черепашью пару?» Это снова уводит нас в область неведомого, в страну бесконечной MU-петельности.

Таким образом, из Основного Факта 1 мы можем вывести

ОСНОВНОЙ ФАКТ 2: Свойство формировать пару доказательства может быть проверено на Блупе — следовательно, оно представлено в ТТЧ некоей формулой с двумя свободными переменными.

Как и ранее, мы не упоминаем точно, к какой именно системе относятся данные пары доказательств; оказывается, что это не столь важно, потому что оба Основных Факта действительны для любой формальной системы. Это — общее свойство формальных систем: мы всегда можем определить при помощи предсказуемо конечного теста, является ли данная последовательность строк доказательством, или нет. То же верно и для соответствующих арифметических понятий.

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

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

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

Eа: ПАРА-ДОКАЗАТЕЛЬСТВА-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) показывает то же самое для мета-мета-мета-ТТЧ, и т. д.

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

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

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