Hilbertovský kalkul

Hilbertovský kalkulus (značme H) je axiomatický formální systém, pojmenovaný po významném německém matematikovi přelomu 19. a 20. století, Davidu Hilbertovi. V Hilbertovském axiomatickém systému provádíme přímé důkazy (případně důkazy z předpokladů) za použití několika axiomů a odvozovacích pravidel (Hilbertovský výrokový kalkulus užívá pouze jedno pravidlo), důkaz je teda poměrně náročnější a delší, proto se dnes častěji užívá kalkulus přirozené dedukce.

Hilbertovský výrokový kalkulus

Výrokové axiomy

$A_{1}:\varphi \implies (\psi \implies \varphi )$
$A_{2}:(\varphi \implies (\psi \implies \chi ))\implies ((\varphi \implies \psi )\implies (\varphi \implies \chi ))$
$A_{3}:(\lnot \varphi \implies \lnot \psi )\implies (\psi \implies \varphi )$
$A_{4}:(\varphi \wedge \psi )\implies \varphi a(\varphi \wedge \psi )\implies \psi$
$A_{5}:\varphi \implies (\psi \implies \varphi \wedge \psi )$
$A_{6}:\varphi \implies (\varphi \vee \psi )a\psi \implies (\varphi \vee \psi )$
$A_{7}:(\varphi \implies \chi )\implies ((\psi \implies \chi )\implies ((\varphi \vee \psi )\implies \chi ))$

Odvozovací pravidla

Modus ponens

$\varphi ,(\varphi \implies \psi )\vdash \psi$

Hilbertovský predikátový kalkulus

Predikátové axiomy

Axiomy specifikace

Jesliže term t je substituovatelný za x ve formuli $\varphi$, můžeme použít následující axiomy, též nazývané jako axiomy substituce:
$B_{1}:\forall x\varphi \implies \varphi x(t)$ $B_{2}:\varphi x(t)\implies \exists x\varphi$

Odvozovací pravidla

Pravidla generalizace

Jestliže x není volná proměnná v $\psi$, můžeme použít následující pravidla:
$GENA:\psi \implies \varphi \vdash \psi \implies \forall x\varphi$ $GENB:\varphi \implies \psi \vdash \exists x\varphi \implies \psi$