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

2017-02-04T19:04:19Z

93.185.26.48: /* Коррекция аксиом */

[[Категория: Математическая логика]]

[[Лекция 3 | <<]][[Лекция 5 | >>]]

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

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

=== Язык ===

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

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

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

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

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

(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=
Если некоторое вхождение переменной <tex>x</tex> находится в области действия квантора по переменной <tex>x</tex>, то такое вхождение мы назовем '''связанным'''. Вхождение переменной <tex>x</tex> непосредственно рядом с квантором (<tex>\forall x \dots</tex>) мы назовем '''связывающим'''. Те вхождения переменных, которые не являются связанными или связывающими, назовем '''свободными'''. Формула, не имеющая свободных вхождений переменных, называется '''замкнутой'''.
}}

{{Определение
|definition=
Будем говорить, что переменная <tex>y</tex> свободна для <tex>x</tex> при подстановке в формулу <tex>\psi</tex> (или просто свободна для подстановки вместо <tex>x</tex>), если после подстановки <tex>y</tex> вместо свободных вхождений <tex>x</tex> ни одно ее вхождение не станет связанным.
}}

Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы аксиом исчисления высказываний и дополним их следующими двумя схемами.
Здесь <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>

(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>.

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

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

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

<tex> \frac {(\phi) \rightarrow (\psi)} {(\phi) \rightarrow \forall{x}(\psi)}</tex>
<tex> \frac {(\psi) \rightarrow (\phi)} {\exists{x}(\psi) \rightarrow (\phi)}</tex>

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

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



"Не входит свободно" - это также важный вопрос.
Рассмотрим формулу <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=
Формальная система, составленная из указанного языка, множества аксиом и множества правил вывода, называется '''исчислением предикатов'''.
}}

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

{{Определение
|id=valid
|definition=
Формула в исчислении предикатов общезначима, если она истинна на любом предметном множестве <tex>D</tex>, при любой оценке предикатов, и при
любых оценках свободных индивидных переменных.
}}

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

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

{{Теорема
|statement=
Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо.
|proof= Упражнение.
}}

{{Теорема
|statement=
Теорема о дедукции. Если <tex>A \vdash B</tex>, то <tex> \vdash A \rightarrow B </tex>
|proof=
Доказательство разбором случаев. 3 старых случая те же, добавилось
2 новых правила вывода.
Упражнение.
}}

{{Теорема
|statement=
Исчисление предикатов полно.
|proof=Без доказательства.
}}
===Интерпретация булевых формул с кванторами как игр для двух игроков===

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

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

{{Теорема
|statement=
Дано утверждение: <tex>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)</tex>, где <tex>\{Q_i\}_{i=1}^{n} </tex> является чередующейся последовательностью кванторов <tex>\forall</tex> и <tex>\exists</tex>.
# Если утверждение <tex>P_1</tex> истинно, то у игрока «существует» есть набор ходов, используя который, он может победить.
# Если же утверждение <tex>P_1</tex> ложно, то у игрока «для всех» есть набор ходов, используя который, он может победить.
|proof=
# Выражение <tex>P</tex> истинно. Провернём доказательство по индукции.
#* '''База:''' в <tex>P_1</tex> один квантор.
#*: Если единственный квантор {{---}} «любой», то какой бы параметр не поставил игрок «для всех» утверждение будет истинно по условию теоремы.
#*: Если единственный квантор {{---}} «существует», то, по условию, есть такой параметр, что утверждение будет истинно. Его и подставит игрок «существует», после чего сразу победит.
#* '''Переход:''' теорема верна, когда утверждение <tex>P_1</tex> содержит не более <tex>n-1</tex> квантора, докажем, что она верна и для утверждений, содержащих <tex>n</tex> кванторов.
#*: Пусть первый квантор «существует», тогда <tex>P_1 = \exists x_1 P_2</tex>, где <tex>P_2 = P_2(Q_2, \ldots, Q_n, \Psi(x_1,\dots ,x_n)_{x_1=const})</tex>. По условию теоремы найдётся такой параметр <tex>x_1 = x_{1_0}</tex>, что <tex>P_1</tex> истинно. Но выражение <tex>P_2</tex> истинно и содержит <tex>n-1</tex> квантор, значит, для <tex>P_2</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_1 = x_{1_0}</tex> и полученным набором ходов мы получаем выигрышную стратегию.
#*: Пусть теперь первый квантор «для всех», тогда <tex>P_1 = \forall x_1 \exists x_2 P_3</tex>, где <tex>P_3 = P_3(Q_3, \ldots, Q_n, \Psi(x_1, x_2, \dots ,x_n)_{x_1=const, x_2=const})</tex>. По условию теоремы для любого параметра <tex>x_1</tex> найдётся такой параметр <tex>x_2 = x_{2_0}</tex>, что <tex>P_1</tex> истинно. Но утверждение <tex>P_3</tex> истинно и содержит <tex>n-2</tex> квантора, значит, для <tex>P_3</tex> есть набор ходов игрока «существует», при котором он выигрывает. С выбранным <tex>x_2 = x_{2_0}</tex> и полученным набором ходов мы получим выигрышную стратегию.
# Доказательство существования выигрышной стратегии игрока «для всех» при ложном выражении <tex>\Psi</tex> аналогично.
}}

Викиконспекты - Вклад участника [ru]

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