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 tedy 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$

Důkaz v H

Řekneme, že formule $\varphi$ je dokazatelná v H $(\vdash \varphi )$, když existuje důkaz formule $\varphi$ v H, tedy existuje konečná posloupnost formulí $\alpha _{1},\cdots \alpha _{n}$, kde $\alpha _{n}=\varphi$ a $\forall i<n$ platí, že $\alpha _{i}$:* je instancí axiomu* $\exists j,k<i$ tak, že $\alpha _{j}\cdots \alpha _{k}=\alpha _{j}\rightarrow \alpha _{i}$ a $\alpha _{i}$ vznikla použitím některého pravidla.

Řekneme, že formule $\varphi$ je dokazatelná v H z množiny předpokladů $\Gamma$ $(\Gamma \vdash \varphi )$, když existuje důkaz formule $\varphi$ z $\Gamma$ v H, tedy existuje konečná posloupnost formulí $\alpha _{1},\cdots \alpha _{n}$, kde $\alpha _{n}=\varphi$ a $\forall i<n$ platí, že $\alpha _{i}$:* je instancí axiomu* je prvkem $\Gamma$* $\exists j,k<i$ tak, že $\alpha _{j}\cdots \alpha _{k}=\alpha _{j}\rightarrow \alpha _{i}$ a $\alpha _{i}$ vznikla použitím některého pravidla.

Odkazy

Související články

Kalkul přirozené dedukce
Gentzenovský sekventový kalkul