§ 4. Устранимость характеристик (i-символов)

1. Обобщение i-правила; связь с первоначальным i-правилом; термы ...

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

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

После этого подробного изложения способов применения -символа, т. е. формализации понятия «тот, который», мы теперь

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

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

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

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

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

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

переходит в такую схему, выводимость которой непосредственно усматривалась бы.

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

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

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

а эта последняя переводима с использованием обеих аксиом равенства в формулу

В соответствии с этим, в качестве формальной -аксиомы» мы можем взять формулу

Исходя из этой аксиомы и воспользовавшись формулой

мы немедленно получим схему -правила в качестве производного правила.

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

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

Обозначим посредством формулу

Применим -правило к формуле

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

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

Первая из этих формул вместе с формулой

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

Вторая из них совместно с формулой

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

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

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

а следовательно, и

Если мы теперь положим т. е. введем определение

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

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

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

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

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

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

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

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