1632
правки
Изменения
м
test==Исчисление предикатов== Выберем множество истинностных значений <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=Без доказательства.}}
rollbackEdits.php mass rollback
[[Лекция 3 | <<]][[Лекция 5 | >>]]
