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