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

Hilbertovský predikátový systém užívá výrokové axiomy $A_{1}-A_{7}$ plus axiomy specifikace (v podstatě jde o axiomatická schémata, protože za uvedené formule můžeme dosadit libovolné formule), též nazývané jako axiomy substituce

Axiomy specifikace

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

Odvozovací pravidla

Stejně jako výrokové axiomy si zde vypůjčíme i odvozovací pravidlo modus ponens plus dvě pravidla generalizace.

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$

Odkazy

Související články

Kalkul přirozené dedukce
Gentzenovský sekventový kalkul