Изменения

# 1. Язык. Добавим к языку исчисления высказываний новые конструкции с предикатами

*<выражение>}&::=&\s{<импликация>}\\*<импликация>}&::=&\s{<дизъюнкция>} | \s{<дизъюнкция>} <tex> \rightarrow \s{</tex> <импликация>}\\*<дизъюнкция>}&::=&\s{<конъюнкция>} | \s{<дизъюнкция>} <tex> \vee \s{</tex> <конъюнкция>}\\*<конъюнкция>}&::=&\s{<терм>} | \s{<конъюнкция>} \& \s{<терм>}\\\s{*<терм>}&::=&\s{<предикат>} | \s{<предикат>} (\s{<аргументы>}) \\&|&<tex>\exists\s{</tex> <переменная><терм>} | <tex>\forall\s{</tex> <переменная><терм>}\\\s{*<аргументы>}&::=&\s{<переменная>}\\\s{*<аргументы>}&::=&\s{<переменная>,<аргументы>}\end{eqnarray*}\end{bnf}

# (a) ''индивидные'' переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита (b) предикаты (они обобщили пропозициональные переменные) (c) кванторы: всеобщности (<tex> \forall </tex>) и существования (<tex> \exists </tex>). 2. Аксиомы. \begin{{Определение |definition}=Будем говорить, что переменная $<tex>y$ </tex> свободна для $<tex>x$ </tex> при подстановке в формулу $<tex>\psi$ </tex> (или просто свободна для подстановки вместо $<tex>x$</tex>), если после подстановки ни одно ее вхождение не станет связанным.\end{definition}}

Здесь $<tex>x$ </tex> - переменная, $<tex>\psi$ </tex> - некоторая формула, $<tex>y$ </tex> - некоторая переменная.Запись $<tex>\psi[x := y]$ </tex> будет означать результат подстановки $<tex>y$ </tex> в $<tex>\psi$ </tex> вместо всех свободных вхождений $<tex>x$</tex>. Пусть $<tex>y$ </tex> свободно для подстановки вместо $<tex>x$</tex>.  (11) <tex>\forall{x}(\psi) \rightarrow (\psi[x := \alpha]) </tex>

\begin{tabular}{lll}(11) & $\forall{x}(\psi) \rightarrow (\psi[x := \alpha])$\\ (12) & $<tex>(\psi[x := \alpha]) \rightarrow \exists{x}(\psi)$\end{tabular}</tex>

Заметим, что если взять формулу $<tex>\exists x A(x,y)$</tex>, то по схеме аксиом (11),если игнорировать ограничение на свободу для подстановки, следующее утверждение должно быть тавталогиейтавтологией: $<tex> \forall y \exists x A(x,y) \rightarrow \exists x A (x,x)$</tex>. Однако, оно ей не является.

# 3. Правила вывода.

Пусть $<tex>x$ </tex> не входит свободно в $<tex>\phi$</tex>. Тогда рассмотрим следующие дополнительные

\begin{tabular}{lll}$<tex> \inferfrac {(\phi) \rightarrow \forall{x}(\psi)}{(\phi) \rightarrow \forall{x}(\psi)}$ &</tex>$<tex> \inferfrac {\exists{x}(\psi) \rightarrow (\phi)}{\exists{x}(\psi) \rightarrow (\phi)}$\end{tabular}</tex>

\begin{{Определение |definition}=

\end{definition}}

вместо оценки для переменных $<tex>f_P$ </tex> в исчислении высказываний ввестиоценку для предикатов: для каждого $<tex>k$</tex>-местного предиката $<tex>P^k_n$ </tex> определитьфункцию $<tex>f_{P^k_n}: D^k \rightarrow V$</tex>.

\begin{{Определение |definition}=Формула в исчислении предикатов общезначима, если она истинна на любом предметном множестве $<tex>D$</tex>,

\end}} {{Определение |definition=Пусть имеется некоторое исчисление предикатов с множествомаксиом $A$, и пусть дан некоторый (возможно, пустой) список <tex>\Gamma</tex> ''замкнутых'' формул исчисления предикатов. Тогда, вывод формулы <tex>\alpha</tex> в исчислении с аксиомами <tex>A \cup \Gamma</tex> мы назовем выводом из допущений <tex>\Gamma </tex>, и будем записывать это как <tex>\Gamma \vdash \alpha </tex>.}}

\begin{theorem}{Теорема|statement=

\end{theorem|proof= Упражнение.}}

\begin{theorem}{Теорема|statement=

\end{theorem} \begin{|proof}=

2 новых правила вывода. Упражнение.\end{proof}}

\begin{theorem}{Теорема|statement=

\end{theorem}|proof=Без доказательства.}}