Гильберт, Бернайс - Основания математики. Теория доказательств (947376), страница 129
Текст из файла (страница 129)
Рассмотрим этот случай ветвления. Пусть относящаяся к формуле Эу5 (х) аксиома для квантора существования записывается в виде 5(1)-ьЛй5(Х), а относящаяся к этой формуле схема вывода имеет вид 6 (и) Ц) й(йв (е) - 6 В этом случае операция устранения квантора существования заключается в том, что данный вывод формулы Й заменяется некоторым другим, который строится из двух «подвыводов» таких, что один из них дает формулу 5(1)-ь Й, а второй — формулу )5(1)-о Й, и вывода формулы Й из этих двух формуле помощью двукратного применения схемы заключения к формуле (6 (1) Й) ((16 (1) Й) Й). истинной в логике высказываний. Первый из искомых подвыводов получается следующим образом. В выводе верхней формулы нашей схемы для квантора существования мы повсюду заменяем переменную и цифрой В результате этого получается некоторый вывод формулы 5())-»,' -+ 9, из которого мы по правилам исчисления высказываний получаем формулу 5 (1) -~.
(Зй5 (Х) -ь- 9) которая в этом случае оказывается на месте прежней формулы Зй5(й)-+ (1). Тем самым здесь удается сэкономить одно применение схемы для квантора существования. Добавление посылки 5 (1) к формуле Зьй (ь) -ь 9, которая в фигуре нашего вывода является исходной формулой его концевого фрагмента, может быть пронесена сквозь схемы заключений. Действительно, из любой схемы Я Я ~® 4 если в каждой из ее верхних формул, а также и в нижней формуле импликативно добавить одну и ту же посылку ез, получаются две схемы вывода х)-:-~ ~-~-ч.
Я, 3-~-(йб-~~) х)-ь4 6-ь-ь которые с помощью формул (ф ) Я) «((Я еьф) 1 (ф 1 ф) и (ъЗ-ь (Е-Ф%) (а 3.(Е ).а)) истинных в логике высказываний, сводятся к применению схемы заключения'). Все это дает нам некоторый вывод интересующей иас формулы $ (1)-ь-Й. Второй подвывод мы получаем из имеющегося вывода формулы Й, импликативно добавляя к аксиоме $ (1) -ь Зхй (1) посылку )5(1). Так как получающаяся в результате этого формула является истинной в логике высказываний, то тем самым экономится одно использование аксиомы для квантора существования в качестве исходной формулы. Добавленная посылка ) 8 (1) и в этот раз проносится сквозь схемы заключения и таким образом мы получаем некоторый вывод формулы 15(1)-е-Й. Что же касается формулы Й, то она получается, как уже было сказано, из выведенных нами формул й(1)-~-Й и )8(1)-э.Й и из соответствующей формулы, истинной в логике высказываний.
На этом описание операции устранения квантора существования заканчивается. Применением этой операции устраняется одно ветвление: в первом подвыводе исключается относящаяся к формуле Зхв(х) схема вывода для квантора существования, а во втором — относящаяся к Зф(е) аксиома для этого квантора (в ее роли исходной формулы) э), причем в дальнейшем, в процессе использования заключительных формул обоих этих подвыводов данная экзистенциальная формула ЗЕ5(х) больше уже не участвует. Действительно, степень формулы Й, а тем самым и степени обеих этих заключительных формул, как мы знаем, меньше степени д формулы Лгб (й) ь) Это рассуждение соотэетстеуег той часта доказательства дедунпионной теоремы, которая относится н исчислению высказываний; см.
т. 1, с. 194, 1Эб. Однако от этого данззательстзэ оно несколько отличается тем, чю до. полннтельнзя посылка добавляется здесь не псюду, в только е определенной. ведущей к выводимой нами формуле нити вывода. з) Точнее говоря, исключается одно применение рассматриваемой схемы, или соотеетствеино рзссметриеземой аксиомы для ннлнторе сущее~ноннина.
20 д. Гнльберт, П. Бернайс еи ею ПРИЛОЖЕНИЕ Фп докАЗАтелъстео кАльмАРА Как н в случае устранения индукции, при устранении кван- тора существования тоже непосредственно не очевидно, а лишь должно быть специально доказано, что происходит действительное упрощение вывода. Во всяком глучае, фигура вывода в результате применения операции устранения квантора существования усложняется. Граница концевого фрагмента вывода после: выполнения этой операции тоже должна быть установлена заново. Подобно случаю устранения индукции, при устранении кван- тора существования тоже может быть введено соглашение, уста. навливающее, какое из ветвлений должно устраняться в том ' случае, когда их имеется более одного. С каждым ветвлением связывается, как мы знаем, схема заключения, в которой схо- ' дятся две нити вывода †од, ведущая от аксиомы, а другая от нижней формулы схемы вывода для квантора существования.
В этом случае от нижней формулы схемы к заключительной, формуле всего вывода в целом будет идти некоторая однозначно , определенная нить этого вывода. Мы можем теперь условиться,, что всякий раз будет производиться устранение того ветвления, у которого указанная нить, ведущая от нижней формулы схемы . к заключительной формуле вывода, в рассматриваемом в данный момент концевом фрагменте расположена левее остальных. И если иа одной н той же нити лежат несколько ветвлений, то мы будем брать то из них, у которого нижняя формула схемы отстоит от заключительной формулы вывода больше остальных.
А теперь, прежде чем приступить к доказательству того, что операции устранения квантора существования н индукции в опре-,'. деленном смысле дают действительные упрощения, мы должны еще рассмотреть случай, когда к концевому фрагменту вывода ие примыкает ни одна схема индукции, а также не выполнено и, предварительное условие проведения операции устранения кваи- ' тора существования. В этом случае у иас имеется фигура вывода, .: в которой к концевому фрагменту не примыкает ня одна схема . индукции, а в самом этом фрагменте после вычисления нумерических термов н разделения связанных переменных любая экзистенциальная формула, к которой относится какая-либо аксиома для квантора существования, отлична от всех экзистенциальных формул, к которым относятся какие-либо (граничащие с концевым ': фрагментом) схемы для кваитора существования.
Заметим также, что в соответствии о нашими соглашениями, касающимися разде- ' ления связанных переменных, эта операция делает различными только такие формулы, которые нигде внутри рассматриваемого нами концевого фрагмента (где имеются лишь формулы, истинные в логике высказываний, и схемы заключения) не играют роли одной общей молекулы. Это дает нам возможность г помощью следующих соглашений однозначно придать всем молекулам формул, входящих в концевой фрагмент, значения «истина» и «ложын Истинностные значения нумерических равенств будут прежними. Экзистенциальная формула, к которой относится какая-либо аксиома для квантора существования, объявляется истинной, а экзистенциальная формула, к которой относится схема вывода, примыкающая к концевому фрагменту, объявляется ложной. Для остальных экзистенциальных формул их истинностные значения устанавливаются произвольным образом: например, можно всем им приписать значение «истинам Понимание связок исчисления высказываний как истинностных функций сохраняется.
На основании этих соглашений получается, что: 1) нумерические формулы имеют прежние оценки; 2) формулы, истинные в логике высказываний, являются истинными формулами и в смысле нового определения; 3) любая аксиома для квантора существования, фигурирующая в концевом фрагменте, является истинной; то же самое верно и относительно результата ее полного вычисления; 4) нижняя формула любой граничащей с концевым фрагментом схемы вывода для квантора существования является истинной; 5) любая схема заключения с истинными верхними формулами имеет истинную нижнюю формулу.
Если теперь сократить концевой фрагмент, взяв в качестве исходных формул не сами аксиомы для квантора существования, а результаты их полного вычисления (и, значит, опустив стоящие над ними формулы), то получится фигура вывода, все исходные формулы которой будут истинными (формул равенства здесь в качестве исходных формул не будет!), и с помощью схем заключения мы в дальнейшем будем получать только истинные формулы. Следовательно, заключительная формула нашего вывода должна быть истинной в смысле нового определения.
Но так как она является нумерической, то она будет истинной и в прежнем смысле. Таким образом, в данном случае поставленная цель оказывается достигнутой. Заметим, что при новом определении истинности значений молекул, которым мы здесь воспользовались, новые истинностные значения устанавливались лишь для таких молекул, которые являются экзистенциальными формулами, а в остальных случаях брались прежние истинностные значения. Теперь рассмотрим общий случай и покажем, что, отправляясь от любого, построенного в соответствии с нашими правилами вывода, после конечного числа применений операций устранения индукции и квантора существования мы придем к такому выводу, в котором ни одна схема индукции не будет примыкать к концевому фрагменту, а в самом этом фрагменте в после вычисления нумернческих термов и разделения связанных переменных †буд отсутствовать ветвления.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
