1632
правки
Изменения
м
1. === Язык. === Добавим к языку исчисления высказываний новые конструкции с предикатами
2. === Аксиомы. ===
Будем говорить, что переменная Дана некоторая формула <tex>y s</tex> свободна для . Будем говорить, что подстрока <tex>xs_1</tex> при подстановке в формулу строки <tex>\psis</tex> (или просто свободна для подстановки вместо является подформулой, если она в точности соответствует какому-то одному нетерминалу в дереве разбора строки <tex>xs</tex>), если после подстановки ни одно ее вхождение не станет связанным.
Чтобы получить список аксиом {{Определение |definition=Если в формулу входит подформула, полученная по правилам для исчисления предикатовкванторов (то есть, возьмем все схемыаксиом исчисления высказываний и дополним их следующими двумя схемами.Здесь <tex>\forall x\alpha</tex> - переменная, или <tex>\psiexists x \alpha</tex> - некоторая ), то мы будем говорить, что формула, <tex>y</tex> - некоторая переменная.Запись <tex>\psi[x := y]</tex> будет означать результат подстановки <tex>yalpha</tex> находится в <tex>\psi</tex> вместо всех свободных вхождений области действия данного квантора по переменной <tex>x</tex>. Пусть Также, будем говорить, что любая подформула формулы <tex>y</tex> свободно для подстановки вместо <tex>x\alpha</tex>находится в области действия данного квантора.}}
3. === Правила вывода.===
%<Комментарии: <!-- По-моему, в следующем абзаце бред. // Андрей Рыбак --> "Не входит свободно>> " - это также важный вопрос.%Рассмотрим формулу $<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> ложна.%Вывод из гипотез также вполне можно расширить на исчисление предикатов. === Итог ===
[[Лекция 3 | <<]][[Лекция 5 | >>]]
rollbackEdits.php mass rollback
[[Категория: Математическая логика]]
[[Лекция 3 | <<]][[Лекция 5 | >>]]
==Исчисление предикатов==
аксиомы и правила вывода.
и получим язык исчисления предикатов. Вот расширенная грамматика:
(c) кванторы: всеобщности (<tex> \forall </tex>) и существования (<tex> \exists </tex>).
{{Определение
|definition=
}}
{{Определение
|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>
<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>
{{Определение
|definition=
Формальная система, составленная из указанного языка, множества аксиом и множестваправил вывода, называется '''исчислением предикатов'''.
}}
функцию <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>.
}}
|proof=Без доказательства.
}}
