442
правки
Изменения
→Интерпретация булевых формул с кванторами как игр для двух игроков
[[Категория: Математическая логика]]
[[Лекция 3 | <<]][[Лекция 5 | >>]]
==Исчисление предикатов==
аксиомы и правила вывода.
и получим язык исчисления предикатов. Вот расширенная грамматика:
*<выражение>}&::=&\s{<импликация>}\\*<импликация>}&::=&\s{<дизъюнкция>} | \s{<дизъюнкция>} <tex> \rightarrow \s{</tex> <импликация>}\\*<дизъюнкция>}&::=&\s{<конъюнкция>} | \s{<дизъюнкция>} <tex> \vee \s{</tex> <конъюнкция>}\\*<конъюнкция>}&::=&\s{<терм>} | \s{<конъюнкция>} \& \s{<терм>}\\\s{*<терм>}&::=&\s{<предикат>} | \s{<предикат>} (\s{<аргументы>}) \\&|&<tex>\exists\s{</tex> <переменная><терм>} | <tex>\forall\s{</tex> <переменная><терм>}\\\s{*<аргументы>}&::=&\s{<переменная>}\\\s{*<аргументы>}&::=&\s{<переменная>,<аргументы>}\end{eqnarray*}\end{bnf}
Добавились 3 новых сущности:
{{Определение |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> \begin{tabular}{lll}$\inferfrac {(\phi) \rightarrow \forall{x}(\psi)}{(\phi) \rightarrow \forall{x}(\psi)}$ &</tex>$\infer{<tex> \existsfrac {x}(\psi) \rightarrow (\phi)}{\exists{x}(\psi) \rightarrow (\phi)}$\end{tabular}</tex>
Добавив эти схемы к схеме для правила Modus ponens исчисления высказываний,
мы сможем породить множество правил вывода.
Для задания оценки для выражения в исчислении предикатов необходимо
вместо оценки для переменных $<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>, при любой оценке предикатов, и при любых оценках свободных индивидных переменных. }}
Обратите внимание на требование отсутствия свободных переменных в допущениях.
Исчисление предикатов корректно, т.е. любое доказуемое утверждение общезначимо.
Теорема о дедукции. Если <tex>A \vdash B</tex>, то <tex> \vdash A \rightarrow B </tex>
Доказательство разбором случаев. 3 старых случая те же, добавилось
2 новых правила вывода. Упражнение.\end{proof}}
Исчисление предикатов полно.