1302
правки
Изменения
→Аксиомы
Если некоторое вхождение переменной <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>
