§ 4. Представимость рекурсивных функций; переход к удовлетворительной системе аксиом для арифметики

1. Возврат к полному формализму; система (С); понятие существенного расширения формализма; примеры несущественных расширений; представимость функции.

От рассмотрения рекурсивной арифметики мы теперь вернемся к прежнему кругу идей. Мы исходили из тех соображений, что присоединение к исчислению предикатов системы аксиом (В) еще не дает нам формализма арифметики, несмотря на то, что все пять аксиом Пеано оказались в ней формализованными, причем не дает по той простой причине, что мы не включили в эту систему разрешения вводить функции при помощи рекурсивных определений. Это привело нас к более детальному рассмотрению метода рекурсивных определений, которое показало, что хотя рекурсивное введение функции и заслуживает названия определения, поскольку при подстановке какой-либо цифры вместо выделенной (посредством данной рекурсии) переменной, а тем более при подстановке цифр вместо всех переменных, оно дает нам некоторое определяющее выражение, но что для самой функции, рассматриваемой с переменными аргументами, при этом не получается никакого выражения, чем рекурсивное введение и отличается от явного определения, которое заключается во введении определенного сокращенного обозначения. В качестве еще одного отличия рекурсивного определения в сравнении с явным мы констатировали то обстоятельство, что непротиворечивость введения рекурсивных определений еще не гарантируется непротиворечивостью предшествующих аксиом, а зависит от определенных свойств этих аксиом. Рекурсивные определения неявно характеризуют штрих-функцию и поэтому они могут также играть роль арифметических аксиом. В частности, мы нашли, что аксиомы с помощью аксиомы равенства оказывается здесь излишней) и формулы могут быть выведены из рекурсивных равенств для функций . В случае присоединения схемы индукции, для вывода формул достаточно уже одних рекурсивных равенств для функции . А из рекурсивных равенств для и на основе

явного определения

с помощью аксиом равенства, формулы схемы индукции можно вывести аксиомы

Все эти выводы основываются на элементарном исчислении со свободными переменными.

Если же за основу взять исчисление предикатов, то тем более получится, что все формулы системы аксиом (В) могут быть выведены из системы аксиом, состоящей из второй аксиомы равенства, формулы рекурсивных равенств для функций и аксиомы индукции, т. е. из системы формул

с добавленным явным определением

Еще более, чем рассмотрением этих выводимостей, силу рекурсивных определений мы продемонстрировали тем, что с помощью рекурсий, обходясь без использования связанных переменных, мы осуществили построение значительного фрагмента арифметики. Это построение рекурсивной арифметики сделало в высшей степени правдоподобным предположение, что если мы положим в основу рассмотрения все исчисление предикатов в целом, то присоединение рекурсивных определений к символам и аксиомам системы (В) приведет к существенному расширению нашего формализма. Но какого-либо строгого доказательства этому факту мы еще не дали. Для того чтобы провести такое доказательство, мы должны будем уточнить, что именно мы будем понимать под существенным расширением нашего формализма. Расширение какого-либо формализма имеет место уже тогда, когда вводится какой-нибудь функциональный знак, который нельзя явно определить с помощью какого-либо ранее

построенного терма таким образом, чтобы при замене данного функционального знака этим термом формулы, посредством которых вводится этот функциональный знак, переходили в выводимые (т. е. в выводимые в исходном формализме). В этом смысле слова формализм системы (В) расширяется уже введением функции при помощи рекурсивных равенств

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

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

должно было бы перейти в формулу, выводимую средствами системы (В), т. е. оказалось бы выводимым равенство

Но тогда средствами системы (В) можно было бы вывести и формулы

(так как но предположению а не содержит переменной u), а тем самым и формулу

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

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

и тогда средствами системы (В) можно было бы вывести равенство

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

между тем как эта формула является ложной.

Таким образом, функция действительно не допускает явного определения в формализме системы (В). И тем не менее совокупность высказываний, изобразимых в формализме системы (В) посредством формул, не претерпевает никакого расширения. Действительно, функциональное отношение, изображаемое равенством

может быть выражено без функционального знака формулой

Именно, если мы сокращенно обозначим эту формулу посредством то из аксиомы непосредственно могут быть выведены формулы

из этих формул при помощи схемы индукции можно будет получить

а с помощью формул и второй аксиомы равенства мы получим

Эти две формулы выражают тот факт, что отношение всякому значению переменной а однозначно сопоставляет то единственное значение переменной для которого имеет место а формулы

выражают тот факт, что это соответствие, рассматриваемое как функция, удовлетворяет рекурсивным равенствам для

Только что приведенные выводы осуществляются без использования функции Если же дополнительно присоединить рекурсивные равенства для то индукцией по а мы получим

эквивалентность

которая в прямом виде выражает тот факт, что равно тому числу которое находится к а в отношении Из этой эквивалентности с помощью аксиом равенства [т. е. с использованием формулы 6а)) из гл. V] можно, далее, получить формулу

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

Между прочим, с исключением функционального знака из формул можно связать (что из предшествующего непосредственно не усматривается) исключение функции из выводов; иначе говоря, в выводе формулы, не содержащей функционального знака мы всегда сможем обойтись без использования функции

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

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

и формулой

позволяет сделать следующие выводы относительно цифр, являющихся значениями фигурирующих здесь переменных: Если цифра, значение, которое получается в результате вычисления то формула

является истинной и в то же самое время выводимой средствами системы (В). А если цифра, отличная от то формула

является ложной, а ее отрицание выводимо средствами системы (В).

Такое же положение вещей, с каким мы сталкиваемся здесь в связи с функцией имеет место и в отношении функции

которую мы в нашей рекурсивной арифметике ввели посредством явного определения

с помощью функций а

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

может быть заменено формулой

принадлежащей формализму системы (В). К этой формуле упомянутое определение функции а ведет нас не непосредственно, а лишь через выводимые из него формулы

Эти формулы определяют функцию в том смысле, что для любых двух цифр и (в зависимости от того, равны эти цифры или различны) они дают возможность вывести либо равенство

либо равенство

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

заменить формулой

которую мы для краткости обозначим посредством то определяющие формулы перейдут в формулы

которые могут быть выведены с помощью формулы

Кроме того, с помощью аксиом равенства могут быть выведены формулы

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

и что если отлично от значения то теми же самыми средствами может быть выведена формула

Рассмотрение примеров этих двух функций, присоединение которых к формализму системы (В) хотя и расширяет запас термов, но не изменяет запаса изобразимых отношений, наводит нас на мысль дать следующее уточнение понятия существенного расширения (речь идет о расширении формализма путем присоединения какой-либо функции).

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

можно представить формулой

этого формализма в том смысле, что при каждом замещении переменных

цифрами

в рассматриваемом формализме оказывается выводимой формула

если совпадает со значением

и формула

в противном случае. При этом представляющая формула

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

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