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


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

40 ИСКЛЮЧЕНИЕ СВЯЗАННЫХ ПЕРЕМЕННЫХ (ГЛ. I
дающий указанными свойствами, мы будем называть нормированным доказательством.
Если в полученном нами нормированном доказательстве формулы (? не будет исходных формул, получающихся (в результате подстановки) из е-формулы, то мы сможем обойтись в нем совершенно без использования е-символов. Действительно, структура нашего нормированного доказательства полностью сохранится, если мы заменим в нем каждый е-терм переменной а, причем, очевидным образом, подстановки достаточно будет производить вместо тех е-термов, которые не являются составными частями каких-либо других е-термов. В результате такой замены мы получим некоторый вывод формулы (? из аксиом $ь . . . , % ? который осуществляется средствами одного только элементарного исчисления со свободными переменными; при этом мы получим вывод и в первоначальном смысле этого слова, так как для каждой исходной формулы, получающейся в результате подстановки из тождественной формулы исчисления высказываний или из одной из аксиом фь . . . , ^ь мы можем дополнительно дописать ее вывод из соответствующей формулы. Итак, утверждение первой е-теоремы в отмеченном выше случае доказано, и, следовательно, нам достаточно показать, что из любого нормированного доказательства произвольной формулы (? могут быть устранены те исходные формулы, которые получаются в результате подстановки в е-формулу.
Мы будем называть такие исходные формулы критическими формулами, причем формулу
мы будем называть критической формулой, связанной с е-т ер MOM eB9l(t>). (При этом е-терм, с которым связана данная критическая формула, мы будем указывать лишь с точностью до обозначения входящих в него связанных переменных.)
б) Гильбертовский подход. Теперь доказательство первой е-теоремы свелось к тому, чтобы показать, что из любого нормированного доказательства могут быть устранены все критические формулы. Метод, которым мы проведем это устранение, восходит к Гильберту. Для изложения этого метода мы сначала рассмотрим частный случай, когда все критические формулы доказательства связаны с одним и тем же е-термом. Пусть эти формулы имеют вид ')
(Я)
*) Здесь явно используется тот факт, что не может быть двух таких различных формул 21 (с) и 58 (с), для которых е ?1 (к) и в 5) (s) были бы одинако-

 

1 10 20 30 40 41 42 43 44 45 46 47 48 49 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


Математика