2. Россеровский подход и его упрощение, произведенное Хазенъегером; подстановка i-термов; аксиома (i); свойства рассматриваемых формальных систем.

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

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

а подстановку -термов формализуем с помощью аксиомы

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

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

Для собственного формула является выводимой (быть может, с переименованными переменными и поэтому аксиома дает нам формулу

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

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

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

Россеровская формализация характеристик теперь может быть упрощена путем объединения аксиом в формулу

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

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

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

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

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

Формулами их являются либо элементарные формулы, либо формулы, образованные из других формул при помощи символов

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

В качестве исходных формул у нас имеются: 1) собственные аксиомы; 2) формулы, построенные по одной из следующих схем формул:

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

б) схемы, соответствующие основным формулам (а) и (Ь) исчисления предикатов:

в) схема, соответствующая аксиоме равенства

г) схема, соответствующая аксиоме

д) быть может, схема, соответствующая аксиоме индукции:

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

Среди аксиом должна быть формула если она не является выводимой.