Исчисление предикатов — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Интерпретация булевых формул с кванторами как игр для двух игроков)
(не показаны 22 промежуточные версии 7 участников)
Строка 1: Строка 1:
 
[[Категория: Математическая логика]]
 
[[Категория: Математическая логика]]
 +
 +
[[Лекция 3 | <<]][[Лекция 5 | >>]]
  
 
==Исчисление предикатов==
 
==Исчисление предикатов==
Строка 23: Строка 25:
 
аксиомы и правила вывода.
 
аксиомы и правила вывода.
  
# Язык. Добавим к языку исчисления высказываний новые конструкции с предикатами  
+
=== Язык ===
 +
 
 +
Добавим к языку исчисления высказываний новые конструкции с предикатами  
 
и получим язык исчисления предикатов. Вот расширенная грамматика:
 
и получим язык исчисления предикатов. Вот расширенная грамматика:
  
*<выражение>}&::=&\s{<импликация>}\\
+
*<выражение> ::= <импликация>
*<импликация>}&::=&\s{<дизъюнкция>} | \s{<дизъюнкция>} \rightarrow \s{<импликация>}\\
+
*<импликация> ::= <дизъюнкция> | <дизъюнкция> <tex> \rightarrow </tex> <импликация>
*<дизъюнкция>}&::=&\s{<конъюнкция>} | \s{<дизъюнкция>} \vee \s{<конъюнкция>}\\
+
*<дизъюнкция> ::= <конъюнкция> | <дизъюнкция> <tex> \vee </tex>  <конъюнкция>
*<конъюнкция>}&::=&\s{<терм>} | \s{<конъюнкция>} \& \s{<терм>}\\
+
*<конъюнкция> ::= <терм> | <конъюнкция> & <терм>
\s{<терм>}&::=&\s{<предикат>} | \s{<предикат>} (\s{<аргументы>}) \\
+
*<терм>::= <предикат> | <предикат> (<аргументы>) | <tex>\exists </tex> <переменная><терм> | <tex>\forall </tex> <переменная><терм>
&|&\exists\s{<переменная><терм>} | \forall\s{<переменная><терм>}\\
+
*<аргументы> ::= <переменная>
\s{<аргументы>}&::=&\s{<переменная>}\\
+
*<аргументы> ::= <переменная>,<аргументы>
\s{<аргументы>}&::=&\s{<переменная>,<аргументы>}
+
 
\end{eqnarray*}\end{bnf}
 
  
 
Добавились 3 новых сущности:  
 
Добавились 3 новых сущности:  
\begin{enumerate}
 
\item \emph{индивидные} переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита
 
\item предикаты (они обобщили пропозициональные переменные)
 
\item кванторы: всеобщности ($\forall$) и существования ($\exists$).
 
\end{enumerate}
 
  
# Аксиомы.
+
(a) ''индивидные'' переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита
\begin{definition}Будем говорить, что переменная $y$ свободна для $x$
+
 
при подстановке в формулу $\psi$ (или просто свободна для подстановки
+
(b) предикаты (они обобщили пропозициональные переменные)
вместо $x$), если после подстановки ни одно ее вхождение не станет связанным.
+
 
\end{definition}
+
(c) кванторы: всеобщности (<tex> \forall </tex>) и существования (<tex> \exists </tex>).
 +
 
 +
=== Аксиомы ===
 +
 
 +
 
 +
{{Определение
 +
|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> находится в области действия данного квантора.
 +
}}
  
Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы
+
{{Определение
аксиом исчисления высказываний и дополним их следующими двумя схемами.
+
|definition=
Здесь $x$ - переменная, $\psi$ - некоторая формула, $y$ - некоторая переменная.
+
Если некоторое вхождение переменной <tex>x</tex> находится в области действия квантора по переменной <tex>x</tex>, то такое вхождение мы назовем '''связанным'''. Вхождение переменной <tex>x</tex> непосредственно рядом с квантором (<tex>\forall x \dots</tex>) мы назовем '''связывающим'''. Те вхождения переменных, которые не являются связанными или связывающими, назовем '''свободными'''. Формула, не имеющая свободных вхождений переменных, называется '''замкнутой'''.
Запись $\psi[x := y]$ будет означать результат подстановки $y$ в $\psi$ вместо
+
}}
всех свободных вхождений $x$. Пусть $y$ свободно для подстановки вместо $x$.
 
  
\begin{tabular}{lll}
+
{{Определение
(11) & $\forall{x}(\psi) \rightarrow (\psi[x := \alpha])$\\
+
|definition=
(12) & $(\psi[x := \alpha]) \rightarrow \exists{x}(\psi)$
+
Будем говорить, что переменная <tex>y</tex> свободна для <tex>x</tex> при подстановке в формулу <tex>\psi</tex> (или просто свободна для подстановки вместо <tex>x</tex>), если после подстановки <tex>y</tex> вместо свободных вхождений <tex>x</tex> ни одно ее вхождение не станет связанным.
\end{tabular}
+
}}
  
