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

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

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

В качестве примера рассмотрим следующее доказательство формулы 0'"' чь 0": а чь Ь -!- а' ~ Ь' а' ~ 0 в. а" ~ 0' а'~0 а" ~ 0' а" ~ 0' -+ а ~ 0" а"'~0" 0"" чь О" В результате разложения этого доказательства на нити мы полу- чим следующую фигуру разложения: Здесь в первую очередь бросается в глава то, что отдельные формулы доказательства встречаются в фигуре разложения в нескольких местах. Правда, само по себе это еще не исключает того, что в процессе возвратного переноса подстановок одна и та же формула докааательства будет всюду претерпевать одни и те же изменения.

Однако в действительности дело будет обстоять не так. В самом деле, начав производить возвратный перенос подстановок, мы прежде всего должны будем заменить формулу 9) формулой 10), т. е. подставить в 9) 0' вместо а. Затем эту подстановку нужно будет выполнить в идущих за формулой 9) схемах ааклю- — 1) ~ — в2) 3) 4) 6) 7) — з.8) — 9) ! 10) (А-~В) +(-]В э.-]А) (а ' =- Ь' -+. а =- Ь) — з- (а ~= Ь вЂ” в- а' Ф Ь') а' = Ь' — в- а = Ь 1) ) 3) 2) 1) 4) 3) 2) ~,)~ 10) [РЛ. Чг НАЧАЛА АРИФМЕТИКИ 10), 9), 8), 4), 3) 3 = 1 (ровенвтеа1 в (1 (неравенства), 1, 11, 111.

9 Си. с. 47. чения, а потом в нитях доказательства 10), 9), 8), 4), 2), 1) вместо 4) надо будет вставить ту формулу, которая у нас полу- чится вместо 8), а в нитях 10), 9), 7), 5), 4), 2), 1), 10), 9), 7), 5), 4), 3) вместо 4) — ту формулу, которая получится вместо з). Но при воэвратноы переносе подстановки 0' вместо а мы вме- сто 8) получим формулу 0" Ф 0' -+ 0"" чь 0", а вместо 5) — формулу 0" чь 0-+. 0" ~ О'.

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

И все же этого могло бы и не случиться. В частности, этого могло не случиться и в тоы случае, если бы мы применили наш метод возвратного переноса подстановок к гипотетическому доказательству формулы 0 Ф О, хотя заключительная формула этого доказательства вовсе не содержит никаких переменных. Иначе говоря, некоторые переменные могли бы остаться даже и после возвратного переноса подстаиовок. Если это действительно окажется так, мы удалим оставшиеся переменные, заменив каждую из них каким-либо допустимым выражением без переменных. Чтобы каким-нибудь образом нормировать эти замены, мы условимся подставлять: а) вместо любой формульной переменной без аргументов формулу 0=0, б) вместо формульной переменной с аргументом а равенство а=а, 1 11 ОВЩЕТОГИЧЕСКАЯ ЧАСТЬ ДОКАЭАТРТЬСТВА 283 в) вместо форыульной переыенной с несколькими аргументами =,..., 1 формулу а=то:...

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

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

Н '), определяли понятие м е н ь ш е для фигур типа 1гл. чг нАчАлА АгиФ»гвтнки 284 овщклогичвскля члсть докязлтвльствл Из двух различных цифр 3 н 1 (мы теперь имеем в виду фигуры О, 0", 0",...) одна, как легко видеть, явлнется составной частью другой в том смысле, что ее построение осуществляется в процессе построения этой второй цифры. Неравенство 3(1 мы будем считать и с т и н н ы м, если цифра а отлична от цифры 1 и является ее составной частью; в противном случае эта формула будет считаться л о ж н о й. Исходя из так определенных истинностных значений для равенств и неравенств, мы получим соответствующее определение и для нумерических формул, составленных из элементарных формул такого рода с помощью связок исчислении высказываний; при этом надо будет воспользоваться определениями истинностных функций Ь, ~, -ю-, В смысле этого определения все формулы нашей модифицированной (в результате исключения переменных) фигуры разложения принимают значение «истина», или, как мы будем говорить, являются истинными.

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

Тем самым любая формула такого вида оказывается истинной. То же самое верно и в отношении формул, получающихся из аксиомы (Р,) и, следовательно, имеющих вид В'=1 ~6=1; действительно, всякая такая формула истинна, во-первых, тогда, когда 3 совпадает с 1, потому что в этом случае истинно равенство а = 1; а во-вторых, она истинна и тогда, когда а отлично от 1, так как в этом случае 3' отлично от 1' и тем самым равенство 3' =- 1 ложно.

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

Тем самым действительно получается, что все формулы нашей фигуры являются истиннь1ми. Однако это находится в противоречии с тем фактом, что в конце рассматриваемого нами доказательства должна быть формула Очь О. Действительно, эта формула — как не содержащая переменных— процедурой исключения переменных не затрагивается; следовательно, в модифицированной фигуре разложения заключительной формулой должна быть формула 0-ь 0; как и все формулы этой фигуры, она должна быть истинной, в то время как в действительности она является ложной. Тем самым для того случая, когда употребление связанных переменных в выводе не допускается, невозможность вывода формулы ОФО иэ рассматриваемой нами системы аксиом доказана. Рассуждение это основывается на том же самом принципе, с помощью которого мы ранее убедились в невозможности вывода средствами исчисления предикатов, равно как и средствами расширенного исчисления предикатов, каких-либо двух формул Я и ~ Я.

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

Это сопоставление было нами осуществлено в резуль- 1) См. с. 233, [гл. Р1 НАЧАЛА АРИФМЕТИКИ 286 ОБЩЕЛОГИЧЕСКАЯ ЧАСТЬ ДСКАЗАТЕЧЬСТВА 287 тате разложения доказательства на нити и последующего исключения переменных. Конечно, рассмотренному результату можно придать и положительную форму, следующим образом усилив доказанную нами теорему невозможности: Всякая формула, выводимая из нашей систелы аксиом без использования связанных переменных, является истинной.

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

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