аксиомы и правила вывода.
1. === Язык. === Добавим к языку исчисления высказываний новые конструкции с предикатами
и получим язык исчисления предикатов. Вот расширенная грамматика:
(c) кванторы: всеобщности (<tex> \forall </tex>) и существования (<tex> \exists </tex>).
2=== Аксиомы === {{Определение |definition=Дана некоторая формула <tex>s</tex>. АксиомыБудем говорить, что подстрока <tex>s_1</tex> строки <tex>s</tex> является подформулой, если она в точности соответствует какому-то одному нетерминалув дереве разбора строки <tex>s</tex>.}} {{Определение |definition=Если в формулу входит подформула, полученная по правиламдля кванторов (то есть, <tex>\forall x \alpha</tex> или <tex>\exists x \alpha</tex>), то мы будем говорить, что формула <tex>\alpha</tex> находится в области действия данного квантора по переменной <tex>x</tex>. Также, будем говорить, что любая подформула формулы <tex>\alpha</tex> находится в области действия данного квантора.}}<!--\begin{definition}Если некоторое вхождение переменной $x$ находитсяв области действия квантора по переменной $x$, то такое вхождениемы назовем \emph{связанным}. Вхождение переменной $x$ непосредственно рядом с квантором ($\forall x \dots$) мы назовем \emph{связывающим}.Те вхождения переменных, которые не являются связанными или связывающими, назовем \emph{свободными}. Формула, не имеющая свободных вхождений переменных, называется \emph{замкнутой}.\end{definition} \begin{definition}Будем говорить, что переменная $y$ свободна для $x$ при подстановке в формулу $\psi$ (или просто свободна для подстановки вместо $x$), если после подстановки $y$ вместо свободных вхождений $x$ни одно ее вхождение не станет связанным. \end{definition} -->
{{Определение
|definition=
