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


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

50 РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ [ГЛ. VII
пая переменная) входит только на местах, указанных в качестве аргумента, то ?! (а) также будет верифицируемой. Но это вытекает из того, что при указанных предположениях формула ЭД (j) верифицируема для любой цифры §.
Из теоремы о том, что всякая выводимая формула без формульных переменных является верифицируемой, в частности, вытекает непротиворечивость системы (D).
Обратное утверждение, что всякая верифицируемая формула является также и выводимой, может быть получено из свойства 8 процедуры редукции, если воспользоваться выводимостью всякой истинной нумерической формулы системы (D), выводимостью истинных неравенств и сравнений, а также теоремой о частичной редукции 1). Таким образом, в формализме системы (D) верифици-руемость также совпадает с выводимостью.
Из полученных результатов вытекает, что если формула, принадлежащая нашему формализму, не содержит свободных переменных, то либо она сама, либо ее отрицание выводимо. Проверка того, какой именно из этих двух случаев имеет место, производится при помощи процедуры редукции; при этом в случае выводимости соответствующей формулы она дает нам также и способ, позволяющий найти вывод этой формулы.
В частности, если выводимая формула без свободных переменных имеет вид За; Ш(ж), то процедура редукции ведет к нахождению такой цифры j, что будет выводимой формула ?! (§) (это последнее вытекает из теоремы о частичной редукции). Что> же касается формул вида \fx ЭД(а;), не содержащих свободных переменных, то каждая такая формула выводима тогда и только-тогда, когда для каждой цифры j выводима формула ?I(s).
Таким образом, система (D) обладает теми же самыми свойствами полноты, что и системы (А) и (В), и в той же самой мере позволяет производить проверку разрешимости всех формулируемых в ней проблем.
Однако с этим преимуществом связана и определенная недостаточность в отношении изобразительных способностей этого-формализма. Действительно, рассмотрим в формализме системы (D) [подобно тому, как это делалось в системе (В)] формулы, содержащие а в качестве единственной свободной переменной. Каждая такая формула либо сама является своей собственной редукцией, либо переводима в нее. Эту последнюю снова можно перевести (методами, которые использовались в процедуре редукции) либо в истинную формулу 0 = 0, либо в ложную формулу 0 < 0, либо в дизъюнктивную нормальную форму, члены которой суть конъюнкции составных частей вида
*) См. соответствующие соображения в гл. VI, с. 310—314.

 

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 410 420 430 440 450 451 452 453 454 455 456 457 458 459 460 470 480 490 500 510 520 530 540 550


Математика