Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 112
Текст из файла (страница 112)
Аналогичным образом можно убедиться в том, что система формул 1 1), 2), 3) тоже представляет собой систему аксиом, достаточную для вывода всех позитивно тождественных формул. Для этого достаточно показать, что формализм, исходными формулами которого являются импликативные формулы исчисления высказываний, а выводимость определяется с помотчью схемы заключения и трех (соответствующих формулам 1 1), 2) и ЗЦ схем формул (3) пн ПРИЛОЖЕНИЕ ПОЗИТИВНО ТОЖДЕСТВЕННЫЕ 1-К.ФОРМУЛЫ а из ДВУХ фоРмУл 4) эх и й[-+ (йб-+ ~) с помощью схем (4) и (5) и схемы заключения следующим образом может быть выведена формула 4)-+.~: Ф-и[тг, (14[-+С)-~-((Я-+-~)-и($-~~)) (Я -«- ~) -з- (Р41 -+ Я;) ~1 - (4О ~). Ф (4О ~))- И(Ф ~)- (Ф ~))- (Ф- Ф- ~))) ((ж- ~) (Ф а))- у (й) ((4О ч)- (Ч)- ч.)), ((4О й)- д а)) (1)) (я! ~)) 3 а м е ч а н и я.
Относительная простота полученных нами доказательств полноты объясняется тем обстоятельством, что понятие позитивно тождественной импликатнвной формулы определяется при помощи условий, формулируемых в терминах выводимости. Еще одна характеристика совокупности позитивно тождественных импликативных формул может быть получена — об этом мы здесь лишь упомянем — из исчисления допри(ение), которое независимо друг от друга разработали Г.
Генцен и С. Яськовский'). 5 2. Позитивно тождественные 1-К-формулы При формализации чистой логики следования с помощью исчисления высказываний нельзя ограничиться рассмотрением одних только импликативных формул, потому что при этом нет возможности иметь сразу несколько посылок у одного заключения. Этот недостаток преодолевается при помощи введенного П, Герцем и детально разработанного Генценом ') исчисления секвенций. ') Оеп[хеп О. [[п1егансьнпхеп ВЬег баа [он[асье Бсй[ейеп.— Ма[Ь. х., 1934, 39, № 2 н 3 (нмеется русский перевод н сб. «Математяческая теория логяческого ямаодам — Мл Фнаматтнз, 1967, с. 9 — 74.-Прям. перев.).— 3 а а 1«отта [г ! Б1.
Оп [Ье гп1еа о1 анрроац[опа !и [от«па! !ой[с. — 3[об[а !ох[се, ч[агахагта, 1934, Яськоаскяй предпринял ато исследование по нннннатнае Я. Лукасеанча. ') Не г ! х Р. ОЬег Ах[огпепауа1епге 1йг Ье![ешке Ба!хата[ел[с. — Ма[В. дпп., !923, 89, № !/2 я 1929, 101, № 4; Оеп1хеп 6. ОЬег б!е Ех[«1епх нпаЬЬапЕ[дег Ах[оп[ел«уз[саге хн нпепб! [сьеп Ба[хауз[ел[ел. — Мабь Апп., 1932, 107, № 3, а также Оп1егапсьнпкеп йЬег баа [ох!«сье Бсщ[ейеп.— Ма[В. х., 1934, 39 (см. прим, перев.
а предмду1дей сноске). 3 сь вводятся с е к в е н ц и и с несколькими посылками десь Я„..., Я„- к). является сокращенной записью выражения ((Я й 6) й 6) -+. (К й 9). Теперь речь пойдет о том, чтобы найти подходящее обобщение понятия позитивно тождественной импликативной формулы для случая 1-К-формул.
При этом в качестве ориентира мы будем иметь в виду, что выражение Я1йЯ«й...йЯк- В должно считаться равнозначным выражению 61 -и (Яа +... -«. (Яа — ~ чт)...), Я Е,й...йа„ выражение — равнозначным конъюнкции («)[-«.е )й й(Я- е ) а выражение Я й (чт й 6) — равнозначным выражению [2[й6)йб. ') См. Приложение 1, с. 458. Другая напрашивающаяся возможность состоит в использовании конъюнкции, с помощью которой составная импликация вида Я1-~.(Я«-1-" -1-(Яа ~)" ) может быть преобразована в одну импликацию Ягй ° ° йЯн — 6 Формулу исчисления высказываний, которая строится из формульиых переменных с помощью одних только символов импликации и конъюнкции, мы будем называть 1-К-формулой.
При записи 1-К-формул мы будем учитывать наше соглашение об экономии скобок. По этому соглашению конъюнкция, являющаяся посылкой или заключением импликации, либо первым членом другой конъюнкции, может не заключаться в скобки '). Например, выражение Яйбй6-+ Юйй б«3 ПРИЛОЖЕНИЕ ПОЗИТИВНО ТОЖДЕСТВЕННЫЕ 1-К-ФОРМУЛЫ $2] пп Р Эти сооб ажения приводят нас к процедуре построения фо- 1-К- о м лы.
мулы, которая будет называться т р а ф аисформац ней данной -ф р улы. Операция эта заключается в следующем: Сначала вычеркиваются все те скоби, конъюнкции. Затем скобки, которые окаймляют ' кции. атем среди импликаций «с конъюнкциями» т. среди таких импликаций к », т.
е. , у которых в посылке или в заключении такие имеется конъюнкция, разыскиваются «самые , у которых каждая импликация, фиг и внутренние», т. е. илн в заключении, уже не со е внут енн и, уже не содержит конъюнкций. Такая самая иутренняя импликация «с конъюнкциями» с шага преобразований) имеет вид » (с учетом первого 61 г йЯЖ 61 й 16« где формулы Я„..., 6 6, и . ° „и ., Э„не содержат вхождений конъюнкции и одно из чисел е] и и но н и и (но не оба одновременно) ься .
еперь каждая из этих нмпликаций заме ется следующей соответствующе й фо й е формулой: заменя- % -»'(Яг-'. ° ° « (Ям -'81) )11 б,[6, (6, ... (г[,„б),)...Ц й(61=(62 .. (6 Е ) )) В результате этого количество импликаций «с конъюнк и ванных шага) процедур на о б аз меньшится. у (выполняем у надо удет повторить нужное число раз до тех пор, пока в рассматриваемой фо м ле все и удет ", будет представлять удет импликативной, либо будет еще опустить скоб нмпликативных фо м л. И ф р у .
, наконец, надо ь ск ки вокруг конъюнкций, Полученная таким образом форму б формацией первоначально заданн й фо мула удет называться т анс- П о' формулы. Р р имер. Трансформацией формулы (А-г-ВАС)-+-А ег Ве«1:] является формула ( ((А-+ В)-+.((А-г-С) «-А))бг((А-г-В)- ((А-+-С)-г-В)) й (( А - В) -» ((А -» С) -» 12)). Трансформацией любой импликативной формулы является сама. Трансформацией конъюнкции ЯЙЗ является кон совпадает с трансформацией импликации 61-~-8, г трансформацией Формулы 6 6— лы, а,— трансформацией формулы 3.. Теперь мы определим понятие позитивно тождественн о й 1-К-фо р м у л ы следующим образом: 1-К-формула будет называться позитивно тождественной, если ее трансформация является позитивно тождественной импликативной формулой или конъюнкцией таких формул.
Таким образом, каждая позитивно тождественная 1-К-формула является тождественно истинной. Действительно, всякая позитивно тождественная импликативная формула (а потому и конъюнкция таких формул) является тождественно истиииои; а кроме того, все операции, из которых состоит переход от формулы к ее трансформации, таковы, что при любом распределении истинностных значений переменных истинностное значение всей формулы в целом остается без изменений.
Для импликативных формул новое понятие позитивной тождественности совпадает с прежним. Аналогия нового понятия с понятием позитивно тождественной импликативной формулы проявляется и в следующих предложениях, которые мы докажем ниже: Всякая непосредственно тождественная 1-Кформула является позитивно тождественной. Всякая формула, выводимая из позитивно тождественных 1-К-формул с помощью подстановок и скемы заключения, является позитивно о]ождественной. Зтн предложения вытекают нз следующей дедуктивной характеризации совокупности позитивно тождественных 1-К-формул: Совокупность всех позитивно тождественных 1-К-формул совпадает с совокупностью формул, которые могут быть получены о использованием следующих двух схем формул: (Зг) (82) и;р«х схем вывода: (Ог) Я- (6- (д) Я, Я-~6 (Ь«) 6- Е, 6- (3- 6) (З«) если ограничиться применением этих схем к 1-К-формулам.
Для доказательства этого утверждения нам потребуется установить два факта. С одной стороны, нужно будет показать, что каждая формула, полученная с помощью применяемых к 1-КФормулам схем (51) — (ь»), является позитивно тождественной, 525 524 ПРИЛОЖЕНИЕ ПП ПОЗИТИВНО ТОЖДЕСТВЕННЫЕ ЬК-ФОРМУЛЫ а с другой стороны, что каждая позитивно тождественная 1-К- формула может быть получена применением к 1-К-формулам схем (3К) — (8К).
Первая часть доказательства получается из следующих утверждений: 1. Трансформация любой 1-К-формулы, имеющей видбйЗ-«Я или 6 й 6-«6, либо сама является непосредственно тождественно импликативной формулой, либо является конъюнкцией таких формул. 2. Трансформация 1-К-формулы Я%6-«Я совпадает с трансформацией формулы Я- (З- (5). 3. Если Я и Я-«З — позитивно тождественные 1-К-формулы, то каждый конъюнктивный член трансформации формулы 8 (или соответственно сама эта трансформация) выводим из позитивно тождественных импликатнвных формул с помощью схемы заключения и, следовательно, сам является позитивно тождественной импликативной формулой.
4. Если Я- Е и Я вЂ” «(6-«6) — позитивно тождественные 1-К- формулы, то каждый конъюнктивный член трансформации формулы Я- 5 (или соответственно сама эта трансформация) является позитивно тождественной импликативной формулой. Утверждения 1, 2 и 3 получаются непосредственно из определений позитивно тождественной 1-К-формулы и трансформации. Утверждение 4 получается с помощью следующей леммы: Если импликативная формула ч.
выводима из импликативных формул Яп ..., 5О~ и еще каких-нибудь позитивно тождественных импликативных формул с помощью одной только схемы заключения, то импликативная формула Ст- (Як- " (Ж1- ~) ) является позитивно тождественной. Эта лемма в свою очередь получается из двух ранее доказанных результатов: результата о том, что совокупность позитивно тождественных импликатнвных формул совпадает с совокупностью формул, получающихся в результате применения к импликативным формулам схем формул 6-«(6-«6) и (6 — «(3-«6))-«((6-«Е)-«(6- Я)) и схемы заключения, и результата о том, что теорема о посылках верна для выводов, осуществляемых с помощью этих схем.
Таким образом, мы убедились, что эти схемы, будучи применены и 1-К-формулам, дают только позитивно тождественные формулы Теперь нам остается показать, что любая позитивно тождественная 1-К-формула может быть получена путем применения этих схем к 1-К-формулам.
Для этого удобно воспользоваться следующими вспомогательными утверждениями: 1) Из схем (8,) и (Ь,) в качестве выводимой схемы получается схема формул Я -«(Э -«6), а из нее с помощью схемы заключения ($,) в качестве производной схемы получается схема вывода Я а с помощью этой схемы и схемы (8,) в качестве производной схемы вывода получается схема силлогизма 6-«8, 9-«Я Из схемы силлогизма в сочетании со схемой (8,) в качестве производной схемы получается схема вывода ф -«Я, ф -э- З, 6 -«(3-» 6) ч)-«Я (эту схему вывода мы будем кратко называть схемой дву- кратного устранения).
Если в эту схему мы вместо ч) подставим выражение Яйб, то, опираясь на (3т) и (8,), получим схему вывода Я -«(6 -« Я) Я~Е- представляющую собой обращение схемы (Ь,). Схема (3У) по "! образцу терминологии, применяемой в исчислении высказываний ), может быть названа схемой разъединения посылок, а ее обращение, оказывающееся производной схемой вывода, есте- ственно назвать схемой соединения посылок. 2) Из схем (Ь,) и (8,) получается схема формул 8-«(6-«6), из которой в сочетании со схемой заключения ($,) получается схема формул Е ~ Р ')С.*.~.*. В.
527 ПРИЛОЖЕНИЕ пн схемы разъединения посылок получится схема формул Я вЂ” «(9 — «6 "УЗ). (8) Эта схема, с одной сто оны 4) дает схему роны, в сочетании со схемой заключе ния пения — схему а с другой стороны, в сочетании со схемой двукра кратного устра- 6-«3, 6-«5 6-«ВЬЮ Из по последней в сочетании со схемами (В ) и (В схему формул и, и (,) мы получаем ЯЬЗ-«ЗЬЯ, а затем, с использованием схемы силлогизма,— м, — схемы формул (Я 44 е) 44 6 -«Я 44 (3 е4 5) Я й (6 й (1) (Я й 3) й4 5, Из утверждений 1) и 2) получается, что для любого де к- тивного формализма, заключающегося в раз ешении п схемы (8 ) — ($4) к каким-либо об аз формул, содержащей импликацию и конъюнкцию (в ка теоремы о п емы о посылках. Действительно, мы уже убедились, что схема формул 6 — «Я выводима с помощью схем (В ) — (Ь ), хем, — ( 4), а схема вывода 6 3 — «Я является производной, так что теперь остается только п ове н выполнение условий касающихся ОснОВных схем ВыВода (54) (54) (54) Дл это непосредственно очевидн о, так как в нашем асположени имеется схема (В4).
Для схем (8 ) (5 заключается в том, что до ж б м, и,) упомян тое л ны ыть производными схемы вывода у условие 'Л (6 Е), ж (' (6 6)) ч)-«(Я-«гг) н Ф (г(х е я) !)3-«(6- (Э-«и))' ПОЗИХИВНО ТОЖДЕСТВЕННЫЕ !.К-ФОРМУЛЫ для первой из них это получается из схемы (54) в сочетании со схемами соединения и разъединения посылок, а для второй — тоже с помощью схем соединения и разъединения посылок, взятых В сочетании со схемой формул (г(х:з)ая яа(еаб) и со схемой силлогизма.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
