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]

Hilbertovský výrokový kalkulus

Výrokové axiomy [2]

$ 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:
$ GEN A: \psi \implies \varphi \vdash \psi \implies \forall x \varphi $
$ GEN B: \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

Zdroje

  1. VAVREČKOVÁ Šárka. Logika a logické programování. (2005).
  2. ŠVEJDAR Vítězslav. Logika: neúplnost, složitost a nutnost. Academia, Praha, 2002. ISBN 80-200-1005-X.

Související články

Kalkul přirozené dedukce
Gentzenovský sekventový kalkul