Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 60

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 60)

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

Тогда в точности так же, как и в предыдущем случае, мы разложим фигуру доказательства на нити и произведем перенос подстановок в исходные формулы. Правда, здесь, ввиду наличия схем (а) и (р), нам потребуется провести специальные мероприятия. Рассматриваемые схемы Я -+. (В (а) й) (а) -э. Я и Я вЂ” ~7хй)(х) Зхй)(х)-э-Я применимы, как известно, лишь в предположении, что переменная а встречается только там, где это указано аргументом. Мы должны будем специально проследить за тем, чтобы это условие, будучи выполненнымвначале, соблюдалось и после возвратного переноса подстановок. С этой целью перед выполнением переноса подстановок мы предпримем следующие действия.

Мы пойдем по рааложенной фигуре доказательства, начиная с заключительной формулы, и всюду, где будут встречаться две формулы Я -в- ч х З (х) и Я -э ю (а) или соответственно Зхй(х)-+ Я и В(а)-А-Я, связанные друг с другом применением схемы (а) (или соответственно (р)), мы во второй из этих формул (т. е. в первой формуле схемы) подставим вместо а какую-нибудь ранее в этой нити доказательства не встречавшуюся свободную переменную и сохраним ее в продолжении атой нити и в нитях, ответвляющихся от нее, до того места, до которого можно проследить это вхождение переменной а, начиная с рассматриваемого места. Для разъяснения этого указания мы рассмотрим следующий фрагмент доказательства: -1) а<ЬАЬ<с- а(с -~ 2) а<ЬАЬ<с-д< ° — + 3) д(аАа(с-ьд(с 1 схема (р) Г- 4) Зх (д ( х А х < с) — ~- д < с ) — ~ 5) Эх(а <х Ах< с)-~-а<с (за этими формулами могут идти еще и другие, ведущие нас к заключительной формуле 6).

Мы рассмотрим нить доказательства, идущую сначала от заключительной формулы 6 к формуле 5) и проходящую затем через формулы 5), 4, 3), 2), 1). Для этой нити наше предписание состоит в следующель В формуле 3), которая связана с 4) по схеме (р), мы должны вместо переменной а подставить какую-нибудь еще нигде в этой нити (начиная с самой формулы 6) не встречавшуюся переменную — например г. Производить зту замену в рассматриваемой нити дальше не надо, так как в формуле 2) переменная а уже не встречается. В результате этого вместо следующих друг за другом в указанной нити доказательства формул 1), 2), 3), 4), 5) мы получим следующий модифицированный ряд формул: а(ЪАЬ(с -А.а(с, с)<ЬАЬ<с -+с)<с, с)(г А г(с — ~-с)(с, Зх (И( х А.

х < с)-+ Ы( с, Зх (а ( х А х ( с) -+. а ( с. Структура доказательства при этом преобразовании останется абсолютно незатронутой; только в применениях схем (а) и (р) вместо ранее выделенной переменной а теперь будет фигурировать некоторая другая переменная (в рассматриваемом случае — переменная г).

На этом примере можно убедиться, что принятые нами меры действительно являются необходимыми. Предположим для определенности, что на том отрезке нашего доказательства, который ведет от формулы 5) к заключительной формуле 6, переменные а и с, фигурирующие в формуле 5), исключаются не в результате подстановки, а в результате применения формул (а), (Ь), и схем пгоцкдтвл гкдукция 289 288 нлчйлъ лэиэмвтики сгл. ш (а), (Р) [например, по правилу (6) ')); тогда при возвратном переносе подстановок формула 5) не будет затронута. Если же в рассматриваемой нити доказательства мы применим процедуру возвратного переноса цодстановок к первоначальным формулам разложенного вывода, начиная с формулы 5), то вместо формул 3) и 4) получим формулы 3') а < а «х а ( е -+.

а с и 4') Зх(а(хек:х«с)-е-а«.,с и тем самым структура вывода окажется разрушенной, так как условие применимости схемы (Р), необходимое для перехода от 3') к 4'), не будет выполняться. Если же процедуру возвратного переноса подстанозок мы применим к формулам, предварительно модифицированным согласно нашему предписанию, то вместо первоначальных формул 3) и 4) мы получим формулы Зе) а «"' г бс г ( е -е а ( с и Зх (а «.

х А х( с) — ~ а ( е; 4*) при этом структура доказательства сохранится; только выделенная в схеме (Р) переменная а в 3*) будет заменена на г. Осуществив в схемах (и) и (Р) описанные выше замены, мы можем затем произвести возвратный перенос подстановок в исходные формулы — так, как зто делалось раньше,— без ущерба для структуры доказательства, поскольку роль выделенной з схемах (а) и ([)) переменной а мы теперь будем поручать и некоторым другим свободным индивидным переменным. После возвратного переноса подстановок можно будет указанным ранее способом исключить и, возможно, остающиеся еще ухормульные переменные.

Исключить все свободные индивидные переменные прежними методами теперь невозможно, ввиду наличия в схемах (сх) и (Р) свободных переменных. Таким образом, фигура разложения, к которой мы пришли, состоит не только из нумерических формул; в ее формулах встречаются свободные и связанные переменные, а следование формул доказательства друг за другов! происходит не только на основе повторения уже имеющихся формул и применения схем заключения, но также и на основе схем (сх) и ([!) и переименования связанных переменных. В качестве исходных формул к тождественным формулам исчисления высказываний и нашим аксиомам присоединяются еще и основные формулы (а) и (Ь) исчисления предикатов. х) См. с.

!46. 8 3. Доказательство непротиворечивости с помощью процедуры редукции 1. Исключение квантора всеобщности; этапы редуцирования; понятие редукции формулы. Мы будем теперь стремиться обобщить нашу первоначальную процедуру таким образом, чтобы вместо и с т и н н о с т и нумерических формул рассматривалось некоторое более общее свойство, которым обладают не только нумерические формулы и которое будет затем обнаружено у всех формул любого конкретного доказательства. Этот клан мы осуществим методом, который независимо друг от друга разработали Эрбран и Пресбургер '). Метод зтот заключается в том, что формулам, содержащим связанные переменные, ставятся в соответствие их р е д у к ц и и — форлсулы без связанных переменных, равнозначные первоначальным формулам при содержательном нх истолковании.

Мы можем упростить зту процедуру, с самого начала полностью удалив из доказательства квавторы всеобщности. Действительно, если в первоначально данном нам доказательстве каждое выражение чхЯ (х) мы заменим соответствующим ему выражением ! Зх ! Я(х), то основная формула (а) сзсх А (х) -+ А (а) перейдет при атом в формулу ! Зх 1А (х) -+ А (а), которая получается из основной формулы (Ь) в результате подстановки и контрапозиции, а схема (а) Я -+-'п)(а) Я вЂ” ь сбсх й)(х) перейдет в схему Я -ь [В (а) Я вЂ” ь !Зх !л)(х)' вместо которой может быть вставлен вывод формулы Я вЂ” ь-~Зх ~й) (х) из формулы Я -+-й) (а), ') Н в г Ь г в и й 1. ЙвсЬегсЬев впг !а СЬеог1е йе 1в йвюопвСгаыоп: Ыввеггас!оп.— Рапв, !930, сЬ.

1ч; Р г в в Ь п г 8 в г М. 1)Ьег йсе чо11всапй!8)св!с еспев зеч1ввеп 8увсепсв йвг Аг!сЬюесЖ хапхег ЕаЫеп, сп сче1сЬвю й!в Айй!с!оп а1в е!пх!яв Орегвыоп Ьегчогхг!СС. — С.г. йп ргвпс!ег сопзтев йев спаСЬ. йев Раув 81ачев, ЖагвсЬап, 1930. д. Глльберх, и. вернайе 291 ПРОЦЕДУРА РЕДУКЦИИ (гл. Ул нАчАлА АРнв>метики 290 который получится, если мы сначала применим контрапоэнцию: 13(а)->. )>Я, аатем схему (()): Зх 13(х)-э )Я, а затем еще раэ контрапозицию: Я-+. 13х 13(х).

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

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

Кроме переменной х формула Зх Я (х), вообще говоря, может содержать еще и другие связанные переменные, относящиеся к внешним по отношению к ней кванторам существования. Выражение Я (х) строится с помощью связок исчисления выскааывакяй из равенств и неравенств а=Ь, а<Ь, где а и Ь суть либо цифры, либо индивидные переменные, быть может, с навешенными на ннх штрихами, причем зто могут быть как свободные, так и связанные индивндные переменные. Чтобы в дальнейшем иметь возможность указывать количество навешенных на а штрихов, мы будем посредством а(1) Я~ 'У'." Ч Я(, члены которой Я, ...

Характеристики

Список файлов книги