Исчисление предикатов — Ефремов Евгений

Алфавит

$x,y,z,u,v,\ldots,x_1,x_2,\ldots\$ — переменные
$c,d,\ldots,c_1,c_2,\ldots\$ — символы констант
$P,Q,R,S,\ldots,P_1,P_2,\ldots\$ — предикатные символы
$F,G,H,\ldots,F_1,F_2,\ldots\$ — функциональные символы
$\urcorner,\vee,\wedge,\to\$ — логические связки
$=\$ — символ равенства
$\exists,\forall\$ — кванторы
$\left(\ ,\right)\$ — скобки

Формулы

Терм:
1. Переменная — терм.
2. Если $t_1,\ldots,t_n$ — термы, $F^{(n)}$ — символ операции, то $F(t_1,\ldots,t_n)$ — терм.

Атомарной формулой называется выражение вида $t=g$ или $P(t_1,\ldots,t_n)$ , где $t,g,t_1,\ldots,t_n$ — термы, $P^{(n)}$ — предикатный символ.

Формула:
1. Атомарная формула — формула.
2. Если $\Phi, \Psi$ — формулы, $x$ — переменная, то $(\Phi\wedge\Psi)$ , $(\Phi\vee\Psi)$ , $(\Phi\to\Psi)$ , $\urcorner\Phi$ , $\exists x\Phi$ , $\forall x\Phi$ — формулы.

Аксиомы

$\begin{array}{rl} 1.&\Phi\to\left(\Psi\to \Phi\right)\\ 2.&\left(\Phi\to \Psi\right)\to\left(\left(\Phi\to\left(\Psi\to \Theta\right)\right)\to\left(\Phi\to \Theta\right)\right)\\ 3.&\Phi\wedge \Psi\to \Phi\\ 4.&\Phi\wedge \Psi\to \Psi\\ 5.&\left(\Phi\to \Psi\right)\to\left(\left(\Phi\to \Theta\right)\to\left(\Phi\to \Psi\wedge \Theta\right)\right)\\ 6.&\Phi\to \Phi\vee \Psi\\ 7.&\Psi\to \Phi\vee \Psi\\ 8.&\left(\Phi\to \Theta\right)\to\left(\left(\Psi\to \Theta\right)\to\left(\Phi\vee \Psi\to \Theta\right)\right)\\ 9. &\left(\Phi\to \Psi\right)\to\left(\left(\Phi\to\urcorner \Psi\right)\to\urcorner \Phi\right)\\ 10.&\urcorner\urcorner \Phi\to \Phi\\ 11.&\forall x\Phi\to[\Phi]^x_t\\ 12.&[\Phi]^x_t\to\exists x\Phi\\ 13.&x=x\\ 14.&\left(x=y\right)\to\left([\Phi]^z_x\to[\Phi]^z_y\right) \end{array}$

$\Phi,\Psi,\Theta$ — формулы исчисления предикатов, $x,y,z$ — переменные, $t$ — терм.

Правила вывода

$1.\ \Phi,\Phi\to \Psi\vdash \Psi$ — modus ponens
$2.\ \Phi\to \Psi\vdash \Phi\to \forall x\Psi$ , если $x\notin FV(\Phi)$
$3.\ \Phi\to \Psi\vdash \exists x\Phi\to \Psi$ , если $x\notin FV(\Psi)$

Версия для печати