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

Так или иначе, величины m = 31311311130, и n = 30, безусловно, не являются парой доказательства MIU. Само по себе, это еще не означает, что 30 — не номер MIU. Могло бы найтись другое число, составляющее пару доказательства с 30. (На самом деле, мы уже выяснили ранее, что 30 — не теорема MIU. Следовательно, ни одно число не может составлять пару доказательства с 30.)

А как насчет пар доказательства в ТТЧ? Я приведу вам два параллельных примера, лишь один из которых является действительной парой доказательства. Можете ли вы определить, какой именно? (Кстати, именно здесь появляется кодон «611», функция которого — отделять Гёделевы номера последующих строк в деривации ТТЧ. В этом смысле, «611» служит в качестве знака препинания. В системе MIU эту роль выполняет начальное «3» каждой строки; там не нужна никакая дополнительная пунктуация.)

1) m = 626,262,636,223,123.262,111,666,611,223,123,666,111,666

n = 123,666,111,666

(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) формулу аналогичным образом (опять с двумя свободными переменными):