Избранное
ЭБ Нефть
и Газ
Главная
Оглавление
Поиск +
Еще книги ...
Энциклопедия
Помощь
Для просмотра
необходимо:


Книга: Главная » Гильберт Д.N. Основания математики Теория доказательств
 
djvu / html
 

610 ПРИЛОЖЕНИЕ [V ;
Как и в случае устранения индукции, при устранении квантора существования тоже непосредственно не очевидно, а лишь ', должно быть специально доказано, что происходит действительное упрощение вывода. Во всяком случае, фигура вывода в результате применения операции устранения квантора существования усложняется. Граница концевого фрагмента вывода после ; выполнения этой операции тоже должна быть установлена заново.
Подобно случаю устранения индукции, при устранении квантора существования тоже может быть введено соглашение, устанавливающее, какое из ветвлений должно устраняться в том случае, когда их имеется более одного. С каждым ветвлением связывается, как мы знаем, схема заключения, в которой схо- ( дятся две нити вывода —одна, ведущая от аксиомы, а другая от нижней формулы схемы вывода для квантора существования. В этом случае от нижней формулы схемы к заключительной > формуле всего вывода в целом будет идти некоторая однозначно , определенная нить этого вывода. Мы можем теперь условиться, ', что всякий раз будет производиться устранение того ветвления, у которого указанная нить, ведущая от нижней формулы схемы к заключительной формуле вывода, в рассматриваемом в данный момент концевом фрагменте расположена левее остальных. И если на одной и той же нити лежат несколько ветвлений, то мы будем брать то из них, у которого нижняя формула схемы отстоит от заключительной формулы вывода больше остальных. •'
А теперь, прежде чем приступить к доказательству того, что : операции устранения квантора существования и индукции в опре- '-, деленном смысле дают действительные упрощения, мы должны еще рассмотреть случай, когда к концевому фрагменту вывода не примыкает ни одна схема индукции, а также не выполнено и , предварительное условие проведения операции устранения кван-тора существования. В этом случае у нас имеется фигура вывода, ; в которой к концевому фрагменту не примыкает ни одна схема ~ индукции, а в самом этом фрагменте после вычисления нумери-ческих термов и разделения связанных переменных любая экзистенциальная формула, к которой относится какая-либо аксиома для квантора существования, отлична от всех экзистенциальных формул, к которым относятся какие-либо (граничащие с концевым / фрагментом) схемы для квантора существования. Заметим также, что в соответствии о нашими соглашениями, касающимися разде- ; ления связанных переменных, эта операция делает различными только такие формулы, которые нигде внутри рассматриваемого нами концевого фрагмента (где имеются лишь формулы, истинные в логике высказываний, и схемы заключения) не играют роли одной общей молекулы. Это дает нам возможность с помощью следующих соглашений однозначно придать всем молекулам формул, входящих в концевой фрагмент, значения «истина» и «ложь»:

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 180 190 200 210 220 230 240 250 260 270 280 290 300 310 320 330 340 350 360 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550 560 570 580 590 600 610 611 612 613 614 615 616 617 618 619 620 630 640 650


Математика