Если Qn есть n-местная предикатная переменная, a x1,..., xn — предметные переменные, то выражение Qn (x1,..., xn) есть, по определению, атомарная (элементарная) формула. Индекс n у предикатной переменной в атомарной формуле обычно опускается. Содержательно Q (x1,..., xn) означает высказывание, гласящее, что объекты x1,..., xn связаны отношением Q. Формулами считаются атомарные формулы, а также выражения, получаемые из них посредством следующих операций образования новых формул из уже полученных: 1) если j и
— формулы, то (j&
), (j
), (jÉ
) и ùj — также формулы; 2) если j — формула и х — предметная переменная, то
"xj, $xj — формулы. Определением формулы заканчивается описание языка исчисления предикатов.
Вхождение предметной переменной х в формулу j называется связанным, если х входит в часть j вида $xj или "xj или стоит непосредственно после знака квантора. Несвязанные вхождения переменной в формулу называются свободными. Если найдётся хоть одно свободное вхождение х в j, то говорят, что переменная х входит свободно в j или является параметром j. Интуитивно говоря, формула j с параметрами выражает некоторое условие, которое превращается в конкретное высказывание, если (конкретизировав предварительно область объектов) приписать определённые значения входящим в формулу параметрам и предикатным буквам. Связанные же переменные не имеют самостоятельного значения и служат (вместе с соответствующими кванторами) для обозначения общих утверждений или утверждений существования. Если j — формула, а х и у — предметные переменные, то через j(х½у) будет обозначаться результат замещения всех свободных вхождений x в j на y (а если при этом у оказалось на месте х в части формулы вида "y или $y, то следует дополнительно заменить все связанные вхождения у в эту часть на переменную, не входящую в j; это делается для того, чтобы не допустить искажения смысла j при замене х на у).
Пусть j,
, h — произвольные формулы, а
х и
у — предметные переменные. Тогда формулы следующих видов принимаются в качестве аксиом классического исчисления предикатов:
1. (jÉ(
Éh)),
2. ((jÉ(
Éh))É((jÉ
)É(jÉh))),
3. ((j&
)Éj),
4. ((j&
)É
),
5. (jÉ(
É(j&
))),
6. ((jÉh)É((
Éh)É((j
)Éh))),
7. (jÉ(j
)),
8. (
É(j
)),
9. (ùjÉ)(jÉ
)),
10. ((jÉ
)É((jÉù
)Éùj))
11. (j
ùj),
12. ("xjÉj(x/y)),
13. (j(x/y) É$xj).
В исчислении предикатов употребляются след. три правила вывода. 1) Правило вывода заключений: из формул j и (jÉ
) выводится формула
. Два кванторных правила вывода: 2) из формулы (jÉ
), где
не содержит свободно
х, можно вывести (jÉ
"x
); 3) из формулы (jÉ
), где
не содержит свободно
х, можно вывести (
$xjÉ
).
В отличие от других формулировок исчисления (см., например, Логика, раздел Предмет и метод современной логики), здесь j,
и h не принадлежат языку рассматриваемого исчисления, а обозначают его произвольные формулы; поэтому каждая из записей 1—13 есть аксиомная схема, «порождающая» при подстановке вместо греческой буквы некоторую конкретную аксиому; специальных правил подстановки при этой формулировке не надо.
Интуиционистское исчисление предикатов отличается от классического лишь тем, что закон исключенного третьего (аксиома 11) исключается из числа аксиом. Различие двух исчислений отражает различие в их истолкованиях. Истолкование логических связок &,
, É, ù в исчислениях предикатов таково же, как и в соответствующих исчислениях высказываний. Что касается истолкования кванторов, то в классическом исчислении предикатов кванторы трактуются с точки зрения актуальной бесконечности. Точнее, каждая формула получает значение «истина» или «ложь», если определить модель исчисления предикатов, т. е. определить множество объектов, приписать каждой предикатной букве формулы некоторое отношение на этом множестве и приписать всем параметрам формулы некоторые объекты в качестве значений. Формула называется классически общезначимой, если она в любой модели принимает значение «истина». Как показал К.
Гёдель, в классическом исчислении предикатов выводимы все классически общезначимые формулы, и только они. Эта теорема Гёделя и представляет собой точное выражение идеи формализации логики: в классическом исчислении предикатов выводятся все логические законы, общие для всех моделей.