Заметим, что если взять формулу $\exists x A(x,y)$, то по схеме аксиом (11),
+
Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы аксиом исчисления высказываний и дополним их следующими двумя схемами.
если игнорировать ограничение на свободу для подстановки,  
+
Здесь <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>.
$\forall y \exists x A(x,y) \rightarrow \exists x A (x,x)$. Однако, оно ей не является.
 
  
Все аксиомы, порожденные данными схемами в новом языке, мы назовем аксиомами исчисления
+
(11) <tex>\forall{x}(\psi) \rightarrow (\psi[x := \alpha]) </tex>
 +
 
 +
(12) <tex>(\psi[x := \alpha]) \rightarrow \exists{x}(\psi) </tex>
 +
 
 +
Заметим, что если взять формулу <tex>\exists x A(x,y)</tex>, то по схеме аксиом (11),
 +
если игнорировать ограничение на свободу для подстановки, следующее утверждение должно быть тавтологией:
 +
<tex> \forall y \exists x A(x,y) \rightarrow \exists x A (x,x) </tex>. Однако, оно ей не является.
 +
 
 +
Пример, когда нарушение свободы для подстановки приводит к противоречию:
 +
 
 +
<tex>
 +
\forall{x}(\psi) \to (\psi[x := \alpha]) \\
 +
\psi := \exists a \lnot P(a) = P(b), x := b, \alpha := a \\
 +
\forall b \exists a (\lnot P(a) = P(b)) \to \exists a (\lnot P(a) = P(a)) \\
 +
</tex>
 +
 
 +
Такой предикат <tex>P</tex>, очевидно, существует (если в предметном множестве больше одного элемента). Тогда
 +
 
 +
<tex>
 +
\exists a (\lnot P(a) = P(a))
 +
</tex>
 +
 
 +
Противоречие, следовательно, <tex>z</tex> должен быть свободен для подстановки вместо <tex>\alpha</tex>.
 +
 
 +
Все аксиомы, порожденные данными схемами в новом языке, мы назовем аксиомами исчисления
 
предикатов.
 
предикатов.
  
# Правила вывода.
+
=== Правила вывода ===
  
Пусть $x$ не входит свободно в $\phi$. Тогда рассмотрим следующие дополнительные
+
Пусть <tex>x</tex> не входит свободно в <tex>\phi</tex>. Тогда рассмотрим следующие дополнительные
 
правила вывода исчисления предикатов:
 
правила вывода исчисления предикатов:
  
\begin{tabular}{lll}
+
<tex> \frac  {(\phi) \rightarrow (\psi)} {(\phi) \rightarrow \forall{x}(\psi)}</tex>
$\infer{(\phi) \rightarrow \forall{x}(\psi)}{(\phi) \rightarrow (\psi)}$ &
+
<tex> \frac  {(\psi) \rightarrow (\phi)} {\exists{x}(\psi) \rightarrow (\phi)}</tex>
$\infer{\exists{x}(\psi) \rightarrow (\phi)}{(\psi) \rightarrow (\phi)}$
 
\end{tabular}
 
  
 
Добавив эти схемы к схеме для правила Modus ponens исчисления высказываний,
 
Добавив эти схемы к схеме для правила 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}
+
Рассмотрим формулу <tex>A(x) \rightarrow A(x)</tex>. Легко показать, что такая
 +
формула общезначима и доказуема. Однако, <tex>(\exists{x}A(x)) \rightarrow A(x)</tex>
 +
не является общезначимой, если <tex>A(x)</tex> не общезначима: достаточно взять в качестве
 +
оценки свободной переменной <tex>x</tex> то значение, на котором <tex>A(x)</tex> ложна.
 +
Вывод из гипотез также вполне можно расширить на исчисление предикатов.
 +
 
 +
