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


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

20 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ [ГЛ. I
ством 91; тогда ...». С формальной точки зрения этот прием сводится к добавлению формулы 81(6) к числу исходных.
Для формул, не содержащих символа в, этот способ умозаключений — в чем мы убедились с помощью дедукционной теоремы — не открывает никаких новых возможностей в части, касающейся доказательств: любая формула без символа и, выводимая с использованием данного символа и формулы Я (в), будет выводиться и без использования этого символа. Кроме того, для любой формулы 23(0), выводимой с помощью формулы 81(6), можно будет без использования символа в вывести формулу
81 (с) -к 33 (с)
со свободной переменной с, не входящей в формулу 33 (б). При этом искомый вывод будет получаться из вывода формулы 33 (3), если мы символ и всюду заменим переменной с, затем к каждой формуле импликативно присоединим посылку 81 (с), а потом добавим небольшие фрагменты доказательства, необходимые для сохранения структуры вывода (как это делалось при доказательстве дедукционной теоремы "•)).
Таким образом, в силу выводимости формулы 3^31 (?) имеет место полный параллелизм между выводами, производящимися с использованием формулы 4Л (и), и сопоставленными им выводами, не использующими символа 6; при этом каждой строке вывода, представляющей собой формулу 33 (?), сопоставляется некоторая (однозначно определенная — с точностью до выбора не входящей в 33 (3) свободной переменной с) формула
И (с)-»- 93 (с),
а каждой строке вывода, представляющей собой не содержащую символа ? формулу 33, сопоставляется сама эта формула.
Хотя формула 31 (с) ->-33 (с), вообще говоря, дедуктивно и не равна формуле 33 ($), даже если пользоваться формулой 81(6), тем не менее из нее и из Ш (и) путем соответствующей подстановки и применения схемы заключения мы сразу получим 33(6).
Этот результат немедленно распространяется и на формулы с несколькими кванторами существования
не содержащие свободных переменных (но содержащие, быть может, какие-нибудь другие связанные переменные, отличные от
-«!• ••-. ЕС).
Если формула такого рода уже будет иметься в качестве исходной или в качестве выведенной формулы и если мы затем
1) См. т. I, гл. IV, с. 194—196,

 

1 10 20 21 22 23 24 25 26 27 28 29 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 620 630 640 650


Математика