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