Hilbertovský kalkul: Porovnání verzí

 
Řádek 42: Řádek 42:
 
tedy existuje konečná posloupnost formulí <math>\alpha_1,\cdots \alpha_n</math>, kde <math>\alpha_n = \varphi</math> a <math>\forall i<n</math> platí, že <math>\alpha_i</math>:<br />
 
tedy existuje konečná posloupnost formulí <math>\alpha_1,\cdots \alpha_n</math>, kde <math>\alpha_n = \varphi</math> a <math>\forall i<n</math> platí, že <math>\alpha_i</math>:<br />
 
* je instancí axiomu<br />
 
* je instancí axiomu<br />
* je prvkem <math>\Gamma</math>* <math>\exists j, k<i</math> tak, že <math>\alpha_j \cdots \alpha_k = \alpha_j \rightarrow \alpha_i</math> a <math>\alpha_i</math> vznikla použitím některého pravidla.
+
* je prvkem <math>\Gamma</math><br />
 +
* <math>\exists j, k<i</math> tak, že <math>\alpha_j \cdots \alpha_k = \alpha_j \rightarrow \alpha_i</math> a <math>\alpha_i</math> vznikla použitím některého pravidla.
  
 
== Odkazy ==
 
== Odkazy ==

Aktuální verze z 21. 9. 2014, 21:57

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

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ů , když existuje důkaz formule z v H, tedy existuje konečná posloupnost formulí , kde a platí, že :

  • je instancí axiomu
  • je prvkem
  • tak, že a 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