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


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

350 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ. V
лишь некоторым аналогом теоремы Гёделя, так как оно формулируется в совсем других предположениях.
Но во всяком случае заслуживает серьезного внимания та имеющая принципиальное значение мысль, которую Финслер — со ссылкой на существование в достаточно богатых выразительными возможностями формализованных языках дедуктивно неразрешимых предложений —выдвинул здесь на первый план, связав ее с вопросом о непротиворечивости. Он подчеркнул, что доказательство непротиворечивости какого-либо формализма в обычном смысле этого слова еще не дает -никаких гарантий от противоречий, потому что противоречие может заключаться в формальной выводимости отрицания некоторого выразимого в данном формализме, но не выводимого предложения, которое, однако, с содержательной точки зрения может быть признано истинным.
Теорема Гёделя показывает, что это соображение применимо и к формализмам, рассматриваемым в теории доказательств, причем даже в том случае, когда в основу рассмотрения кладется финитная точка зрения. Действительно, возьмем какой-либо формализм F, удовлетворяющий условиям ai) и б*) и содержащий квантор всеобщности, и на основании этой теоремы построим такую одноместную рекурсивную функцию f(m), для которой в случае непротиворечивости этого формализма равенство f([) = О истинно при любой цифре [ и невыводима формула V#(f (я) = 0). Если к исходным формулам этого формализма добавить формулу 1 V*(f (д;) = 0), то полученный формализм Рг — в предположении, что в исходном формализме F действует дедукционная теорема1)—будет обладать тем свойством, что с доказательством не противоречивости F будет получаться и его непротиворечивость. Несмотря на непротиворечивость Fit выводимая в FI формула 1 VA; (f (х) = 0) в данном случае будет изображать отрицание истинного высказывания, и эта непротиворечивость формализма Рг будет утрачена, если мы добавим к Рг в качестве формальной аксиомы изображение некоторого истинного высказывания, которое дается формулой V*(f (я) = 0).
радокс возникающим в таком формализме с необходимостью, а рассматривает его лишь как противоречие, возникающее вследствие недоразумения. При этом под формализмом Финслер понимает нечто совсем отличное от того, что под этим понимается в теории доказательств; а именно, формализм понимается им всего лишь как придание словам, грамматическим формам и составным конструкциям определенных значений, на основе которых для любого конкретно предъявленного текста с помощью надлежащего разбора можно решить вопрос о том, выражает ли он какое-либо содержание (или, соответственно, что именно он выражает). — Из рассуждений Финслера совершенно не вытекает, что формально неразрешимые предложения могут возникать и в формализмах, рассматриваемых в теории доказательств. !) См. т. I, с. 194—199,

 

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 351 352 353 354 355 356 357 358 359 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


Математика