442
правки
Изменения
→Интерпретация булевых формул с кванторами как игр для двух игроков
Чтобы получить список аксиом для исчисления предикатов, возьмем все схемы аксиом исчисления высказываний и дополним их следующими двумя схемами.
Здесь <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>f_{P^k_n}: D^k \rightarrow V</tex>.
{{Определение |id=valid
|definition=
Формула в исчислении предикатов общезначима, если она истинна на любом предметном множестве <tex>D</tex>, при любой оценке предикатов, и при
