Hilbertovský kalkul: Porovnání verzí

Řádek 1: Řádek 1:
'''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í, [[David Hilbert|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á [[Kalkul přirozené dedukce|kalkulus přirozené dedukce]]<ref name="Vavreckova">VAVREČKOVÁ Šárka. Logika a logické programování. (2005).</ref>.
+
'''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í, [[David Hilbert|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á [[Kalkul přirozené dedukce|kalkulus přirozené dedukce]].<ref name="Vavreckova">VAVREČKOVÁ Šárka. Logika a logické programování. (2005).</ref>
 +
 
 
== Hilbertovský výrokový kalkulus ==
 
== Hilbertovský výrokový kalkulus ==
 +
 
=== Výrokové axiomy <ref name="Svejdar ">ŠVEJDAR Vítězslav. Logika: neúplnost, složitost a nutnost. Academia, Praha, 2002. ISBN 80-200-1005-X.</ref> ===
 
=== Výrokové axiomy <ref name="Svejdar ">ŠVEJDAR Vítězslav. Logika: neúplnost, složitost a nutnost. Academia, Praha, 2002. ISBN 80-200-1005-X.</ref> ===
 
<math> A_1:  \varphi \implies (\psi \implies \varphi)</math><br />
 
<math> A_1:  \varphi \implies (\psi \implies \varphi)</math><br />
Řádek 9: Řádek 11:
 
<math> A_6:  \varphi \implies (\varphi \vee \psi)</math>  a  <math>\psi \implies (\varphi \vee \psi)</math><br />
 
<math> A_6:  \varphi \implies (\varphi \vee \psi)</math>  a  <math>\psi \implies (\varphi \vee \psi)</math><br />
 
<math> A_7:  (\varphi \implies \chi) \implies ((\psi \implies \chi) \implies ((\varphi \vee \psi) \implies \chi))</math>
 
<math> A_7:  (\varphi \implies \chi) \implies ((\psi \implies \chi) \implies ((\varphi \vee \psi) \implies \chi))</math>
 +
 
=== Odvozovací pravidla ===
 
=== Odvozovací pravidla ===
 
==== Modus ponens ====
 
==== Modus ponens ====
 
<math> \varphi, (\varphi \implies \psi) \vdash \psi</math>
 
<math> \varphi, (\varphi \implies \psi) \vdash \psi</math>
 +
 
== Hilbertovský predikátový kalkulus ==
 
== Hilbertovský predikátový kalkulus ==
 
=== Predikátové axiomy ===
 
=== Predikátové axiomy ===
Hilbertovský predikátový systém užívá výrokové axiomy <math>A_1 - A_7</math> 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'''
+
Hilbertovský predikátový systém užívá výrokové axiomy <math>A_1 - A_7</math> 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 ====
 
==== Axiomy specifikace ====
 
Jesliže [[Logická formule|term]] ''t'' je [[Substituce|substituovatelný]] za ''x'' ve [[Logická formule|formuli]] <math> \varphi </math>, můžeme použít následující axiomy: <br />
 
Jesliže [[Logická formule|term]] ''t'' je [[Substituce|substituovatelný]] za ''x'' ve [[Logická formule|formuli]] <math> \varphi </math>, můžeme použít následující axiomy: <br />
 
<math> B_1:  \forall x \varphi \implies \varphi x (t)</math><br />
 
<math> B_1:  \forall x \varphi \implies \varphi x (t)</math><br />
 
<math> B_2:  \varphi x (t) \implies \exists x \varphi</math>
 
<math> B_2:  \varphi x (t) \implies \exists x \varphi</math>
 +
 
=== Odvozovací pravidla ===
 
=== Odvozovací pravidla ===
 
Stejně jako výrokové axiomy si zde vypůjčíme i odvozovací pravidlo '''modus ponens''' plus dvě pravidla generalizace.
 
Stejně jako výrokové axiomy si zde vypůjčíme i odvozovací pravidlo '''modus ponens''' plus dvě pravidla generalizace.
 +
 
==== Pravidla generalizace ====
 
==== Pravidla generalizace ====
 
Jestliže ''x'' není [[Logická formule|volná proměnná]] v <math> \psi </math>, můžeme použít následující pravidla: <br />
 
Jestliže ''x'' není [[Logická formule|volná proměnná]] v <math> \psi </math>, můžeme použít následující pravidla: <br />
 
<math> GEN A:  \psi \implies \varphi \vdash \psi \implies \forall x \varphi</math><br />
 
<math> GEN A:  \psi \implies \varphi \vdash \psi \implies \forall x \varphi</math><br />
 
<math> GEN B:  \varphi \implies \psi \vdash \exists x \varphi \implies \psi</math>
 
<math> GEN B:  \varphi \implies \psi \vdash \exists x \varphi \implies \psi</math>
 +
 
== 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,
 +
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 />
 +
 +
Ř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.
  
 
== Odkazy ==
 
== Odkazy ==

Verze z 21. 9. 2014, 21:56

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