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.[1]
Obsah
Hilbertovský výrokový kalkulus
Výrokové axiomy [2]
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 (\varphi \wedge \psi) \implies \psi }
a
Odvozovací pravidla
Modus ponens
Hilbertovský predikátový kalkulus
Predikátové axiomy
Hilbertovský predikátový systém užívá výrokové axiomy 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 , můžeme použít následující axiomy:
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 , můžeme použít následující pravidla:
Důkaz v H
Řekneme, že formule je dokazatelná v H , když existuje důkaz formule v H,
tedy existuje konečná posloupnost formulí , kde a platí, že :
- je instancí axiomu
- tak, že a vznikla použitím některého pravidla.
Řekneme, že formule 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}
, když existuje důkaz formule z v H,
tedy existuje konečná posloupnost formulí , kde a platí, že :
- 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 \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 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} vznikla použitím některého pravidla.