Гильберт, Бернайс - Основания математики. Логические исчисления и формализация арифметики (947375), страница 75
Текст из файла (страница 75)
Таким образом, заменяя в соответствии с процедурой вычисления кан1дый функциональный знак с цифрами соответствующей еь1у цифрой, мы придем к тому, что все встре- 2) См. в. 275 н далее. ~гл чы РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ либо вид у=1- (3 — 6). ающиеся в доказательстве рекурсивно введенные функциональные знаки будут последовательно, друг за другом, исключены. Таким образом, все формулы станут нумерическими, причем нсе исходные формулы перейдут в истинные нумерические формулы. Действительно, для рекурсивных равенств мы уже ранее установили, что при подстановке цифр вместо переменных они переходят в равенства вида Формулы Я,„..., Я2 по предположению верифицируемы, а термы, которые мы подставляем в эти формулы вместо встречающихся в них переменных, после применения операций возврат- него переноса подстановок, устранения переменных и исключения рекурсивно введенных функциональных знаков могут быть только цифрами. Таким образом, зги формулы также перейдут в истинные нумерические формулы.
Теперь остается рассмотреть аксиому (32). Любая формула, получающаяся из нее в результате подстановки и устранения переменных, будет иметь вид а = Ь -Ф- (Я (а) — 3-1Я((Ь)), В ней могут встречаться различные рекурсивно введенные функциональные знаки. В частности, в формуле Я (а) терм а (соответственно в формуле Я (Ь) терм Ь) может быть аргументом такого функционального анака.
Но в любом случае в отношении модификации, которую эта формула испытывает в ходе исключения рекурсивно введенных функциональных знаков, имеет место следующая альтернатива: либо терм а заменяется той же самой цифрой, что и Ь, и тогда формула Я (а) заменяется той же самой формулой, что и Я (Ь); либо термы а и Ь заменяются различными цифрами. Таким образом, получающаяся при этом формула имеет либо вид где у и 1 — различные цифры.
В обоих случаях получающаяся нумерическая формула является истинной. Таким образом, действительно, в результате выполненных операций все исходные формулы нашей фигуры доказательства перейдут в истинные нумерические формулы. Но остальные формулы выводятся из них с помощью повторений и применений схем заключения, а заключительная формула 6 при выполнении этих операций никаких изменений вообще не испытывает, так как она является нумерической с самого начала.
Поэтому совершенно так же, как в ранее рассмотренном нами доказательстве, проведен- ктеРА 363 Ч П НЕКОТОРЫЕ ПОЯСНЕНИЯ ПРИ1ЩИПИАЛЬНОГО ХАРА ключения переменных, получается, что формула6 ном методом исключен является истинной. д пущения рекурсивТем самым мы показ али что и в случае о о м ла, выводимая ных определе й делений всякая нумернческая формула, выв из аксиом (~2)$ о исчисления со свободными перемен средствами элеь1ентаРног ными, Уд б ет истинной. казательства позволяет полУ- ассмот енный нами метод док й ез льтат. рассмотрим произвольч и екоторый б ее о П Резул ' „я,н ел „ им ю казанными средствами формулу, относ ную выводиму у является нумерической. мы не и едполагаем, что она н содержит формульных переМы б ем только считать, что она не о ~.ы уд в я их в нее свободных индивидных переменных.
Пусть вместо входящих в е п оизводится подстановка каких-ли о ци р, и и т о и ла Яь. Тогда эта формула, которая теперь этом получается фор~у~~ . Огда уже вообще не сод р е жит никаких переменных, то К ее выводу мы снова при помощи д у и оп скаемых нами средств. ее в переменных и рекурсивно и именить наш метод исключения пер можем пр введенны фу ц х ф нк напальных знаков. ди в. Единственное отличие по сравб дет состоять в том, что нению с предыдущ р им ассуждением у ф нкциональных зназаключительна р льная фо мула при исключении ункцио б вменениям. Но в любом ков возмож д р но по ве гнется каким-ли о изме Я* либо же сама является истинсл чае получается, что формула а ли о уж чения фу ц ф нк иональных знаков 1Т.
е. в результате ф нкций) она переходит в некоче ний рекурсивно определенных ункций мл. тору о ю истинную нумерическую форьу у. и и любой подстановке цифр вместо свободных Таким образом, при лю ои по ю его вычисления ых переменных в реаультате последующего выч ИНДИВИДНЫХ П Р значений соответствующих тункции ,для рекурсив сивно определенных функций) формула пере ет в и т ну у р н ю н ме ическую формулу. ния нашей нынешней терминологии фор- В порядке расширения наш й к е и е ставляется м л, обладающую такого рода свойством, также пред мулу, о лада ифицируемой.
Тем самым понятие верифиестественным назвать вери„.иц и емоети распространится и на такие Рормулы, в ко цируемоети еденные функциональные знаки, но нет имеются рекурсивно введен о м льных, а также связанных переменных. формуль х, мы можем придать полученному Пользуясь этим термином, мы нами результату следующую формулирою1У: В к формула бев фермульных переменных, выво имая е сякал щью перечисленных выше средств, являе р Д " е Обобщение этого результата, которое непосреддальнеишее о о нами ассмот ения, состоит ственно получается из проведенного нами р р РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ % 1 ] НЕНОТОРые пОяснения пРинципиАльнОГО хАРАктеРА 865 >ГЛ, У>Г в том, что мы можем допустить наличие в формулах Я1, ..., Я> рекурсивно введенных функциональных анаков, если только эти формулы будут верифицнруемыми в смысле только что произведенного обобщения.
Действительно, при этом предположении мы можем быть уверены, что после выполнения тех операций, которыми формулы какого-либо (разложенного на нити) доказательства преобразуются в нумерические формулы, на месте тех формул из числа Я„..., Яб которые используются в качестве исходных формул, будут стоять истинные нумерические формулы. Тем самым мы приходим к констатации следующего факта: Если элементарное исчисление со свободными переменными расш и- рить путем присоединения некоторых рекурсивных определений, верифицируемых (но все же не содержащих связанных переменных) аксиом и аксиомы равенства (! ), то всякая формула, выводимая в полученном таким образом формализме и не содержащая формульных переменных, будет верифицируемой.
Эта редакция полученного нами реаультата позволяет беа труда включить в рассмотрение схему индукции и показать, что в случае добавления этой схемы выводимые формулы, не содержащие формульных переменных, тоже будут верифицирувмыми. Заметим, что вследствие полного исключения из нашего рассмотрения связанных переменных применение схемы индукции также должно быть ограничено такими формулами, в которых связанные переменные не встречаются.
Представим себе, что нам дано доказательство формулы Ж, не содержащей формульных переменных. Пусть это доказательство проведено средствами элементарного исчисления со свободными переменными с добавлением рекурсивных определений, верифицируемых аксиом Я„..., Я> (не содержащих связанных переменных), а также аксиомы (з,) и, кроме того, с использованием схемы индукции.
Тогда, как было показано в гл. >>1, с помощью разложении доказательства на нити и возвратного переноса подстановок мы можем с самого начала устранить формульные переменные, причем, как мы уже отмечали 1), для того чтобы не нарушился вид схемы индукции, необходимо в случае надобности заменить переменную а во второй формуле Я (а) -> Я (а ) атой схемы какой-нибудь другой свободной переменной. Теперь рассмотрим одно из тех применений схемы индукции, которым при поступательном, т. е.
начинающемся с исходных формул доказательства, просмотре его нитей не предшествует никакая схема индукции. Пусть формулы этой схемы (после выпол- !) См. с. 328. пения соответствующих операций) имеют вид 3 (О), 3 (г) — 1- 3 (г'), 3 (1). Для первых двух формул наша фигура доказательства дает вывод беа использования схемы индукции. Но теперь для произвольной цифры А формула 3 (8) с помощью подстановок и повторного применения схемы ааключении может быть выведена из формул 3 (О) и 3 (г) — ~ 3 (г'). Твм самым эта формула может быть выведена с использованием перечисленных средств, но без испольвования схемы индукции. Следовательно, в соответствии со сформулированным нами ранее результатом, опа верифицнруема, т. е.
при каждой подстановке циф вместо встречающихся в ней нндизидных переменных (формульные переменные, по условию, в нее не входят) в результате последующего вычисления аначений соответствующих функций она переходит в истинную нумерическую формулу. Так как скаванное справедливо для любой цифры ), то формула 3 (г) также оказывавтси вернфицируемой. Теперь мы расширим систему аксиом Я„..., Яи добавив к нвй формулу 3 (г). Тогда формулу 3 (1) можно будет получить не по схеме индукции, а непосредственной подстановкой.
Теперь этот прием мы можем по очереди применить ко всем встречающимся в докааательстве схемам индукции. Таким образом, получается, что мы можем избежать применения схемы индукции для вывода формулы !й, добавив к аксиомам Я„..., !й! ряд верифицируемых формул — обозначим их посредством 3„..., 30 В результате формула!ь оказывается выводимой средстчами элементарного исчисления с добавлением рекурсивных определений из аксиом Я>,..., Яп 3„..., 31 и аксиомы (>,).
При этом все аксиомы Я„..., Яп 3„..., 3~ суть верифицнруемые формулы, не содержащие формульных (а также связанных) переменных. Но отсюда, в соответствии с нашим предыдущим результатом, получается, что формула !й является вернфицнруемой. Из доказанной таким образом теоремы, в частности, следует, что если мы положим в основу наших рассмотрений элементарное исчисление со свободными переменными, то рекурсивные определ ния в сочетании с аксиомами равенства, схемой индукции е и какими-либо вернфицируемыми аксиомами никогда не смогу т привести нас ни к какому противоречи>о. 3. Невозможность вывода непротиворечивости рекурсивных определений в качестве следствии непротиворечивости систем предыдущих аксиом; замвнимость арифметических аксиом явными д Д) НЕКОтоРЫЕ ПОЯСНЕНИЯ ПРИНЦИПИАЛЬНОГО ХАРАКТЕРА 667 И'л чп РЕКУРСИННЫЕ ОПРЕДЕЛЕНИЯ 366 определениями; явное определение символа<при помощи соответствующей рекурсивной функции; вывод основных свойств символа <. Если этот результат, а также предыдущие рассуждения, направленные на установление непротиворечивости рекурсивных определений, мы рассмотрим с целью сравнения рекурсивных определений с собственно явными определениями, то заметим здесь следующее существенное различие: присоединение к системе аксиом каких-либо явных определений всегда непротиворечиво, если исходная система является непротиворечивой сама по себе (т.
е. до присоединения этих определений); в противоположность атому, непротиворечивость присоединения к какой-либо системе аксиом рекурсивных определений мы установили только при более сильном предположении, что аксиомы Ям ..., Яд являются вериЯици ракмлди. Это предположение является на самом деле существенным и не может быть ааменено предположением о непротиворечивости исходной системы аксиом. В атом можно убедиться на следудощем простом примере Мы будем исходить из элементарного исчисления со свободными переменными. К логическим символам исчисления высказываний мы присоединим символы =, 0 и символ штриха (снмвол ( мы не присоединяем). В качестве аксиом мы возьмем обе аксиомы равенства "а = а а = Ь-+- (А (а) -~ А (Ъ)), а кроме них,— еще две формулы 0' ~ 0 а" = а.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
