Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 85
Текст из файла (страница 85)
В соответствии с этим, например, 6 ((а = Ь)) будет обозначать формулу Зхб (х 70. 11з.з'. 13з ЗР) [а не Лхб(х, 70 11" 13зз)), Заметим, что формулы, о выводи- мости которых идет речь при проверке интересующего нас условия на выводимость, могут быть заданы в виде (Ф) ((и) = 0-Р6((1 (лт) = 0)). Наша лемма с небольшой специализацией может быть сформулирована следующим образом: По любому выводу в (ЕР) формулы Я может быть получен некоторый вывод формулы 6((Я)). (Специализация этой формулировки по сравнению с первоначальной заключается в том, что фигурирующее в 6((Я)) сопоставленное Я арифметическое функциональное выражение берется относительно всех входящих в Я свободных индивидных переменных.) В дальнейшем эта лемма всегда будет применяться в данной формулировке. Применяя эти сокращенные обозначения с фигурными скобками, следует помнить, что выражения а и Ь, вообще говоря, не являются составными частями формулы 6((а=8)), так что не длл любых термов а и Ь из аксиомы равенства (3з) может быть выведена формула а = Ь -Р (6 ((с = а)) -+ 6 ((Г = Ь))).
В то время как оперируя с равенствами в сокращенно-скобочной записи, надо соблюдать особые меры предосторожности, действия над импликациямн в фигурных скобках подчиняются прозрачным правилам. В этом плане мы хотели бы Отметить следующее: Если чо и ч.— формулы из (Е„), то формула 6(((б а)) (6 ((С)) 6((а))) выводима в (ЕР). Действительно, если формуле (Р относительно входящих в нее свободных индивндных переменных сопоставлено арифметическое функциональное выражение э, а формуле ч.— выражение 1, то формуле С-Р~ относительно входящих в нее свободных индивидных переменных сопоставляется арифметическое выражение 80 7з.111. Поэтому формула, выводимость которой надо установить, имеет вид 6 (80 7з ° 1 1~) -Р (6 (а) -Р 6 (1)).
Следовательно, она получается подстановкой из формулы 6(80 7' 11')-Р(6 (з)-ч-8(1)). ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [гл. ч Но для этой формулы вывод получается в силу определения формулы 6' (т, и), которая, как мы знаем, переводима в 6(т, л). Тем самым мы получаем некоторую выводимую схему формул 6 ((С - ч,)) †« (6 ((С)) -« 6 ((хь))), которую мы кратко будем называть первой 6-схемой, Из этой схемы с помощью нашей леммы тут же получается в качестве производной схемы следующая в т о р а я 6-с х е м а." (: — « ч. 6 ((С)) -«6 ((ч.)) В самом деле, согласно лемме, по выводу формулы Ж-«ч. может быть получен вывод формулы 6((( -«'ь)), а Огсюда с помощью первой 6-схемы и схемы заключения мы получаем формулу 6 ((Ф)) — 6((%).
Из второй 6-схемы мы сначала выведем следующее утвержде- .ние: Если ((т) н (,(т) — термы и если равенство ( (т) = 1, (т), а также формула („(т) = 0-«6 ((1, (т) = 0)) выводимы в (2Р), то формула ( (т) = 0-«6 ((! (т) = 0)) тоже выводима в (ХР). В самом деле, из равенства 1(т) = 1! (т) с помощью аксиомы равенства ()а) получается формула (д(т) =0-«((т) =О, которая по второй 6-схеме дает формулу 6((1,(т)=0)) — 6(((( )=О)), а эта формула вместе с формулой 1! (и) = 0-«6 (((а (т) = 0)), выводимость которой мы предполагаем, по правилу силлогизма дает формулу (А(т) =0-«6((((т) =0)).
$2! ФОРМАЛИЗАЦИЯ АД!НФМЕТИЧЕСКОГО ФОРМАЛИЗМА 39! Наконец, эта формула, взятая совместно с формулой ((и) =(А(т), с помощью аксиомы равенства (Яа) дает нам искомую формулу ((т) = 0 «6 ((( (и) = 0)). В силу только что доказанного утверждения, в искомом доказательстве формулы (е) можно ограничится рассмотрением только таких рекурсивных термов ! (и), у которых все входящие в них функциональные знаки, кроме штрих-символа, вводятся с помощью соответствующих рекурсивных равенств; причем все знаки — и непосредственно встречающиеся в ! (т), и те, которые входят в рекурсивные определения непосредственно встречающихся, — являются одноместными или двуместнымн. Устроенные таким образом рекурсивные термы называются нормальными. Сами по себе функциональные знаки, фигурирующие в рекурсивных термах, могут иметь большое число аргументов, равно как и функциональные знаки, вводимые явными определениями в качестве сокращений для термов, образованных суперпозициями рекурсивных функций.
Однако такие явные определения могут быть устранены; а кроме того, как было показано ранее в гл. 'ЧП т. 1'), любая многоместная рекурсивная функция может быть составлена из одноместных и двуместных. Поэтому для любого рекурсивного терма ! можно указать нормальный рекурсивный терм 1, с теми же самыми переменными, для которого в рамках рекурсивной арифметики, а значит, и в формализме (ХР), выводится равенство Следовательно, для любого рекурсивного терма ! (и) с единственной переменной т, если он сам еще не является нормальным, можно указать такой содержащий единственную переменную т нормальный терм (,(т)„что в (У ) выводимо равенство ((и)=(а(т). Если для этого терма 1,(л!) мы сможем вывести формулу (, (т) = 0 — «6 (((, (т) 0)), то, по ранее доказанному, можно будет вывести и формулу ( (т) = О-«6 (Ц (т) = 0)).
Таким образом, наша задача сводится к тому, чтобы для любого нормального рекурсивного терма ( (т) с единственной ') Си. т. !, с. 996 н далее. ВЫХОД ЗА РАМКИ ТВОРИИФЦОКАЗАТЕЛЬСТВ [Гл. у переменной лт установить выводимость формулы 1(лт) =0-ь6((((лт) =О)). С этой целью мы покажем, что, вообще, для любого нормального рекурсивного герма 1 и для любой свободной индивидной переменной с может быть выведена формула 1 = с — 1- Е ((1 = с)). Отсюда, в частною и, получится выводимость формулы ((лд) =с-ьа((1 (т) =с)) для любого нормального рекурсивного терма ((дл) с единственной переменной лд.
Если арифметическое функциональное выражение, сопоставленное терму ((лт) относительно переменной лд, обозначить посредством () (т), то эта формула будет иметь вид ((и) — а ь6(70. 111( ).1Зз з'). Отсюда, в результате подстановки цифры 0 вместо переменной с, мы получим формулу ( (лт) = 0 -ь 6 (70 11» '"" 13'). Но это и есть формула ( (лт) = 0-+ к) ((( (лт) = О)), которую требуется доказать. А теперь, чтобы убедиться, что для любого нормального рекур- сивного терма 1 и для любой свободной индивидной переменной с выводима формула 1 = с.~. 6 ((1 = с)), мы сначала заметим, что эта формула имеет вид 1=с-ь6(70 11' 13' ") где 1, представляет собой арифметическое функциональное выражение, сопоставленное терму 1 относительно всех входящих в него переменных. Если переменная с не входит в 1, то она не входит и в 1, (как мы знаем, 1, содержит те же самые переменные, что и 1), и тогда из рассматриваемой формулы выводима формула ьд (1 Е(70.
110. 13з зд) Обратно: из этой формулы мы для любой свободной переменной с получаем формулу 9)Р0.11 .13 '). ФОРМАЛИЗАПИЯ АРИФМВТИЧЗСКОГО ФОРМАЛИЗМА 393 Таким образом, выводимость формулы 1= с-ь6 ((1=с)) для любой свободной индивидной переменной с равносильна выводимости формулы Чу((=д Е(70.11".
13.з'), где 1т — арифметическое функциональное выражение, сопоставленное терму 1 относительно всех входящих в него переменных. Эту формулу, Однозначно определенную термом 1, мы будем обозначать посредством 5 [1)т). Теперь наша задача может быть сформулирована следующим образом: требуется показать, что для любого наперед заданного нормального рекурсивного терма 1 выводима формула 5 Щ С этой целью мы рассмотрим способ образования нормальных, рекурсивных термов. Любой такой терм, как мы знаем, либо является символом 0 или свободной индивндной переменной, либо получается из какого-либо нормального рекурсивного герма в результате применения штрих-символа, либо представляет собой рекурсивно введенный одноместный или же двуместный функциональный знак, аргументами которого являются нормальные рекурсивные термы.
С процессом порождения каждого такого герма, кроме фактического построения самого герма, связывается еще и определенная упорядоченная последовательность Ж рекурсивных определений, в которой для каждого фигурирующего в 1 функционального знака, отличного от штрих-символа (а может быть, и для каких-нибудь еще функциональных знаков), содержатся относящиеся к нему рекурсивные равенства, причем эти рекурсивные равенства в зависимости от того, какая функция вводится — одноместная или двуместная, имеют либо вид ((0)=а, ((л')=Ь(л, ((л)), либо вид ( (а, О) = о (а), ( (а, л') = Ь (а, л, ((а, л)), где в первом случае термы а и Ь(л, лт), а во втором случае термы о(а) и Ь(а, л, лд) суть нормальные рекурсивные термы, не содержащие других переменных, кроме указанных, и такие, что кроме штрих-символа в них фигурируют только такие функциональные знаки, что относящиеся к ним рекурсивные равенства в последовательности Я предшествуют рассматриваемой рекурсии.
') В атом обозначении прямые скобки указыиают на то, что зависимость формулы 6[0 от терма Ь зообпте тозорн, заключается не только и том, что терм! входит з зту формулу. з з1 ФОРМАЛИЗАПИЯ АРИФМЕТИЧЕСКОГО ФОРМАЛИЗМА зээ 394 ВЫХОД ЗА РАМКН ТЕОРИИ ДОКАЗАТЕЛЬСТВ !ГЛ. Р После сказанного наша задача сводится к доказательству следующих четырех утверждении: 1. Формула 5[0], а также любая формула 5[с] со свободной индивидной переменной г выводимы. 2. Каков бы ни был терм 1, по выводу формулы 5[1] может быть построен вывод формулы 5 [Е].
3. Если 6(с) — терм, г — фигурирующая в нем, но не входящая в 6(0) свободная индивидная переменная, а 1 — терм, не содержащий переменной с, и если формулы 5 [6(с)] и 5[1] выводимы, то выводима также и формула 5[6(1)]. 4. Если а — рекурсивный терм без переменных такой, что формула 5[а] выводима, а Ь(л, с) †так рекурсивныи терм, не содержащий отличных от и и с переменных, что выводима формула 5[Ь (и, с)], и если функциональный знак ! (Л) вводится рекурсивными равенствами ((0)=а и ((л')=Ь(п, 1(л)), то формула 5[((п)] выводима, Если а(а) — рекурсивный терм с единственной переменной а такой, что выводима формула 5[а (а)], если Ь(а, и, с) — рекурсив- ный терм без отличных от а, л н с переменных такой, что выво- дима формула 5[Ь(а, л, с)], и если функциональный знак [(а, л) вводится рекурсивными равенствами [ (а, О) = А (а) и [ (а, и') = Ь (а, п, [ (а, и)), то формула 5 [! (а, и)] выводима.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
