Исчисление предикатов

Исчисление предикатов

Выберем множество истинностных значений [math]V[/math]. Также, выберем некоторое предметное множество [math]D[/math]. n-местным предикатом мы назовем функцию из [math]D^n[/math] в [math]V[/math]. Как и раньше, мы ограничимся классическим множеством [math]V[/math] -- истина и ложь, но оставляем потенциальную возможность его расширить.

Предикаты могут быть 0-местными, в этом случае это хорошо нам известные пропозициональные переменные, принимающие какие-то истинностные значения, в происхождение которых мы не вникаем.

Рассмотрим следующий известный пример: каждый человек смертен, Сократ - человек, следовательно, Сократ - смертен. Мы можем формализовать это выражение с помощью предикатов: множество [math]D[/math] - это будет множество всех существ, [math]S(x)[/math] - предикат "быть смертным", [math]H(x)[/math] - предикат "быть человеком". Тогда фраза в полу-формальном виде выглядит так: Для каждого [math]x[/math], такого, что [math]H(x)[/math] верно [math]S(x)[/math], поэтому поскольку [math]H[/math](Сократ), значит, что имеет место [math]S[/math](Сократ).

Чтобы построить новое исчисление, нам требуется указать 3 компонента: язык, аксиомы и правила вывода.

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

и получим язык исчисления предикатов. Вот расширенная грамматика:

• <выражение>}&::=&\s{<импликация>}\\
• <импликация>}&::=&\s{<дизъюнкция>} | \s{<дизъюнкция>} \rightarrow \s{<импликация>}\\
• <дизъюнкция>}&::=&\s{<конъюнкция>} | \s{<дизъюнкция>} \vee \s{<конъюнкция>}\\
• <конъюнкция>}&::=&\s{<терм>} | \s{<конъюнкция>} \& \s{<терм>}\\

\s{<терм>}&::=&\s{<предикат>} | \s{<предикат>} (\s{<аргументы>}) \\ &|&\exists\s{<переменная><терм>} | \forall\s{<переменная><терм>}\\ \s{<аргументы>}&::=&\s{<переменная>}\\ \s{<аргументы>}&::=&\s{<переменная>,<аргументы>} \end{eqnarray*}\end{bnf}

Добавились 3 новых сущности: \begin{enumerate} \item \emph{индивидные} переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита \item предикаты (они обобщили пропозициональные переменные) \item кванторы: всеобщности ($\forall$) и существования ($\exists$). \end{enumerate}

1. Аксиомы.

\begin{definition}Будем говорить, что переменная $y$ свободна для $x$ при подстановке в формулу $\psi$ (или просто свободна для подстановки вместо $x$), если после подстановки ни одно ее вхождение не станет связанным. \end{definition}

Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы аксиом исчисления высказываний и дополним их следующими двумя схемами. Здесь $x$ - переменная, $\psi$ - некоторая формула, $y$ - некоторая переменная. Запись $\psi[x := y]$ будет означать результат подстановки $y$ в $\psi$ вместо всех свободных вхождений $x$. Пусть $y$ свободно для подстановки вместо $x$.

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

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

Все аксиомы, порожденные данными схемами в новом языке, мы назовем аксиомами исчисления предикатов.

1. Правила вывода.

Пусть $x$ не входит свободно в $\phi$. Тогда рассмотрим следующие дополнительные правила вывода исчисления предикатов:

\begin{tabular}{lll} $\infer{(\phi) \rightarrow \forall{x}(\psi)}{(\phi) \rightarrow (\psi)}$ & $\infer{\exists{x}(\psi) \rightarrow (\phi)}{(\psi) \rightarrow (\phi)}$ \end{tabular}

Добавив эти схемы к схеме для правила Modus ponens исчисления высказываний, мы сможем породить множество правил вывода.

\end{enumerate}

%<<Не входит свободно>> - это также важный вопрос. %Рассмотрим формулу $A(x) \rightarrow A(x)$. Легко показать, что такая %формула общезначима и доказуема. Однако, $(\exists{x}A(x)) \rightarrow A(x)$ %не является общезначимой, если $A(x)$ не общезначима: достаточно взять в качестве %оценки свободной переменной $x$ то значение, на котором $A(x)$ ложна. %Вывод из гипотез также вполне можно расширить на исчисление предикатов.

\begin{definition} Формальная система, составленная из указанного языка, множества аксиом и множества правил вывода, называется исчислением предикатов. \end{definition}

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

\begin{definition}Формула в исчислении предикатов общезначима, если она истинна на любом предметном множестве $D$, при любой оценке предикатов, и при любых оценках свободных индивидных переменных. \end{definition}

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

Обратите внимание на требование отсутствия свободных переменных в допущениях.

\begin{theorem} Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо. \end{theorem}

\begin{proof}Упражнение.\end{proof}

\begin{theorem} Теорема о дедукции. Если [math]A \vdash B[/math], то [math] \vdash A \rightarrow B [/math] \end{theorem}

\begin{proof} Доказательство разбором случаев. 3 старых случая те же, добавилось 2 новых правила вывода. Упражнение. \end{proof}

\begin{theorem} Исчисление предикатов полно. \end{theorem} Без доказательства.

<< >>