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


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

170 е-символ и ЛОГИЧЕСКИЙ ФОРМАЛИЗМ Г гл, in
где t], ..., tc — термы без связанных переменных. Но от любой такой дизъюнкции мы можем с помощью средств исчисления предикатов перейти к формуле (?, так что в общем и целом у нас получится вывод этой формулы средствами одного только исчисления предикатов.
Общее доказательство мы проведем по аналогии с рассмотренным частным случаем. Мы будем исходить из выводимой в исчислении предикатов формулы
(1) V^...V^a1, ..., а
с,
которая получается применением основной формулы (а) (вместе с необходимыми переименованиями связанных переменных) и правила силлогизма. Мы введем в новых функциональных знаков с г аргументами
ft(ci, ..., сс), .... fe(clf .... сс).
Используя эти знаки, мы из формулы (1) подстановкой получим формулу
а из нее, применяя нужное число раз правило (6) 1) и производя подстановку, получим формулу
которая вместе с формулой (? по схеме заключения дает формулу
(2) 3si...3sta(si, .... sr, fi(si, .... sc), ...f,(slf .... sr)).
Таким образом, для формулы (2) у нас имеется вывод с помощью средств исчисления предикатов и е-формулы. Согласно обобщенной первой е-теореме2) по этому выводу можно построить вывод без связанных переменных для некоторой дизъюнкции
(3)
где ti1' ..... t^m' — некоторые термы, не содержащие вхождений е-символа. Этот вывод можно осуществить средствами одного
1) См. т. I, с. 146. ») См. с. 54.

 

1 10 20 30 40 50 60 70 80 90 100 110 120 130 140 150 160 170 171 172 173 174 175 176 177 178 179 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


Математика