1302
правки
Изменения
м
→Аксиомы
Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы аксиом исчисления высказываний и дополним их следующими двумя схемами.
Здесь <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}(\Psipsi) \rightarrow (\Psipsi[x := \alpha]) </tex>
(12) <tex>(\Psipsi[x := \alpha]) \rightarrow \exists{x}(\Psipsi) </tex>
Заметим, что если взять формулу <tex>\exists x A(x,y)</tex>, то по схеме аксиом (11),
<tex>
\forall{x}(\Psipsi) \to (\Psipsi[x := \alpha]) \\\Psi 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>y<
=== Правила вывода ===
