Гёдель, Эшер, Бах. Эта бесконечная гирлянда

Вернемся к Крабу и к вопросу о том, совместима ли с реальностью его разрешающая процедура, устанавливающая теоремность (представленная в виде фильтра музыкальной красоты). На самом деле, из событий Диалога мы не можем с уверенностью заключить, является ли дар Краба способностью отличать теоремы от не-теорем, или же способностью отличать истинные высказывания от ложных. Разумеется, во многих случаях это одно и то же, но Теорема Геделя показывает, что так бывает не всегда. Однако это не так уж важно, поскольку, если вы принимаете Версию ИИ Тезиса Ч-Т, ни одна из этих альтернатив невозможна. Утверждение, что ни в какой формальной системе не существует разрешающей процедуры, способной отличать теоремы от не-теорем называется Теоремой Черна. Утверждение, что ни в какой формальной  системе не существует разрешающей процедуры для Истины ТТЧ — если таковая существует, в чем легко начать сомневаться после рассмотрения всех разветвлений ТТЧ, — следует из Теоремы Тарского (опубликованной в 1933 году, хотя Тарский был знаком с подобными идеями значительно раньше).

Доказательства этих двух важных результатов метаматематики весьма схожи. Оба вытекают из автореферентных построений. Давайте сначала рассмотрим вопрос о разрешающей процедуре для теоремности ТТЧ. Если бы существовал некий способ, при помощи которого можно было бы сказать, принадлежит ли данная формула X к классу «теорем» или «не-теорем», то, согласно Стандартной Версии Тезиса Ч-Т, должна была бы существовать некая конечная программа Флупа (общерекурсивная функция), которая могла бы проделать то же самое, когда входными данными является Гёделев номер формулы X. Важно помнить, что любое свойство, которое может быть проверено при помощи конечной программы Флупа, представимо в ТТЧ. Но, как мы вскоре увидим, это было бы источником проблем, поскольку если теоремность — представимое свойство, то Гёделева формула G становится так же порочна, как и парадокс Эпименида.

Все зависит от того, что утверждает G: «G — не теорема ТТЧ». Предположим, что G была бы теоремой. Тогда, поскольку теоремность, по предположению, представима, то формула ТТЧ, утверждающая «G — теорема ТТЧ», была бы теоремой ТТЧ. Но эта формула — не что иное как ~G, отрицание G; выходит, что ТТЧ непоследовательна. Предположим теперь, что G — теорема. Тогда опять, поскольку мы предполагаем, что теоремы представимы, формула, утверждающая «G — не теорема» являлась бы теоремой ТТЧ. Но эта формула — не что иное, как G; мы снова получаем парадокс. В отличие от ранее описанной ситуации, этот парадокс не имеет решения. Проблема заключается в начальном предположении, что свойство теоремности представлено некоей формулой ТТЧ; следовательно, нам придется отказаться от этого предположения. Это заставляет нас признать, что не существует программы Флупа, способной отличить Гёделевы номера теорем от Гёделевых номеров не-теорем. Наконец, если мы принимаем Версию ИИ Тезиса Ч-Т, мы должны пойти еще дальше и заключить, что не существует такого метода, при помощи которого люди могут отличать теоремы от не-теорем (и это включает методы, основанные на восприятии красоты). Сторонники Версии Коллективных Процессов все еще могут полагать, что Крабьи способности возможны; но из всех версий именно эту труднее всего подтвердить фактами.

Теорема Тарского

Теперь давайте рассмотрим результат Тарского. Тарский хотел выяснить, существует ли способ выразить в ТТЧ понятие теоретико-численной истины. То, что теоремность можно выразить (но не представить), мы уже видели; Тарский задался аналогичным вопросом в приложении к понятию истины. Точнее, он хотел определить, есть ли формула ТТЧ с единственной свободной переменной а, которая может быть интерпретирована как:

«Формула, чей Гёделев номер — а, выражает истину.»

Предположим, вместе с Тарским, что такая формула существует. Для краткости назовем ее ISTIN{a}. Теперь используем метод диагонализации и построем высказывание, утверждающее о себе самом, что оно ложно. Для этого мы точно повторим метод Гёделя, начиная с «дяди»:

Ea:<~ISTIN{a}ΛARITHMOQUINE{a'',a}>

Предположим, что Гёделев номер этого дяди — t. Арифмоквайнируем теперь самого дядю и получим формулу Тарского Т:

Ea:<~ISTIN{a}ΛARITHMOQUINE{SSS...SSS/a'',a}>

.                                          |______|  S повторяется t раз

В интерпретации эта формула читается как:

«Арифмоквайнификацией t является ложное утверждение.»

Но, поскольку арифмоквайнификация t — это собственный Гёделев номер Т, формула Тарского Т в точности воспроизводит парадокс Эпименида внутри ТТЧ, говоря о себе «Я — ложь». Разумеется, это ведет к заключению, что это высказывание одновременно является и истинным и ложным (либо ни тем, ни другим). Возникает интересный вопрос: что плохого в воспроизведении парадокса Эпименида? Какие от этого могут быть последствия? В конце концов, этот парадокс уже существует в русском языке, и русский язык пока от этого не погиб.

Магиификраб невозможен