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


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

360 РЕКУРСИВНЫЕ ОПРЕДЕЛЕНИЯ [ГЛ. VII
И все же замена этого рода в том виде, в каком она получается при использовании рекурсивных равенств, не дает нам никакого выражения, которым можно было бы заменить рекурсивно введенный функциональный знак с переменной на месте выделенного аргумента.
В этом и заключается существенное отличие рекурсивных определений от явных, и с этим, в частности, связано то обстоятельство, что доказательство непротиворечивости результата добавления рекурсивных определений к рассмотренным в гл. VI системам аксиом с использованием процедуры замены мы сможем провести только при условии исключения из рассмотрения связанных пере-'менных.
2. Доказательство непротиворечивости добавления рекурсивных определений в рамках элементарного исчисления со свободными переменными; привлечение схемы индукции. Мы сейчас приведем это доказательство. Будут рассматриваться следующие, отличающиеся друг от друга системы аксиом: во-первых, система х)
(Ji), (J,), «О, (<,), (<а), (Pi), (P2),
во-вторых, система (А) 2) и, в-третьих, система (В) 3); при этом нам нужно будет исключить из рассмотрения те аксиомы, которые содержат связанные переменные, т. е. формулу
а ф 0 ->- Зх (х1 = а)
из системы (А) и аксиому индукции из (В).
Все три указанные системы формул обладают тем свойством, что за исключением второй аксиомы равенства (J2) они содержат только такие формулы, в которых не встречается никаких переменных, кроме свободных индивидных, причем все эти формулы являются верифицируемыми.
Что касается логического исчисления, которое мы возьмем, исключив из исчисления предикатов связанные переменные, то оно будет допускать в качестве исходных формул лишь тождественные формулы исчисления высказываний. Будут также допускаться подстановки вместо формульных и вместо свободных индивидных переменных и применение схемы заключения. Это урезанное исчисление мы для краткости будем называть элементарным исчислением со свободными переменными.
Искомое доказательство непротиворечивости результата добавления рекурсивных определений к каждой из трех указанных систем аксиом с исключением связанных переменных будет получено одновременно со следующей, более общей теоремой:
*) См. с. 273.
2) См. с. 322.
3) См. с. 335.

 

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 361 362 363 364 365 366 367 368 369 370 380 390 400 410 420 430 440 450 460 470 480 490 500 510 520 530 540 550


Математика