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

<< >>

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

Выберем множество истинностных значений [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]

Интерпретация булевых формул с кванторами как игр для двух игроков

Примечание: данного материала не будет на экзамене. Это перенесенный конспект из "Теории формальных языков".

Во многих теоремах присутствуют утверждения с кванторами «для всех» и «существует». От того, в каком порядке кванторы входят в утверждение, зависит его смысл. Часто оказывается полезным представлять утверждения с кванторами как «игру», в которой участвуют два игрока — «для всех» и «существует». Есть утверждение [math]\exists x_1 \forall x_2 \exists x_3 \dots Q x_n \Psi(x_1,\dots ,x_n)[/math]. Игроки поочередно выбирают значения параметров. Каждый игрок выбирает значение в зависимости от предыдущих ходов. Цель игрока «существует» делать такие ходы, чтобы утверждение [math]\exists x_1 \forall x_2 \exists x_3 \dots Q x_n \Psi(x_1,\dots ,x_n)[/math] получилось истинным. А цель игрока «для всех» делать такие ходы, чтобы итоговое выражение получилась ложным.

Теорема:

Дано утверждение: [math]P_1 = P_1(Q_1, \ldots, Q_n, \Psi(x_1,\dots ,x_n)) = Q_1 x_1 Q_2 x_2 \ldots Q_n x_n \Psi(x_1,\dots ,x_n)[/math], где [math]\{Q_i\}_{i=1}^{n} [/math] является чередующейся последовательностью кванторов [math]\forall[/math] и [math]\exists[/math]. Если утверждение [math]P_1[/math] истинно, то у игрока «существует» есть набор ходов, используя который, он может победить. Если же утверждение [math]P_1[/math] ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.

Доказательство:

[math]\triangleright[/math]

Выражение [math]P[/math] истинно. Провернём доказательство по индукции. База: в [math]P_1[/math] один квантор. Если единственный квантор — «любой», то какой бы параметр не поставил игрок «для всех» утверждение будет истинно по условию теоремы. Если единственный квантор — «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит. Переход: теорема верна, когда утверждение [math]P_1[/math] содержит не более [math]n-1[/math] квантора, докажем, что она верна и для утверждений, содержащих [math]n[/math] кванторов. Пусть первый квантор «существует», тогда [math]P_1 = \exists x_1 P_2[/math], где [math]P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})[/math]. По условию теоремы найдётся такой параметр [math]x_1 = x_{1_0}[/math], что [math]P_1[/math] истинно. Но выражение [math]P_2[/math] истинно и содержит [math]n-1[/math] квантор, значит, для [math]P_2[/math] есть набор ходов игрока «существует», при котором он выигрывает. С выбранным [math]x_1 = x_{1_0}[/math] и полученным набором ходов мы получаем выигрышную стратегию. Пусть теперь первый квантор «для всех», тогда [math]P_1 = \forall x_1 \exists x_2 P_3[/math], где [math]P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2, \dots ,x_n)_{x_1=const, x_2=const})[/math]. По условию теоремы для любого параметра [math]x_1[/math] найдётся такой параметр [math]x_2 = x_{2_0}[/math], что [math]P_1[/math] истинно. Но утверждение [math]P_3[/math] истинно и содержит [math]n-2[/math] квантора, значит, для [math]P_3[/math] есть набор ходов игрока «существует», при котором он выигрывает. С выбранным [math]x_2 = x_{2_0}[/math] и полученным набором ходов мы получим выигрышную стратегию. Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении [math]\Psi[/math] аналогично.

[math]\triangleleft[/math]