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


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

f
590 ПРИЛОЖЕНИЕ [IV
иметь вид
33,G4(z)) + 2l
и
причем одноместная формульная переменная А здесь не должна, входить ни в 91, ни в ЗЗг(Х(г)), а одноместная формульная переменная X не должна входить в 53г (А (г)).
Правило подстановки вместо свободных переменных здесь совершенно такое же, как в формализме (Z). Для связанных переменных действует правило переименования, причем, естественно, формульная переменная всегда переименовывается в формульную же переменную с тем же самым числом аргументов.
При подстановках и переименованиях всякий раз надо следить за тем, чтобы не возникало коллизий между связанными переменными.
Правило добавления явных определений аналогично соответствующему правилу в формализме Я, с тем, однако, упрощением, что в данном случае отпадают все соглашения, относящиеся к функционалам и функциональным переменным.
Дадим ряд кратких указаний относительно применения этого формализма для формализации математических теорий.
Из аксиомы-определения для формулы а = Ь могут быть выведены формулы
Схема индукции получается из аксиомы индукции в качестве производного правила. Формулы
а Ф О -> Зх (х' = а) и а' Ф а
получаются индукцией по а.
Применяя схему для квантора существования ЭХ(1), мы, в частности, получим формулу
Vz (А (г) ~ 3( (г)) -v ЭХ^Уг (X (z) ~ 91 (г)).
Если в нее подставить вместо именной формы А (с) формулу 31 (с), то посылка перейдет в выводимую формулу
в то время как заключение не изменится. Тогда по схеме заключения мы получим формулу
В большинстве формальных систем, в которых имеются связанные предикатные переменные, но нет нашего правила подстановки,

 

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 460 470 480 490 500 510 520 530 540 550 560 570 580 590 591 592 593 594 595 596 597 598 599 600 610 620 630 640 650


Математика