Изменения

1. === Язык. === Добавим к языку исчисления высказываний новые конструкции с предикатами

2=== Аксиомы ===  {{Определение |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> находится в области действия данного квантора. }} 

Будем говорить, что переменная Если некоторое вхождение переменной <tex>y x</tex> свободна для находится в области действия квантора по переменной <tex>x</tex> при подстановке в формулу , то такое вхождение мы назовем '''связанным'''. Вхождение переменной <tex>\psix</tex> непосредственно рядом с квантором (или просто свободна для подстановки вместо <tex>\forall x\dots</tex>)мы назовем '''связывающим'''. Те вхождения переменных, которые не являются связанными или связывающими, назовем '''свободными'''. Формула, если после подстановки ни одно ее вхождение не станет связаннымимеющая свободных вхождений переменных, называется '''замкнутой'''.

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

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

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> ложна.%Вывод из гипотез также вполне можно расширить на исчисление предикатов. === Итог ===

Формальная система, составленная из указанного языка, множества аксиом и множестваправил вывода, называется '''исчислением предикатов'''.

{{Определение |id=valid

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

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