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


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

480 ПРИЛОЖЕНИЯ fi
мулу 51 вместо формульной переменной 93 подставляется формула б.
Подстановка вместо формульной переменной с одним или несколькими аргументами производится с помощью так называемой именной формы. Именной формой какой-либо формульной переменной, имеющей аргументы, называется элементарная формула, состоящая из той же самой формульной переменной с попарно различными свободными индивидными переменными в роли аргументов; эти переменные в рассматриваемой ситуации мы называем аргументными переменными данной именной формы.
Вариантом данной именной формы мы называем всякое выражение, получающееся из этой именной формы в результате замены каждой ее аргументной переменной какой-либо свободной или связанной индивидной переменной, а под заменителем для данной именной формы мы понимаем любую формулу, в которой встречаются все аргументные переменные данной именной формы1). *
Для задания подстановки в данную формулу вместо данной формульной переменной с аргументами нужно для какой-либо именной формы этой формульной переменной указать некоторый заменитель. Выполнение подстановки в этом случае заключается в том, что всюду, где в данной формуле встречается какой-либо вариант рассматриваемой именной формы, этот вариант заменяется тем выражением, которое получается из указанного заменителя при помощи тех же самых замен, в результате которых этот вариант получается из рассматриваемой именной формы.
Замечание. Для того чтобы в результате подстановки вместо формульной переменной (с аргументами или без них) или переименования связанной переменной в какой-либо формуле снова получилась формула, необходимо, чтобы в получающемся выражении никакой квантор не оказывался в области действия другого одноименного квантора, или —как мы говорим короче — чтобы не возникало коллизий между связанными переменными.
Кроме подстановок и переименований, в выводах исчисления предикатов для перехода от одной формулы к другой используются также следующие схемы (а) и (0):
Схема (а) состоит в переходе от какой-либо формулы 91->-5В(а), в которой 23 (а) не содержит переменной х, к формуле
*) В первоначальном изложения исчисления предикатов (т. I, гл. IV) термины вариант и заменитель ие вводились. Впервые они появляются в данном томе на с. 291,

 

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 461 462 463 464 465 466 467 468 469 470 480 490 500 510 520 530 540 550 560 570 580 590 600 610 620 630 640 650


Математика