Изменения
Нет описания правки
[[Категория: Математическая логика]]
==Исчисление предикатов==
Выберем множество истинностных значений <tex>V</tex>. Также, выберем некоторое предметное множество <tex>D</tex>.
''n-местным предикатом'' мы назовем функцию из <tex>D^n</tex> в <tex>V</tex>.
Как и раньше, мы ограничимся классическим множеством <tex>V</tex> -- истина и ложь, но оставляем потенциальную возможность его расширить.
Предикаты могут быть 0-местными, в этом случае это хорошо нам известные
пропозициональные переменные, принимающие какие-то истинностные значения,
в происхождение которых мы не вникаем.
Рассмотрим следующий известный пример: каждый человек смертен, Сократ - человек,
следовательно, Сократ - смертен.
Мы можем формализовать это выражение с помощью предикатов: множество <tex>D</tex> - это
будет множество всех существ, <tex>S(x)</tex> - предикат "быть смертным",
<tex>H(x)</tex> - предикат "быть человеком". Тогда фраза в полу-формальном виде
выглядит так:
Для каждого <tex>x</tex>, такого, что <tex>H(x)</tex> верно <tex>S(x)</tex>, поэтому поскольку <tex>H</tex>(Сократ),
значит, что имеет место <tex>S</tex>(Сократ).
Чтобы построить новое исчисление, нам требуется указать 3 компонента: язык,
аксиомы и правила вывода.
# Язык. Добавим к языку исчисления высказываний новые конструкции с предикатами
и получим язык исчисления предикатов. Вот расширенная грамматика:
*<выражение>}&::=&\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}
# Аксиомы.
\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)$. Однако, оно ей не является.
Все аксиомы, порожденные данными схемами в новом языке, мы назовем аксиомами исчисления
предикатов.
# Правила вывода.
Пусть $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}
Теорема о дедукции. Если <tex>A \vdash B</tex>, то <tex> \vdash A \rightarrow B </tex>
\end{theorem}
\begin{proof}
Доказательство разбором случаев. 3 старых случая те же, добавилось
2 новых правила вывода. Упражнение.
\end{proof}
\begin{theorem}
Исчисление предикатов полно.
\end{theorem}
Без доказательства.
<tex>
[[Лекция 3 | <<]][[Лекция 5 | >>]]
