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


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

400 ВЫХОД ЗА РАМКИ ТЕОРИИ ДОКАЗАТЕЛЬСТВ [ГЛ. V
утверждения о выводимости формулы
(для любого наперед заданного рекурсивного терма f(m) с единственной переменной т), поскольку мы получаем метод, позволяющий по заданному терму f (m) эффективно строить вывод рассматриваемой формулы. В самом деле, все использованные нами вспомогательные утверждения о тех или иных выводимостях, а также доказательства утверждений 1 — 4 были таковы, что в них либо содержался некоторый способ вывода для формул какого-либо конкретного вида, либо показывалось, как по заданному выводу какой-либо конкретной формулы можно получить вывод какой-либо другой конкретной формулы.
Аналогичное замечание может быть сделано и относительно проведенной нами для формализма (Z^) проверки выполнения первых двух условий на выводимость1).
Общий итог предпринятых выше рассмотрений состоит в том, что для формализма (Z^) оказываются выполненными все предположения второй теоремы Гёделя о неполноте. Таким образом, согласно этой теореме, формула
(х, п) -*- 1 3xS (х, 3-п),
изображающая утверждение о непротиворечивости формализма (2Д), не может быть выведена в (Z^), ибо иначе формализм (Z^) был бы противоречив.
Аналогичным образом можно убедиться, что предположение б2) и добайляемые к нему условия на выводимость выполняются также и для всех таких формализмов, которые, с одной стороны, очерчены достаточно четко, а с другой стороны, включают в себя способы умозаключений исчисления предикатов и обладают средствами, достаточными для изображения понятий и способов умозаключений арифметики, так что в них, в частности, изобразимы рекурсивные функции и соответствующие рекурсивные равенства являются либо аксиомами, либо выводимыми формулами, а кроме того, содержится (в качестве основного правила или производной схемы) схема индукции. Поэтому ко всем таким формализмам применима вторая теорема Гёделя о неполноте.
Как уже упоминалось ранее, условия, фигурирующие в нашей формулировке этой теоремы, могут быть заменены более общими.
В частности, теорема эта — на что указали Гёдель и Крайзел — может быть распространена на формализмы без связанных переменных—например, на рекурсивную арифметику. Для рекурсивной арифметики это вытекает из того, ранее уже отмеченного обстоятельства, что доказательства, устанавливающие выполни-
См. с. 381-383.

 

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 401 402 403 404 405 406 407 408 409 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


Математика