Гильберт, Аккерман - Основы теоретической логики (947372), страница 20
Текст из файла (страница 20)
я, мзш. а. 58. Более простои дакзззтеллегвз (ло еих гтр пеоиублпка- В нижеследующих доказательствах независимости мы используем уже установленную непротиворечивость исчисления. Прежде всего мы покажем, что щи!акая нз аксиом а) — б) не является лишней, т. е. что невозможно получить какую-нибудь из этих ансиом из остальных с помощью правил нызола. При этом мы используем показанный ранее фпк> (гл. 1, 1 13), чта з чистом исчислении высказываний никакая нз этих аксиом не яаляется излишней н притом даже в случае присоединения в качестве йополнительной аксиомы еще Х лХ, т. е. ХХ'УХ. Предположим, чта какая-ниоудь из аксиом а) — б) наказана с папашью остальных аксиом и правил нывола исчисления ппеликатов.
Тогда из формул этпго доказательсгва иы удаляем преднкатпые и предметные переменные следующим образом: отбрасываем знаки общноши и сущесп!ования, а каждое прсдикатяое переменное с аргументами заменяем переменным высказыванием Х. При этом преобразпвзнии е) и 1) переходя> в формулу Х вЂ” >Х. Но характер доказательства этим не нарушается. Подстановка по правилам и1) — пЗ) превращается в подстановку исчгюления высказываний или же в простое повторение. Связь формул через схему заключения не нарушается. Правила () и правило переименования превращаются в простое паптпренне.
Таким образом, рассматриваемая формула была бы ныводииа нз осгальных аксиом а) — б) и Х . Х по правилам исчисления высказываний, что противоречит ранее полученным результатам. Йезависимость аксиомы е) мы покажем, доказав, чго все формулы, которые могут быть получены без использования этой аксиомы, имеют харак>ерпое свойство, отсутствующее у этой аксипмы. Именно, если мы видоизменим фарп!улы, заменяя, начиная ванные) сообщены пзи господами Берпзйеои к Арнольдам 1Пппптох.
Доказательстве, приведенные е тексте, воспроизводят хоп мысли Бернайса. Нюпкигииакгпь сиппемы аккипи 13! Уккпк и.чиглкиик предикатпк с самой внутренней области действия, каждую час~ь формулы, имеющую вид (х) 6 (х), (у) 6(у) и т. д., на (х) 6 (х) ',' Х ~~ ~ Х, (у) 6(у) 'д Х ',' Х и т. д., го каждая форьчула, когорая метнет Сыть получена без использования е), переходит снова в формулу, выводимую в исчислении преднкатов, ибо аксиомы а) — б), 1) указанным преобразованием не затрагиваются. Связь формул на основе правил подстановки а), схемы заключения, правила у2) и правила переименования з) не нарушается.
В случае схемы 11) конечная формула 6- (х) 6(х) переходит в форьгулу вида 6' — «(х) З'(х) ~/ Х ьу Х, т. е. в выводимую формулу. Между гемформула(х)Р(х) — «Р(у) превращается в (х) Р (х) ,г Х „Х вЂ” «Р(у), когорую заведомо нельзя вывести, гак как из нее, в силу истинности посылки, получилось бы Р(у) и, далее, через подстановку по правилу аЗ), Е:(у), т. е.
противоречие. Вполне аналогично доказывается независимость 1)'. Вместо того, чтобы заменять часть формулы, имеющую вид (х)6(х), через (х) 6(х) ~/ Хьг Х, будем заменять (Ех) 6(х) на (Ех)6(х)НХНХ. В остальном рассуждения аналогичны предыдущим. Тем же самьш методом устанавливаем и независнмосчь обоих правил 11) и у2). Если мы заменим на этот раз (х) 6(х) в наших формулах через (х) 91(х)б ХйХ, то все формулы, которые ма~ух быть выведены в исчислении предикшпв без использовапия у1), переходят снова и выводиьгые б ормулы. Напрочив, формула (х) (Р(х) ~/ Р(х)), выводимая вз всей системы аксиом, перехог[нт в заведоьго невыводимую фор;пулу (х) (Р(х) 1г Р(хВ б Х йХ. Отсюда следует, что без правила 21) нельзя обойтись.
Путем замены в формулах ь Само собой рсщуиеетсм чтч е незпппспл~естью аксиомы Г1 пк имеет ничего общего тот факт, что знак сущестпоппппп и спстеие ° попом припиппппльпп пч нужен, тпк кап ведь (Пх) я (х) иощие поипьгпть пак сокращение дпи (х) и (х) (ср. с. зб). частей вида (Ех) 6 (х) на (Ех) 6 (х) 'ч' Х ~Г Х получаем аналогично доказательство незанисимости правила у2), так как при этой замене формула (Ех)(Р(х)йР(х)) переходит.в нсвыводимую формулу. Независимость правила и1) еле;гует из того, что без этого правила выводимы только такие щормулы с индивидуальными переменными, которые имеют одну из форм (х)6(х)- 6(у); 6(у)- (Ех)6(х); (х) 6(х) — «(х) 6(х); (Ех) 6(х) — (Ех) 6 (х); (Еа) ((х) 'Д(х) — «6 (а)); (Ег) (6 ( ) -+ (Ех) 6 (х)) илн же получаются из тзких формул путем подстановка на место индивидуальных переменных илги путем переименования связанных переменных.
Ибо аксиомы е) и 1) имеют такую форму, а с помощью правил вывода получаются всегда снова только формулы экого рода. Из э~о~о следует, что, например, формула (х) Р(х)- (Ех) Р(х) без использования и!) не выводима. Независимость правила а2) устанавливаем путем следующего преобразования. Во всех формулах у пере. менных предикатов опускаем те места аргументов, которые заполнены свободными индивидуальными переменными а. Например, Р(х, х) переходит в Р (х), О (а) — в О. При этом преобразовании каждое доказательство, которое выполняется без использования правила подстановки для индивидуальных переменных, переходит снова в выводимую формулу. Но выводимая формула (х) Р(х) — «Р(х) при этом преобразовании переходит в заведомо невыводимую формулу (х) Р(х) Р (вгорое Р янляется здесь переменнымвысказыванием).
Аналогично доказывается независимость правила 'переименования ч), То же самое преобразование, которое мы произвели в формулах в отношении свобод- нога индивидуального переменного а, мы производим теперь в отношении связанного индивидуального пере- 123 Полнота систсиы а>ослон Уотс исчислении ииодиоатоа менного 2. В данном случае нужно еще отбросить знаки (з) и (Ес). При этом опять-таки формула, которая выводила без использования правила переименования, переходит снова в выводимую формулу. Между тем безусловно выводимая формула (з] Р (с) —.
Р (х) переходит в заведомо невыводнмуюформулу Р—. Р(х). Чтобы показать независимость правила иЗ), мы заменяем в формулах каждую часть вида (х) 2((х), (у) 2((у) и т. д., содержаш>ю переменный предикат 6, на (х) 2((х) >, Х'>г Х, (у) 2>! (у) >у Х >у Хи т. д. Тогда каждая форл!ула, которая выводима без использования правила иЗ), переходит снова в выводимую формулу, Между тем это не выполняется для формулы: (х) а (х) а (у). Необходимость схемы заключения следует из того, что без нее ыо>ут быть выведены только формулы вида Тй >у 6.
В самом деле, все аксиомы имеют эту форму, и правила, за исключением (>), снова дают только формулы этого рода. Таким образом, например, формула Х >у Х ие ма>кот быгь выведена без использования правила р). б 1о. Полнота онстсны ннснам В первой главе (! >3) мы подчеркнули, что полноту системы аксиом можно определить двояким образом. Полнота в более строгом смысле слова имеет место в случае, когда присоединение к аксиомам всякой формулы, не выводимой из них, приводит к противоречию. Такой полноты мы >еперь не имеем. Чтобы установить неполноту нашей системы аксиом, достаточно только найти формулу, которая при арифметическом истолковании, йспользовании нами в доказательстве непротиворечивости, тождественно равна нулю, не будучи, однако, следствием из аксиом.
Одной нз таких формул является: (Ех) Р (х) -ь (х) Р (х). Что эта формула не следует из аксиом, представляется весьма правдоподобным >же потому, чго утверждение, которое оаа выражает: оЕсли существует х, для которого истинно Р(х), то Р(х) истинно для всех хо,— заведомо не всегда верно. В самом деле, оно перестает быть верным для произвольных преди. катон Р, как только область индивидуумов содержит более одного элемента. С~рого формальное доказательстно невозможности вывести зту формулу из аксиом проводится следу>о.
щнм обрнзом. Т!рюкде всего мы задаем способ, с помощью ко!орого превращаел! логические формулы а такие, которые сапер>кат только переменные, обозначающие высказывания. С этой целью мы устрш!яем сначала встречающиеся в формуле сноба> пые переменные, связывая их знаками общности, которые ставим перед всей формулой. Затем мы освобождаемся ог кван>оров, заменяя всякий раз,— зто можно делать, например, начиная снаружи,— (х) 2( (х) на л (!) бс й (2), (Ех) 2>((х) на 2((!) >у >д(2)'. В наших (юрму.щх встречаются теперь, наряду с переменньщп высказываниями, высказывания вида Р (!), Р (2): 6 (!. 2) - ..
Все эти различные высказынания мы заменяем еще затем (различными) переменными высказываниями Мы утверждаем теперь, что каждая форм>ла, выводимая из аксиои, после эгого преобразования превращается во всег,',а-истинное сложное высказывание. Докажем зто сначала для аксиом. Для аксиом а) — б) это ясно, так как такое преобразование их не о ! н 2 являются здесь нменаын сабстнсннынн иролнстан. Исключено>с клон>оран салержагсльна сналнгсн, ганны образин, н лаиущснню, чта область ннлнннлууман солар>ннт только элементы ! н 2.
Уэлсе исхисхсиие аредссхатее !та х мси~ схеме хи ахсиси эа грагивает, Аксиома (х) Р (х) Р (у) преобразуется следующим образом: (у) ((х) Р (х) — Р (у)), ((х) Р (х) †« Р (1)) й ((х) Р (х) †« Р'(2)), (Р (!) й Р (2) -« Р (1)) й (Р (1) й Р (2) †« Р (2)), (А й  — А) й (А й  — «В). Последнее выражение действительно представляет собой истинное сложное высказывание.