7. Универсальная система

Точно так же, как мы говорили об исчислении равенств и машинах Тьюринга внутри соответствующим образом построенных канонических систем, мы начнем сейчас говорить о самих канонических системах внутри системы того же самого типа. Эта возможность, автоссылок, впервые использованная Гёделем [2] в его знаменитой работе о неразрешимости аксиоматических теорий, составляет само ядро теории рекурсивных функций.

Мы рассмотрим все рекурсивно перечислимые множества слов в данном алфавите он системы Поста, алфавиты которых являются расширениями данного алфавита. Чтобы о них можно было говорить внутри канонической системы, мы должны закодировать их словами в фиксированном алфавите. Оказывается, что подходит алфавит

Заменим каждый вспомогательный знак словом из списка

и переменные — словами

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

Пример. Базис множества чисел, не являющихся простыми, определенного в п. 3:

Здесь Вспомогательные знаки были заменены на и переменные соответственно на

Гёделевский номер рекурсивно перечислимого множества — это лексикографический номер его базиса.

Если рекурсивно перечислимое множество задано в виде своего базиса, то неудобно сначала производить все подстановки, а затем размещать применения схем в форме дерева. Поэтому мы чуть иначе определим понятие доказуемости. В следующих трех индуктивных пунктах мы, говоря о знаках, переменных, термах и схемах, имеем в виду коды этих объектов.

1 Схема, встречающаяся в базисе, доказуема.

2 Если некоторая схема доказуема, то доказуема и схема, получающаяся из нее подстановкой некоторой цепочки знаков вместо переменной.

3 Если доказуемы причем терм, то и доказуемо.

Непосредственно проверяется, что слово принадлежит рекурсивно перечислимому множеству тогда и только тогда, когда оно доказуемо из его базиса по этим правилам. Мы готовы теперь к доказательству следующей фундаментальной теоремы.

Существует рекурсивно перечислимое отношение между натуральными числами и словами в данном алфавите, такое, что тогда и только тогда, когда есть гёделевский номер рекурсивно перечислимого множества, которому принадлежит а.

Это отношение будет называться универсальным для рекурсивно перечислимых множеств слов в данном алфавите.

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

знаки

вспомогательные знаки

переменные

схемы

(см. скан)

схема и получена из схемы в результате подстановки цепочки знаков вместо переменной

Доказательство закончено.

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

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

натуральных чисел. Следовательно, диагональное множество неразрешимо.

Мы построили рекурсивно перечислимое множество натуральных чисел, которое неразрешимо.

Это важное следствие принадлежит Чёрчу [1]. Заметим, что в доказательстве скрыто рассуждение, приводящее к парадоксу Рассела. Действительно, если мы отождествим рекурсивно перечислимое множество с его гёделевым номером, то диагональное множество состоит из всех множеств, которые содержат самих себя. Чтобы доказать разрешимость диагонального множества, мы должны были бы указать рекурсивно перечислимое множество, элементы которого — это в точности те множества, которые не содержатся в себе. Рассуждение Рассела показывает, что допущение существования такого множества ведет к противоречию.

Рассмотрим утверждение

которое истинно классически, так как оно немедленно следует из закона исключенного третьего. Интуиционистская интерпретация этого утверждения такова. Мы нашли метод, позволяющий нам доказать либо либо какое бы натуральное ни было нам дано. При такой интерпретации это утверждение ведет к противоречию, если принять тезис Чёрча. Мы видим, таким образом, что если логическим связкам придан их конструктивный смысл, то закон исключенного третьего больше неприменим. Это фундаментальное обстоятельство было открыто Брауэром [1].

Теорема Чёрча — плод работ двадцатых и тридцатых годов, вызванных уверенностью Гильберта в разрешимости всех математических проблем. Брауэр с самого начала отвергал это утверждение Гильберта. Теперь, если разрешимость понимается в смысле существования эффективной процедуры для доказательства или опровержения любого математического

утверждения и если принят тезис Чёрча, то теорема Чёрча усиливает возражение Брауэра до настоящего опровержения.