4. Исчисление равенств

Первое точное определение эффективно вычислимой функции принадлежит Эрбрану и Гёделю [3]. Их идея состояла в попытке найти наиболее общий вид рекурсивных определений теоретико-числовых функций.

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

Здесь переменные, пробегающие множество натуральных чисел.

В общем случае мы рассматриваем список функциональных символов

с каждым из которых связано неотрицательное число, называемое числом мест

Как уже отмечено, всегда должен присутствовать функциональный символ 0 с числом мест нуль и одноместный функциональный символ о для функции следования. Последний функциональный символ с числом мест называется главным функциональным символом.

Цифры определяются следующими индуктивными пунктами.

1 0 - цифра.

2 Если цифра, то и цифра.

Далее предположим, что дан список переменных

Из них и из функциональных символов мы индуктивно строим термы.

1 Переменная есть терм.

2 Если термы, то — терм

В частности, все цифры являются термами. Если термы, то равенство. Список функциональных символов и список переменных вместе с конечным множеством равенств называется исчислением равенств.

Для исчисления равенств имеется два правила вывода.

1 От данного равенства можно перейти к новому равенству, полученному подстановкой некоторой цифры вместо всех вхождений одной и той же переменной.

2 От равенства и равенства где цифры, можно перейти к

равенству, полученному из заменой некоторого вхождения терма на

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

Если выводимо не более чем для одной цифры при любом выборе цифр то мы будем говорить, что рассматриваемое исчисление равенств определяет частично рекурсивную функцию в смысле Эрбрана и Геделя. Мы покажем, что это понятие частично рекурсивной функции не является более общим, чем то, которое мы ввели с помощью канонических систем Поста.

Если дано исчисление равенств, мы можем найти рекурсивно перечислимое множество, элементы которого — это в точности выводимые равенства вида где цифры и главный функциональный символ.

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

знаки

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

переменные

производящие схемы

равенства данного исчисления равенств, перед, которыми вставлена буква Е: