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

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

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

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

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

Тогда из этого определения могут быть выведены формулы единственности для по аргументу с:

Если мы воспользуемся теперь -правилом, то у нас в качестве терма появится

при этом, с одной стороны, -правило даст нам формулу

а с другой стороны, определение символа в сочетании с аксиомой даст формулу

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

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

мы получим формулу

которая переводима в формулу

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

добавим к аксиомам и при этом опустим аксиому

а функциональный знак который ранее был у нас основным знаком, теперь [после введения при помощи -правила] явно определим посредством равенства

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

и

перейдут в некоторые выводимые формулы.

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

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

формула, не содержащая функционального знака выводима тогда и только тогда, когда она выводима в

Таким образом, формализмы и оказываются равносильными в этом смысле слова.

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

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

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

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

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