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

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

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

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

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

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

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

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

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

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

и

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

которые необходимо будет добавить к прежним аксиомам, приведенным в пп. I, II и III § 1 гл. I. Если теперь обозначить посредством К конъюнкцию всех аксиом, а посредством формулу для какого-либо геометрического предложения, выразимого с помощью основных предикатов то доказуемость этого предложения на основе наших аксиом будет равносильна выводимости в исчислении предикатов формулы, которая получится

из формулы

если мы всюду заменим в ней символ формульной переменной А с двумя аргументами, а символы формульными переменными с тремя аргументами.

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

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

— формула, возникающая таким образом из формулы В выводе аксиома может быть заменена формулой и рядом формул вида

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

представляет собой список всех этих связанных переменных,

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

Рассмотрим формулу

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

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

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

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