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

Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle 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

Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \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 Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \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í Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \alpha_1,\cdots \alpha_n} , kde $\alpha _{n}=\varphi$ a $\forall i<n$ platí, že Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \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ů Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \Gamma} Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle (\Gamma \vdash \varphi)} , když existuje důkaz formule Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \varphi} z $\Gamma$ v H, tedy existuje konečná posloupnost formulí $\alpha _{1},\cdots \alpha _{n}$, kde $\alpha _{n}=\varphi$ a Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \forall i<n} platí, že $\alpha _{i}$:

• je instancí axiomu
  
• je prvkem Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \Gamma} * $\exists j,k<i$ tak, že Nelze pochopit (MathML, alternativně SVG nebo PNG (doporučeno pro moderní prohlížeče a kompenzační pomůcky): Neplatná odpověď („Math extension cannot connect to Restbase.“) od serveru „https://en.wikipedia.org/api/rest_v1/“:): {\displaystyle \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