Гильберт, Бернайс - Основания математики. Теория доказательств (Гильберт Д. - Основания математики и прочие работы), страница 4

т. 1, гл. 1!1, с. 201 — 202. ИСКЛЮЧЕНИЯ СВЯЗАННЫХ ПЕРЕМЕННЫХ !ГЛ, 1 ством Я; тогда ...». С формальной точки зрения этот прием сводится к добавлению формулы Я(6) к числу исходных. Для формул, не содержащих символа 6, этот способ умозаключений — в чем мы убедились с помощью дедукционной теоремы— не открывает никаких новых возможностей в части, касающейся доказательств: лсобая формула без символа 6, выводимая с использованием данного символа и формулы Я(6), будет выводиться и без использования этого символа. Кроме того, для любой формулы 8(6), выводимой с помощью формулы Я(6), можно будет без использования символа 6 вывести формулу Я (с) — 8 (е) со свободной переменной с, не входящей в формулу 8(б), При этом искомый вывод будет получаться из вывода формулы 8 (6), если мы символ б всюду заменим переменной с, затем к каждой формуле имплнкативно присоединим посылку Я (с), а потом добавим небольшие фрагменты доказательства, необходимые для сохранения структуры вывода (как это делалось при доказательстве дедукционной теоремы ')).

Таким образом, в силу выводимости формулы И~Я(~) имеет место полный параллелизм между выводами, производящимися с использованеем формулы Я (6), и сопоставленными им выводами, не использующими символа 6; при этом каждой строке вывода, представляющей собой формулу 8 (6), сопоставляется некоторая (однозначно определенная — с точностью до выбора не входящей в 8 (6) свободной переменной с) формула Я (с) — 8 (с), а каждой строке вывода, представляющей собой не содержащую символа 6 формулу 8, сопоставляется сама эта формула. Хотя формула Я (с) — 8 (с), вообще говоря, дедуктивно и не равна формуле 8(6), даже если пользоваться формулой Я(6)„ тем не менее из нее и из Я(6) путем соответствующей подстановки и применения схемы заключения мы сразу получим 8 (6), Этот результат немедленно распространяется и на формулы о несколькими кванторами существования Ж1 ° )гсг((61> '~ гг)~ ие содержащие свободных переменных (но содержащие, быть может, какие-нибудь другие связанные переменные, отличные от х,, ..., Х„).

Если формула такого рода уже будет иметься в качестве исходной или в качестве выведенной формулы и если мы затем 1) См. т. 1, гл. 1Ч, с. !94 — !96, 2! $ и символьное Решяние экзистенцилльных эоимгл введем новые индивидные символы 6,, ..., б, и возьмем формулу Я (бм ..., 61) в кач честве исходной, то это не приведет к существенному расй шир ению нашего формализма. В самом деле, каждой выводимо с помощью формулы Я(бн ..., 61) формуле 8 (бп * 6»1,) где 6 , ...

6 суть какие-либо из символов б, ..., 6„ будет 1 1' соответствовать выводимая без использования символов б,, ..., 6 формула Я(с,, ..., с,)-~-8(с„, ..., с„„), где с, ..., с.— какие-либо не встречающиеся в 8(6„, ..., 6„~) 1 сво д бодные переменные; при этом вывод данной формулы будет б . алее, протекать параллельно выводу формулы 8(б», ..., „„).

Д если с помощью формулы Я(6,, ..., 6,) будет выводиться неко- торая формула 8, не содержащая символов 6,, ..., 6„, то ее можно будет вывести и без применения этой формулы (а значит, и без использования символов 6, ..., 6„). П оведенное рассмотрение теперь можно применить к системе аксиом такой, что среди ее формул имеется формула вида ~ (~) р в или Ж ...

Зу,.Я(х„..., р,), не содержащая свободных перемен- ных. В результате получается, что если, введя индивидный сим- вол б, мы заменим формулу ЗХЯ(х) формулой Я(6), или соответ- ственно введя индивидные символы 6,, ..., б„заменим формулу 3у ... З~,,Я(й,, ..., Ес) формулой Я(6,, ..., 6,), то никакого су- 1 ''' щественного усиления рассматриваемой системы не произойдет. В частности, запас выводимыхсвформул, не содержащих ни одного из введенных индивидных символов, для первоначальной и для модифицированной системы аксиом будет одним и тем же, а отсюда, в частности, вытекает, что вотноисении непро- тиворечивости обе эти системы одинаковы. Чтобы проиллюстрировать рассмотренный метод модификации аксиоматических систем, мы возьмем в качестве примера систему, состоящую из следующих трех аксиом: )(а са), а((сбсЬ(с- а(е, ЗХЛу (х (у).

ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ 1гл 1 Е Эх сли мы введем индивидные символы а и () и заменим акси сиому х=(р(х<р) формулой а<р, то получим систему, состоящую из следующих аксиом без связанных переменных: )(п<а), а<Ь В«Ь<с-+а<с, а< 1). С одной стороны, из этой системы аксиом мы можем полу- чить первоначальную систему, воспользовавшись формулой (Ц'). С другой стороны, новая система аксиом не является существенно более сильной, чем старая. В самом деле, всякой выводимой средствами новой системы формуле 5(а, ()) соответствует выводи- мая средствами старой системы формула а<Ь-~.))(а, Ь), где а и Ь вЂ” какие-либо свободные переменные, не входящие в 5(а, р).

Например, формуле а<а-ь ~(р<а), выводимой средствами нашей модифицированной системы, соот- ветствует формула Ь<с-ь(а Ь-ь )(с<а)), выводимая средствами первоначальной системы. Пока на этот метод исключения экзистенциальных аксиом наложено ограничение, заключающееся в том, что он применяется лишь к аксиомам без свободных переменных. Чтобы освободиться от этого ограничения, мы должны будем распространить наше рассуждение на формулы вида Зйй((п, ..., 1, х), где а, ..., ! — полный списо(й, свободных переменных, входящих в эту формулу. В этом случае вместо индивидного символа б нам придется ввести некоторый функциональный знак ((а, ..., Ь) и подобно тому, как в предыдущем случае мы брали в качестве исходной формулу 2((б), сейчас нам придется взять в качестве исходной формулу 2((д, ..., 1, ((а, „., 1)).

Формализуемый таким образом способ умозаключений состоит в том, что, доказав какую-либо теорему существования, «Для всякого набора объектов 1, ..., 1 существует объект 1, обладаю- ') Сн. Прнложенне 1, с. 461. 4 П симВОльнОе Решение экзистенпиАльных ФОРИУл 23 щий свойством «1(а, ..., 1, 1)», мы продолжаем далее рассуждать следующим образом: «Пусть теперь ( (а, ..., Ь) — какая-либо функция, сопоставляющая каждому набору а, ..., 1 такое значение 1, что для него выполняется ь)((а, ..., 1, (), и т. д,». Обратим внимание на то, что в этом рассуждении используется принцип выбора.

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

Переход от формулы ЗФ (и, ..., 1, й) к формуле е((а, ..., 1, ((а. .., 1)) с новым функциональным знаком (, равно как и переход отформулы Зйй(й) без свободных переменных к формуле 6(б) с новым инднвидныи символом б, мы будем называть символьным решением этих экзистенциальных формул.

Эта операция, совместно с операцией замены связанных переменных свободными'), дает нам способ, позволяющий перейти от произвольной предваренной формулы') 11, не содержащей формульных переменных, к некоторой формуле без связанных переменных, нз которой формулу 5 можно получить обратно средствами исчисления предикатов. В самом деле, всякая такая формула )1 представляет собой формулу одного из следующих двух видов: ьга (В), ЭВ8 (й). Заменив в формуле )(йй,(й) связанную первменную х свободной переменной д, мы получим формулу 5,(а),',дедуктивно равную формуле ч(й11, (х). В результате символьного решения формулы ЖВ11, (И) мы получим некоторую формулу )т, (1), где терм 1 в том случае, когда й, (г) не содержит свободных переменных, представляег собой вновь вводимый индивидный символ, а в противном случае '1 Обшую форнулнровку прннпнпа выбора см.

в ч. 1, гл. П, с. 69. В расснатрнваенон случае в качестве П, следует взять совокупность всевозмо нных значений а, ..., 1, а в качестве о» вЂ” совокупность всевозможных зньч~нвй »1 См. Приложение 1, с. 472. ') О понятна предваренной формулы сн. т. 1, Рл, 1Ч, с. !62 н далее. ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ )гл. ! является вновь вводимым функциональным знаком с аргументами, фигурирующими в 1)т(у) в качестве свободных переменных. Ст формулы й,(1) применением основной формулы (Ь) мы можем возвратиться к формуле Зр~, (у).

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

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

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