=== Итог ===
 +
 
 +
{{Определение
 +
|definition=
 +
Формальная система, составленная из указанного языка, множества аксиом и множества правил вывода, называется '''исчислением предикатов'''.
 +
}}
  
 
Для задания оценки для выражения в исчислении предикатов необходимо
 
Для задания оценки для выражения в исчислении предикатов необходимо
вместо оценки для переменных $f_P$ в исчислении высказываний ввести
+
вместо оценки для переменных <tex>f_P</tex> в исчислении высказываний ввести
оценку для предикатов: для каждого $k$-местного предиката $P^k_n$ определить
+
оценку для предикатов: для каждого <tex>k</tex>-местного предиката <tex>P^k_n</tex> определить
функцию $f_{P^k_n}: D^k \rightarrow V$.
+
функцию <tex>f_{P^k_n}: D^k \rightarrow V</tex>.
  
\begin{definition}Формула в исчислении предикатов общезначима, если она  
+
{{Определение
истинна на любом предметном множестве $D$,  
+
|id=valid
при любой оценке предикатов, и при любых оценках свободных индивидных  
+
|definition=
переменных.
+
Формула в исчислении предикатов общезначима, если она истинна на любом предметном множестве <tex>D</tex>, при любой оценке предикатов, и при  
\end{definition}
+
любых оценках свободных индивидных переменных.  
 +
}}
 +
 
 +
{{Определение
 +
|definition=
 +
Пусть имеется некоторое исчисление предикатов с множеством аксиом <tex>A</tex>, и пусть дан некоторый (возможно, пустой) список <tex>\Gamma</tex> ''замкнутых'' формул исчисления предикатов. Тогда, вывод формулы <tex>\alpha</tex> в исчислении с аксиомами <tex>A \cup \Gamma</tex> мы назовем выводом из допущений <tex>\Gamma </tex>, и будем записывать это как <tex>\Gamma \vdash \alpha </tex>.
 +
}}
  
\begin{definition}Пусть имеется некоторое исчисление предикатов с множеством
 
аксиом $A$, и пусть дан некоторый (возможно, пустой) список $\Gamma$ \emph{замкнутых}
 
формул исчисления предикатов. Тогда, вывод формулы $\alpha$
 
в исчислении с аксиомами $A \cup \Gamma$ мы назовем выводом из
 
допущений $\Gamma$, и будем записывать это как $\Gamma \vdash \alpha$.
 
\end{definition}
 
  
 
Обратите внимание на требование отсутствия свободных переменных в допущениях.
 
Обратите внимание на требование отсутствия свободных переменных в допущениях.
  
\begin{theorem}
+
{{Теорема
 +
|statement=
 
Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо.
 
Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо.
\end{theorem}
+
|proof= Упражнение.
 +
}}
  
\begin{proof}Упражнение.\end{proof}
 
  
\begin{theorem}
+
{{Теорема
 +
|statement=
 
Теорема о дедукции. Если <tex>A \vdash B</tex>, то <tex> \vdash A \rightarrow B </tex>
 
Теорема о дедукции. Если <tex>A \vdash B</tex>, то <tex> \vdash A \rightarrow B </tex>
\end{theorem}
+
|proof=
 
 
\begin{proof}
 
 
Доказательство разбором случаев. 3 старых случая те же, добавилось  
 
Доказательство разбором случаев. 3 старых случая те же, добавилось  
2 новых правила вывода. Упражнение.
+
2 новых правила вывода.  
\end{proof}
+
Упражнение.
 +
}}
  
\begin{theorem}
+
{{Теорема
 +
|statement=
 
Исчисление предикатов полно.
 
Исчисление предикатов полно.
\end{theorem}
+
|proof=Без доказательства.
Без доказательства.
+
}}
 
 
 
 
 
 
[[Лекция 3 | <<]][[Лекция 5 | >>]]
 

Версия 22:22, 10 марта 2018

<< >>

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

