Aksjomat klasycznego rachunku predykatów.html

Jeśli dopuścić reguły odrywania i generalizacji

$\frac{\Phi , \Phi\Rightarrow\Psi}{\Psi}\qquad\frac{\Phi}{\forall_x \Psi}$

jako reguły wnioskowania, to można przyjąć, że aksjomatem klasycznego rachunku predykatów (KRP) jest każda formuła zdaniowa języka KRP, którą można otrzymać z jakiejś tautologii klasycznego rachunku zdań poprzez konsekwentne zastąpienie wszystkich występujących w niej zmiennych zdaniowych formułami zdaniowymi języka KRP i jeszcze dwie klasy formuł (aksjomatów specyficznych):

$\forall_x\Phi(x)\Rightarrow \Phi(t)$ o ile zmienna x nie znajduje się w zasięgu kwantyfikatora wiążącego jakąkolwiek zmienną występującą w termie t;

$\forall_x(\Phi\Rightarrow\Psi)\Rightarrow(\Phi\Rightarrow\forall_x\Phi)$ o ile x nie jest zmienną wolną w formule

Φ

Można również przyjąć za aksjomaty KRP wszystkie podstawienia dowolnie wybranego układu aksjomatów klasycznego rachunku zdań i powyższe dwie klasy aksjomatów specyficznych.

edytuj Bibliografia

Witold A. Pogorzelski, Klasyczny rachunek predykatów, PWN 1981, ISBN 83-01-00567