Вопрос 9: Исчисление предикатов. Правила вывода на основе исчисления предикатов.

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

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

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

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

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

Язык

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

• <выражение> ::= <импликация>
• <импликация> ::= <дизъюнкция> | <дизъюнкция> $\rightarrow$ <импликация>
• <дизъюнкция> ::= <конъюнкция> | <дизъюнкция> $\lor$ <конъюнкция>
• <конъюнкция> ::= <терм> | <конъюнкция> $\land$ <терм>
• <терм>::= <предикат> | <предикат> (<аргументы>) | $\forall$ <переменная><терм> | $\exists$ <переменная><терм>
• <аргументы> ::= <переменная>
• <аргументы> ::= <переменная>,<аргументы>

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

1. индивидные переменные - мы будем записывать их маленькими латинскими буквами из начала алфавита
2. предикаты (они обобщили пропозициональные переменные)
3. кванторы: всеобщности ($\forall$) и существования ($\exists$).

Аксиомы

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

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

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

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

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

(11) $\forall x (\psi) \to (\psi[x := \alpha])$

(12) $(\psi[x := \alpha]) \to \exists x (\psi)$

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

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

$\forall x(\psi) \to (\psi[x := \alpha])$

$\psi := \exists a \neg 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))$

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

$\exists a (\lnot P(a) = P(a))$

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

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

Правила вывода на основе исчисления предикатов

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

$\frac {(\psi, \psi) \rightarrow (\phi)} {\phi}$

$\frac {(\phi) \rightarrow (\psi)} {(\phi) \rightarrow \forall{x}(\psi)}$

$\frac {(\psi) \rightarrow (\phi)} {\exists{x}(\psi) \rightarrow (\phi)}$