Выберем множество истинностных значений [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 компонента: язык, аксиомы и правила вывода.

Язык

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

  • <выражение> ::= <импликация>
  • <импликация> ::= <дизъюнкция> | <дизъюнкция> [math] \rightarrow [/math] <импликация>
  • <дизъюнкция> ::= <конъюнкция> | <дизъюнкция> [math] \vee [/math] <конъюнкция>
  • <конъюнкция> ::= <терм> | <конъюнкция> & <терм>
  • <терм>::= <предикат> | <предикат> (<аргументы>) | [math]\exists [/math] <переменная><терм> | [math]\forall [/math] <переменная><терм>
  • <аргументы> ::= <переменная>
  • <аргументы> ::= <переменная>,<аргументы>


Добавились 3 новых сущности:

(a) индивидные переменные --- мы будем записывать их маленькими латинскими буквами из начала алфавита

(b) предикаты (они обобщили пропозициональные переменные)

(c) кванторы: всеобщности ([math] \forall [/math]) и существования ([math] \exists [/math]).

Аксиомы

Определение:
Дана некоторая формула [math]s[/math]. Будем говорить, что подстрока [math]s_1[/math] строки [math]s[/math] является подформулой, если она в точности соответствует какому-то одному нетерминалу в дереве разбора строки [math]s[/math].


Определение:
Если в формулу входит подформула, полученная по правилам для кванторов (то есть, [math]\forall x \alpha[/math] или [math]\exists x \alpha[/math]), то мы будем говорить, что формула [math]\alpha[/math] находится в области действия данного квантора по переменной [math]x[/math]. Также, будем говорить, что любая подформула формулы [math]\alpha[/math] находится в области действия данного квантора.


Определение:
Если некоторое вхождение переменной [math]x[/math] находится в области действия квантора по переменной [math]x[/math], то такое вхождение мы назовем связанным. Вхождение переменной [math]x[/math] непосредственно рядом с квантором ([math]\forall x \dots[/math]) мы назовем связывающим. Те вхождения переменных, которые не являются связанными или связывающими, назовем свободными. Формула, не имеющая свободных вхождений переменных, называется замкнутой.


Определение:
Будем говорить, что переменная [math]y[/math] свободна для [math]x[/math] при подстановке в формулу [math]\psi[/math] (или просто свободна для подстановки вместо [math]x[/math]), если после подстановки [math]y[/math] вместо свободных вхождений [math]x[/math] ни одно ее вхождение не станет связанным.


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

(11) [math]\forall{x}(\psi) \rightarrow (\psi[x := \alpha]) [/math]

(12) [math](\psi[x := \alpha]) \rightarrow \exists{x}(\psi) [/math]

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

Пример, когда нарушение свободы для подстановки приводит к противоречию:

[math] \forall{x}(\psi) \to (\psi[x := \alpha]) \\ \psi := \exists a \lnot P(a) = P(b), x := b, \alpha := a \\ \forall b \exists a (\lnot P(a) = P(b)) \to \exists a (\lnot P(a) = P(a)) \\ [/math]

Такой предикат [math]P[/math], очевидно, существует (если в предметном множестве больше одного элемента). Тогда

[math] \exists a (\lnot P(a) = P(a)) [/math]

Противоречие, следовательно, [math]z[/math] должен быть свободен для подстановки вместо [math]\alpha[/math].

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

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

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

[math] \frac {(\phi) \rightarrow (\psi)} {(\phi) \rightarrow \forall{x}(\psi)}[/math] [math] \frac {(\psi) \rightarrow (\phi)} {\exists{x}(\psi) \rightarrow (\phi)}[/math]

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


Комментарии:


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

Итог

Определение:
Формальная система, составленная из указанного языка, множества аксиом и множества правил вывода, называется исчислением предикатов.


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


Определение:
Формула в исчислении предикатов общезначима, если она истинна на любом предметном множестве [math]D[/math], при любой оценке предикатов, и при любых оценках свободных индивидных переменных.


Определение:
Пусть имеется некоторое исчисление предикатов с множеством аксиом [math]A[/math], и пусть дан некоторый (возможно, пустой) список [math]\Gamma[/math] замкнутых формул исчисления предикатов. Тогда, вывод формулы [math]\alpha[/math] в исчислении с аксиомами [math]A \cup \Gamma[/math] мы назовем выводом из допущений [math]\Gamma [/math], и будем записывать это как [math]\Gamma \vdash \alpha [/math].


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

Теорема:
Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо.
Доказательство:
[math]\triangleright[/math]
Упражнение.
[math]\triangleleft[/math]


Теорема:
Теорема о дедукции. Если [math]A \vdash B[/math], то [math] \vdash A \rightarrow B [/math]
Доказательство:
[math]\triangleright[/math]

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

Упражнение.
[math]\triangleleft[/math]
Теорема:
Исчисление предикатов полно.
Доказательство:
[math]\triangleright[/math]
Без доказательства.
[math]\triangleleft[/math]