Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 79
Текст из файла (страница 79)
Однако если Р не содержит противоречия, то будет верно и обратное. Действительно, пусть нам дан вывод в Р с номером а формулы с номером и. Если бы условие 6' (а, и) было не выполнено, то для некоторых цифр т и 5, являющихся номерами заключительных формул каких-либо двух выводов в Р с номерами, не превосходящими пт, имело бы место равенство 6 =с(т), т. е. в Р были бы выводимы две формулы, одна из которых является отрицанием другой, т. е.
формализм Р был бы противоречив. С другой стороны, формализм Р* непротиворечив всегда, т. е. независимо от того, непротиворечив ли Р. Действительно, если т) См. с. 355. '! Все требования, предъявляемые здесь к формализму г и к нумерации для него, в следующем параграфе окажутся выполненными для приводимого там арифметического формализма (хн! н для некоторой нумерации етого формализма. 361 ВЫХОД ЗА РАМКИ ТЕОРИИ ПОКАЗАТГЛЬСТВ 1ГЛ Ч бы две формулы, одна из которых является отрицанием другой [и которые, следовательно, имеют номера ~ и е(1)1„обе были выводимы в Р' , то для некоторых двух чисел 1 и 1, являющихся номерами соответствующих доказательств, имели бы место отно- шения ' »(, 1) и 6»(1, е(1)).
Однако по определению выражения 6* эти условия не могут выполняться ни при 1(1, ии при 1(1. вости Р" Это чрезвычайно элементарное доказательство непротивор может быть формализовано в Р выводом формулы речи- 6»(й, и)-Р ) 6»(1, г(п)), и поскольку Р не содержит в себе противоречия, то отсюда, как уже отмечалось выше, следует, что может быть получен этой фо " формулы и в Р . Таким образом, если Р представляет собой » непротиворечивый формализм, удовлетворяющий условиям а,) и б»), то в соответствующем формализме Р» может быть доказана его собственная непротиворечивость.
тео емы Ге еля. е" Но это вовсе не означает какого-либо Опроверже й р р ения второ р еделя. Действительно, эта теорема, как мы помним, по содержит в качестве посылок условия 1, 2 и 3 наложенн пятне выводимости, и мы не показали, что эти условия в Р* выполнены. При ближайшем рассмотрении условие 1 для Р* ока- зывается вообще неопределенным, так как Р» в не определена выводимость одной формулы из другой. Этот недостаток можно было бы устранить. Но в данном слу- чае нам не нужно заниматься этим, так как можно показать, что условие 3 для Р* не будет выполняться если оп фо малнзм Р ф р.
зм непротиворечив. Действительно, условие 3 для Р» утверждает, что если 1(т) — какой-либо рекурсивный терм„а г— номер равенства [(а) =О, то формула ( (т) = Π— )х6* (х, б (г, т)) выводима в Р'. Тем более эта формула должна выводиться в Р. Если, в частности, в роли [(т) взять терм т— — т, то равенство ((т) = О будет выводимо в рекурсивной арифметике а в Р так к , а потому и как этот формализм должен удовлетворять условию а,). Поэтому в Р должна быть выводимой и формула :-)х6» (х, В(г, т)). В подробной записи эта формула имеет вид :-)х[6(х, д(г, т)) й 11иЧВЧТВЧг (и ~хй о~хй6(и, го) й6(о, г) — ~гг(1о))], Из нее н из доказуемой формулы 6(о1, 11)- и .
т ГРАНИЦЫ ИЗОБРАЗИМОСТИ И ВЫВОДИМОСТИ $ н получается формула Эх[6(г, т)<хйЧИЧо(и <хйо(х-+ Угоч'г(6(и, 1о)й6(о, г)-Ргчьг(го)))]. Отсюда (на основании формул для ( и () следует формула '1г'иЧо(и =.В(г, т) йо ="В(г, т)- Чго Рг (6 (и, го) й 6 (о, г)- г чь г (ш))), и из нее в результате перехода от связанных переменных к свободным получается формула А~В(г, т)й1 =.1~(г, т)-1-(6(й, р) й6(1, д)-Рд~г(р)). Следовательно, последняя формула тоже должна быть выводимой в Р.
Между тем, согласно нашему предположению О нумерации, в Р выводима формула т«=.а(г, т). Значит, в Р выводима и формула /г -= т й 1 = т — (6 (Й, р) й 6 (1, д) Р о чь г (р)). Из этой формулы подстановкой терма 1+1 вместо переменной т получается импликация Й ~ й+ 1 й 1 ( й+ 1 — Р (6 (Й, р) й 6 (1, д) -1- д ~ г (р)), а тем самым и формула 6(Й, р) й6(1, д)-Рд~г(р). Из этой формулы, подставив г(р) вместо 11 и воспользовавшись формулой а=а, мы средствами исчисления высказываний получим формулу 6(й, р)-1- ) 6(1, г(р)).
Итак, эта формула выводима в Р. Но на основе наших предположений относительно формализма Р и нумерации для него, было установлено, что в случае непротиворечивости Р эта формула в формализме Р невыводима. Таким образом, если формализм Р непротиворечив, и если для него и для соответствующей нумерации выполняются сформулированные нами условия, то соответствующий формализм Р» удовлетворять условию 3 не может. В дальнейшем речь пойдет о том, чтобы от условной формулировки теорем Геделя перейти к установлению того факта, что невыводимости, утверждаемые в этих теоремах для дедуктивных формализмов определенных типов, имеют место и в случае формализма арифметики, состоящего из системы (Х), аксиом (1»1), (1»з) ФормАлизАция АриФметического ФОРМАлизмА 362 Выход ВА РАмки ТГОРии докАВАтельстВ шл у и (ра) для (х-символа и явных определений, а также для более широких формализмов арифметики.
С этой целью мы рассмотрим соответствующие формализмы на предмет выяснения того, выполняются ли для них предположения этих теорем, т. е. допущения а,) и б,), содержащие в себе более ранние допущения а,) и б,*)'), и условия на выводимость. Тем самым мы возвращаемся к рассмотрению арифметизации метаматематики. й 2. Формализованная метаматематика арифметического формализма а) Описание одного арифметического формализма. Как мы знаем, уже формализм системы (2) дает формализацию арифметики с включением принципа «(ег((пш поп да(пг». Однако в этом формализме рекурсивные функции (за исключением тех из инх, которые могут быть построены с помощью сложения и умножения) непосредственно не изобразимы, а только могут быть представлены в некотором смысле этого слова.
Этот недостаток можно устранить, добавив к системе (7) юправило. В этом случае можно, как было показано в гл. Ч111 т. 1'), явно определить (з-символ таким образом, чтобы формулы ((х,), (ра) н (из) оказались выводимыми с помощью аксиомы индукции; в результате этого мы придем к изображению не только рекурсивных, но и вообще всех тех арифметических функций, которые могут быть определены с помощью принципа наименьшего числа. Изображение рекурсивных функций при этом таково, что соответствующие рекурсивные равенства являются выводимыми формулами. С дедуктивной точки зрения этот формализм вполне удовлетворителен.
Однако арифметизация его метаматематики оказывается довольно неудобной, потому что в соответствии с ыправилом свойство выражения ! Я(х) быть термом зависит от выводимости связанных с формулой Я(с) формул единственности а), так что определение понятия терм оказывается переплетенным с определением выводимости. Этого осложнения можно избежать путем введения вместо с-правила е-формулы, опираясь на которую, е-символ, как известно, может взять на себя роль ь-символа' ), так что, в частности, с помощью е-символа можно будет дать явное определение (!-Символа. Кроме того, в этом случае, как было показано в гл.
11'), возникает возможность устранить аксиому индукции путем добав- ') См. с. 339, 347. ') См. т. 1, с. 43!. а) См. т. 1, с. 463. 4) С, с. 34. з) См. с. 1!6 — !19. ления к формуле А (а) -ь А (Е,А (х)) формулы А (а) - е А (х) чь и' в качестве второй аксиомы для е-символа и взятия в качестве аксиомы формулы а чь 0-ь 6 (а)' = а илн же, вместо нее, формулы а ~ 0 — Лх (х' = а) '). Однако этот формализм по сравнению с формализмом исим- вола имеет тот недостаток, что не каждый его терм без перемен- ных представляет собой формализацию определения какого-либо числа.
Именно, если наряду с е-символом ввести еще один сим- вол В*,Я(х) с соответствующими двумя формальными аксиомами, то нам не удастся вывести равенство к, А (х) = Е,*А (х), по крайней мере, если рассматриваемый арифметический форма- лизм (без е"-символа) непротиворечив'). Тем не менее арифметизация метаматематнкн арифметического ф ализма позволит нам доказать одно наше (сделанное прн обсуждении парадскса Ришара) замечание ) относительно того, а что условие, обозначенное нами посредством в"), в случае ариф- метического формализма может быть удовлетворено.
Это условие утверждает, , во-первых, что прн подходя!цей нумерации свойство з) тп, чтп здесь формула а ~ 0 -ь 6 (а)' = а ма>нет быть заменена формулой а~0- ах(х'=а), проще всего получается нз того, что при наеденни символа 6 (а) пеередстном явного определения 6 (а) = е, (х' = а) Формула а ~ 0-ь 6 (а) ' = а ныаоличея из фармулы а Ф 0 — Эх (х' = а) с помощью е-формулы и схемы (6). з) Н, а предположении непротиноречиапегн рассматриваемого апример, а арифметического чарна формализма можно дозальна просто показать, что добааленне к айсиомам для е-сймаола и еч-енмзола равенств е Яу(х=2 у)=0" н е*„Зу(х=2 у)=(У'" к не приапднт к противоречию.
а) См. с. 333. 364 ВЫХОД ЗА РАМКИ ТЕОРИИ ЛОКАЗАТЕЛЬСТВ 1Гл ч 4 21 ФОРМАЛИЗАШ1Я АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА числа лл быть номером какого-либо терма изображается с помощью некоторого рекурсивного предиката и, во-вторых, что каждый терм, не содержащий свободных переменных, однозначно (хотя, может быть, и не эффективно) определяет некоторое число. Доказательство того, что при подходящем выборе арифметического формализма оба эти требования могут быть удовлетворены совместно, будет проведено с использованием некоторого рекурсивно-арифметического изображения понятия терма (на основе соответствующей нумерации), поскольку наш формализм мы выберем таким образом, чтобы каждый не содержащий аргументов терм представлял собой формализацию однозначного определения некоторого числа.
Последнему из этих требований удовлетворяет формализм 1-правила и не удовлетворяет, как мы только что установили, формализм е-символа. С другой стороны, формализм е-символа дает возможность рекурсивно изобразить понятие терма, в то время как в формализме л-правила этому мешает переплетение понятия герма с условиями на выводимость. Обоим содержащимся в условии в*) требованиям можно удовлетворить, вводя )л-символ не с помощью явного определения, а непосредственно, в качестве основного символа с формулами ()11), (рз) и ()лз), принимаемыми в качестве аксиом, Кроме того, мы должны еще условиться, что, помимо штрих-символа и символов для операций сложения и умножения, будут допускаться только такие функциональные знаки, которые вводятся с помощью каких-либо явных определений.
С точки зрения аксиоматики здесь желательна еще одна модификация. В самом деле, в результате введения формулы ()21) в качестве аксиомы схема (р) становится производной. Но если эту схему опустить, то исчезнет двойственная симметрия исчисления предикатов. Этой трудности не будет, если мы заменим формулу (111) дедуктивно ей равной и аналогичной е-формуле формулой') А (а) - А ((л А (х)), ') В результате этого появится возможность, пользуясь р-снмаолом, явно определить кнанторы, как это было сделано а формализме е-снмзола, н прн этом основные фюрмулы (а) н (Ь) станут выводимыми, а схемы (а) н ((1) пронзаоднымн.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
