Для построения теории доказательств исчисления предикатов мы начнем со схем аксиом и правила вывода исчисления высказываваний. Конечно, применять эти схемы и правило надо для нового понятия формулы .
К этому добавим две новые схемы аксиом: » xA(x)É A( r )(» -схема) и А( r )É $ xA(x)($ — схема), где r свободно для x в А(х). Это значит, что всякая формула, имеющая один из указанных видов, является аксиомой.
Оределения отношения “В1,…, Вi, является доказательством формулы Вi и понятия “В доказуема” (символически |- В) анало-определению, данному ранее, с точностью до добавления двух новых схем и правил. Определение отношения В1, …, Вi, является выводом (формулы Вi) из А1,…, Am также аналогично ранее данному определению.
Кроме того, будем говорить, что в выводе все (свободные) переменные (формул А1,…, Аm) остаются фиксированными, если » — и $ -правила не применяются ни к какой переменной (в качестве х этого правила), входящей свободно в А1,…,Аm, кроме случаев, когда заключение » — или $ -правила находится, раньше первого вхождения формул A1, …, Am (в качестве допущений) в наш вывод. (Мы можем не обращать внимания на те вхождения А1,…, Аm, которые обосновываются не как допущения.)
Таким образом, говоря, что в выводе Bl, …, Вi из допущений А1, …, Аm все переменные остаются фиксированными, мы имеем в виду следующее: пусть Bk—это первая из формул B1,…, Вi, которая обосновывается как допущение; в противном случае Вk не существует и Вk-1 — это Вi. В части Bl,…,Bk-1 нашего вывода (если она существует) любая переменная может быть переменной х » — или $ — правила (заключение которого принадлежит этой части). В части Bk+1,…, Вi, вывода (если она существует) лишь переменная, не входящая свободно в
A1,…,Аm. Может оказаться переменной х » — и $ — правил (заключёние которого принадлежит этой части). Если имеется вывод В из A1,…,Am, все переменные которого остаются фиксированными, то мы говорим, что В выводима из А1, …,Аm (с фиксированными переменными), и пишем А1, …, Аm |— В. Как правило, в этой книге мы будем опускать условие “с фиксированными переменными”.
Будем говорить, что В выводима из A1, …, Аm при фиксировании всех переменных, кроме xl ,…,xq (или с варьированием разве лишь переменных х1, …, хq, или при xl, …, хq в интерпретации всеобщности), и писать Al,…,Аm |- х1…хq В, если имеет место » < аналогии силу в очевидным стать должно понятия этого ачение>между “|-” и “|=”.