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$