Hilbertovský kalkul: Porovnání verzí

Řádek 35: Řádek 35:
 
== Důkaz v H ==
 
== Důkaz v H ==
 
Řekneme, že formule '''<math>\varphi</math> je dokazatelná v H''' <math>(\vdash \varphi)</math>, když existuje důkaz formule <math>\varphi</math> v H,
 
Řekneme, že formule '''<math>\varphi</math> je dokazatelná v H''' <math>(\vdash \varphi)</math>, když existuje důkaz formule <math>\varphi</math> v H,
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>:* je instancí axiomu* <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.<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 />
 +
* <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.<br />
  
 
Řekneme, že formule '''<math>\varphi</math> je dokazatelná v H z množiny předpokladů <math>\Gamma</math>''' <math>(\Gamma \vdash \varphi)</math>, když existuje důkaz formule <math>\varphi</math> z <math>\Gamma</math> v H,
 
Řekneme, že formule '''<math>\varphi</math> je dokazatelná v H z množiny předpokladů <math>\Gamma</math>''' <math>(\Gamma \vdash \varphi)</math>, když existuje důkaz formule <math>\varphi</math> z <math>\Gamma</math> v H,
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>:* je instancí axiomu* 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.
+
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 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.
  
 
== Odkazy ==
 
== Odkazy ==

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]

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)}
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_2: (\varphi \implies (\psi \implies \chi)) \implies ((\varphi \implies \psi) \implies (\varphi \implies \chi))}
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_3: (\lnot \varphi \implies \lnot \psi) \implies (\psi \implies \varphi)}
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_4: (\varphi \wedge \psi) \implies \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 (\varphi \wedge \psi) \implies \psi }
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_5: \varphi \implies (\psi \implies \varphi \wedge \psi)}
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_6: \varphi \implies (\varphi \vee \psi)} 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 \psi \implies (\varphi \vee \psi)}
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_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 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 - 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 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 } , můžeme použít následující 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 B_1: \forall x \varphi \implies \varphi x (t)}
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 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:
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 GEN A: \psi \implies \varphi \vdash \psi \implies \forall x \varphi}
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 GEN B: \varphi \implies \psi \vdash \exists x \varphi \implies \psi}

Důkaz v H

Řekneme, že 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} je dokazatelná v H 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 (\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} 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 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_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 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
  • 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.

Řekneme, že 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} 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 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} 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 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_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 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
  • 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} * 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.

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