Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 57
Текст из файла (страница 57)
х < г), 7х Зу (х < у), лхасу(у'~х), 1э х 'Уу Чг (х' =- г А у' = г -~- х = у) . Однако на атой системе формул мы не остановимся и сведем ее к другой, не содержащей свяэанн х переменных. 3. Переход к аксиомам без связанных переменных с усилением экзистенциальных аксиом; символ О; цифры в новом смысле; аксиомы,Пеано; получившаяся система аксиом. Прел«де всего, в формулах, начинающихся кванторами всеобщности, относящиеся к этим кванторам связанные переменные х, у и г мы можем заменить свободными переменными а, Ь и с; в результате рассматриваемые пять формул перейдут в следующие, дедуктивно Равные им формулы: 1(а <а), а Ь А Ь<с — +а<с, Лу(а <у), Зх'эу (у ~ х), а' = с А Ь' = с-+.
а = Ь. Кроме того, немного упростим последнюю формулу. Из этой фор- мулы в результате подстановки Ь' вместо с, перестановки членов конъюнкции и применения правила разъединения посылок мы получим а отсюда — поскольку Ь' = Ь' получается подстановкой из («,)— мы получим а' = Ь'-» а = Ь. С другой стороны, из атой формулы можно снова получить послед- нюю формулу нашей системы; действительно, из аксиом равенства, как было показано ранее "), выводима формула 4)): а = с-э- (Ь = с — » а = Ь), )гл, ш НАЧАЛА АРИФМЕТИКИ пегеход от вопгосА о невыводимости 271 270 из которои соединением посылок и подстановкой можно получить формулу а =сАЬ =с»а =Ь, которая вместе с формулой а'=Ь-»а=Ь по правилу силлогиама дает формулу а' = с д,.
Ь' = с-» а = Ь. Таким образом, в силу аксиом равенства эта формула окааывается равнозначной формуле а' = Ь'-» а = Ь. Теперь связанные переменные остаются только в двух фор- мулах: Зу (а(у), Зхту (у' ~ х). При содержательной трактовке этим формулам соответствуют экзистенциальные еыснаэмеания. Чтобы избавиться от экзисте— ц ального вида этих выскааываний, мы их усилим путем явного указания тех объектов, существование которых утверждается; именно, в случае первой формулы речь пойдет об указании некоторой функции от аргумента а, а в случае второй — об указании некоторого индивидуального объекта.
Формально уточнение формулы Зу (а(у) Зх уу (у' чь х), мы введем индивидный символ О. Теперь Зхуу (у' чА х) мы сначала возьмем формулу ту(у'~0), вместо формулы из которой она может быть получена применением основной фор- мулы (Ь). Но формула Чу(у'~0) мы осуществим, ваяв вместо нее формулу а(а, из которой исходная выводится применением основной формулы (Ь).
Для того чтобы получить соответствующее уточнение для формулы дедуктивно равна формуле а'~0. Итак, теперь вместо двух рассматриваемых формул Зу(а(у) и Зх)7у(у'Фх) у наг будут иметься фоРмУлы а(а' и а'~0, из которых мы снова можем вывести первоначальные формулы. Итак, все связанные переменные теперь удалены, и мы при- шли к системе, состоящей из следующих пяти формул: ) (а (а), а(Ьд Ь (с-»а (с, а(а, и чьО, а' = Ь'-» а = Ь. Теперь речь пойдет о том, чтобы в рамках расширенного исчисления предикатов доказать непротиворечивость этой системы, т.
е. о том, чтобы в рамках исчисления предикатов установить непротиворечивость системы, состоящей из этих пяти формул и двух аксиом равенства. Прежде всего, рассмотрим этот формализм более детально. В качестве его внелогических символов мы ввели: предикатные символы = и (,нндивидный символ 0 и символ штриха в качестве функционального знака. Применение штриха молзет быть итерировано, и тогда, исходя из какой-либо переменной— например а, — мы получим выражения типа а" а а""' Ф а исходя ив символа О,— выражения такие, как 0' 0" 0" ". 1 В соответствии с нашими соглашениями ') все эти выражения являются термами, т.
е. Мы будем допускать подстановку их вместо свободных индивидных переменных. Выражения, получающиеся из символа 0 в результате однократного или повторного навешивания штриха, мы будем — несколько видоизменяя употреблявшуюся нами в гл. 11 терминологию з) — называть ц и ф р а м и. Введение этих фигур вместо ранее называвшихся цифрами фигур 1, 11„ 111 ') См гл У с 236 л) См.
с. 46. 1гл. чг нАчАлА Ариюметики 272 онщелогическАя чАсть докАЗАтельстВА 273 1 21 имеет то преимущество, что порождающая операция, которая иаображается прибавлением единицы, теперь будет более четко отличаться от исходного объекта «). Конечно, это преимущество было бы достигнуто и в том случае, если бы мы стали использовать знаки и все же, учитывая дальнейшее построение формализма, целесообразно — если мы хотим получить формулы привычного вида — начать не с 1, а с О. Особо заметим, что с нулем не следует связывать каких-либо представлений о «Ничто»; символ О будет всего лишь формальным представителем некоторого определенного исходного объекта. На этом мы и закончим комментарий к нашей символике. Относительно же введенных нами аксиом заметим следующее. Три аксиомы для символа (мы будем обозначать их посредством (<,), (<г) и ( а)) характеризуют отношение а < Ь как отношение порядка, которое, в частности, имеет место между а и а'.
Две последние формулы а' ~ О а' = Ь' — ь а = Ь соответствугот двум аксиомам из числа тех пяти, с помощью которых Пеано дал свою характеризацню натурального ряда 2). Свои аксиомы Пеано изобразил с помощью логической символики; одна из них является формулировкой принципа полной индукции, который мы обсудим впоследствии ').
Остальные выглядят следующим образом: Нуль есть число. Если а — число, то а' также явллется числом. 11в а' =- Ь' следует а = Ь. Д'ля всякого а а' ~ О. Заметим, что в этой системе аксиом понятие ч и с л а совпадает с понятием эл е м е н т а и н д и в и д н о й о б л а с т и, так ') Эту порождающую опсрзцпю з математике обычно обозначают посродстзом «+1ю Этот способ обозязчеппй имеет тот недостаток, что в пом но находят должного отражения рззяычпе з попятпях между «а + 1», с одной стороны, кап числом, следующим за а, и, с другой стороны, пая суммой а и 1. ') Р з з и о 6. Рогьчп!з»1о Мз«Ьегоаг(со.— Ей.
»'.— Тойпо, 1908, 11„ 1 1, р. 27. В первой редакции этой системы зыспом, опубликованной з статье; Р с з и о С. АгПЬжеысоз рг(пс)р(а почз юс«Ьо«(о ехроз(га.— Тот(по, 1908, аксиомы равенства з пх арифметической специализации пылючаются и снстему аксиом. Это оказалось возможным ввиду того, что з зрпфмзтпкс аыспоиы равенства [1,) и (1,) могут быть заменены боя»о специализированными апспома«т. Позднее ( з гл. Ч11) мы установим, что зта возможность является следствием одной теоремы общего характера о зозмо>ппостя замены аксиом равенства зксяоиамя более специального типа.
') См. с. 324. что нам не нужно вводить особый основной предикат б ы т ь ч и с л о и; наоборот, формализация двух аксиом Нуль есть число и Если а — число, то а' также является числом достигается уже в результате введения символов О и штриха в сочетании с правилом подстановки вместо индивидных переменных. Две остальные аксиомы формализуются посредством наших формул а' = Ь вЂ” а = Ь, которые мы будем называть аксиомами Пеано (Рг) и (Р,).
Из формулы (Рг) контрапоаицией получается формула а~ Ь -э. а'ФЬ'. Импликация а=Ь-ьа'=Ь', обратная к (Р ), получается в соответствии с общей процедурой применения аксиомы равенства к функциональным знакам (ее мы налагали в связи с общими разъяснениями по поводу функцио- нальных знаков ')). Подытожим еще раз систему пап«их аксиом: (12) а=а, (" 2) а = Ь -+- (А (а) — »- А (Ь)), (<1) -1 (а <а) (» г) а < Ь дг Ь < с -+ а <с, ( ) а <а', (Р,) а ~0, (Рг) а =Ь вЂ” »а=Ь.
5 2. Общелогическая часть доказателъства непротиворечивости 1. Выбор ааключительной формулы; исключение связанных переменных; разложение доказательства на нити. Нам нун«но будет установить непротиворечивость этой системы. Для того чтобы сузить нашу задачу, мы вспомним замечание, сделанное в конце гл. 1Н. Мы выяснили там, что для установления ') См.
с. 238. 18 д. 1'заьсзрт, и. Берыайс ОБЩЕЛОГИЧЕСКАЯ ЧАСТЬ ДОКАЗАТЕЛЬСТВА 2 2) Йгл. чъ 275 ИАЧАДА АгиФметики 274 непротиворечивости какого-либо формализма достаточно обнаружить невыводимость в нем какой-нибудь определенной формулы. С другой стороны, ясно, что если формализм непротиворечив, то отрицание любой выводимой в нем формулы должно быть невыводимым. Так, в частности, формула ОФО, являющаяся отрицанием выводимой иэ (»») формулы 0=0, должна быть певыводимой. Таким образом, задача установления непротиворечивости нашего формализма сводится к тому, чтобы доказать невыводнмость в нем формулы 0 Ф О. Если вывод какой-либо формулы иэ определенных аксиом (с помощью логического исчисления) назвать ее д о к а з а т е л ьс т в о м, то наша задача будет состоять в том, чтобы установить невозможность какого-либо доказательства формулы 0 чь 0 в рассматриваемой системе аксиом.
Мы разобьем это рассуждение на две части. Сначала мы покажем, что доказательство формулы ' 0~0 в нашей системе аксиом не может быть осуществлено беэ использования свяеанных переменных, а эатем рассмотрим и общий случай. Итак, сначала допустим, что у нас имеется доказательство формулы О:ы: О в нашей системе аксиом и что связанные переменные в нем не встречаются. Тогда в роли исходных формул будут фигурировать только тождественные формулы исчисления выскаэываний и формулы (У»)» (Ув), (()» ((2)» ((з), (Р»), (Рг), а в качестве единственной схемы — схема заключения. Таким обраэом, рассматриваемое докаэательство состоит иэ последовательности формул такой, что для каждой ее формулы имеет место один из следующих трех случаев: 1. Эта формула является тождественной формулой исчисления высказываний или одной иа наших аксиом.
2. Эта формула совпадает с какой-либо из предыдущих формул рассматриваемой последовательности илн получается из нее в реэультате подстановки. 3. Эта формула является результирующей формулой какой- либо схемы заключения. Теперь представим себе, что у нас имеется докааательство такого рода с заключительной формулой 0 ~ О. Над этим доказательством мы последовательно, друг эа другом, выполним две операции, которые мы назовем раэложением этого доказательства на нити и исключением свободных переменных.
Раэложение докагательства на нити производится следующим образом. Мы просматриваем докаэательство в обратном направлении, начиная с эаключительной формулы 6. Рассмотрим эту Формулу с целью выяснения, какая из трех перечисленных выше воэможностей имеет для нее место. Первая возможность — быть тождественной формулой или аксиомой — реалиэоваться не может. Мы можем также отвлечься и от возможности быть повторением какой- нибудь ранее полученной Формулы, так как в этом случае мы могли бы закончить наше доказательство раньше. Но может случиться, что формула 6 получается в результате подстановки иэ формулы, полученной ранее, или что она является результирующей формулой какой-нибудь схемы заключения.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
