Hilbertovský kalkul: Porovnání verzí

(Založena nová stránka s textem „'''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…“)
 
Řá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 teda 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 teda 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 ===== Výrokové axiomy ===<math>A_1: \varphi \implies (\psi \implies \varphi)</math><br /><math>A_2 (\varphi \implies (\psi \implies \chi)) \implies ((\varphi \implies \psi) \implies (\varphi \implies \chi))</math><br /><math>A_3 (\lnot \varphi \implies \lnot \psi) \implies (\psi \implies \varphi)</math><br /><math>A_4 (\varphi \wedge \psi) \implies \varphi$$ a $$(\varphi \wedge \psi) \implies \psi </math><br /><math>A_5 \varphi \implies (\psi \implies \varphi \wedge \psi)</math><br /><math>A_6 \varphi \implies (\varphi \vee \psi)$$ a $$\psi \implies (\varphi \vee \psi)</math><br /><math>A_7 (\varphi \implies \chi) \implies ((\psi \implies \chi) \implies ((\varphi \vee \psi) \implies \chi))</math><br />
 
  
=== Odvozovací pravidla ======= Modus ponens ====<math>\varphi, (\varphi \implies \psi) \vdash \psi</math>
+
== Hilbertovský výrokový kalkulus ==
  
== Hilbertovský predikátový kalkulus ===== Predikátové axiomy ======= Axiomy specifikace ====Jesliže term ''t'' je [[Substituce|substituovatelný]] za ''x'' ve formuli <math> \varphi </math>, můžeme použít následující axiomy, též nazývané jako '''axiomy substituce''': <br /><math>B_1:  \forall x \varphi \implies \varphi x (t)</math><math>B_2:  \varphi x (t) \implies \exists x \varphi</math>
+
=== Výrokové axiomy ===
 +
<math>A_1:  \varphi \implies (\psi \implies \varphi)</math><br />
 +
<math>A_2: (\varphi \implies (\psi \implies \chi)) \implies ((\varphi \implies \psi) \implies (\varphi \implies \chi))</math><br />
 +
<math>A_3(\lnot \varphi \implies \lnot \psi) \implies (\psi \implies \varphi)</math><br />
 +
<math>A_4:  (\varphi \wedge \psi) \implies \varphi  a  (\varphi \wedge \psi) \implies \psi </math><br />
 +
<math>A_5:  \varphi \implies (\psi \implies \varphi \wedge \psi)</math><br />
 +
<math>A_6:  \varphi \implies (\varphi \vee \psi)  a  \psi \implies (\varphi \vee \psi)</math><br />
 +
<math>A_7:  (\varphi \implies \chi) \implies ((\psi \implies \chi) \implies ((\varphi \vee \psi) \implies \chi))</math><br />
  
=== Odvozovací pravidla ======= Pravidla generalizace ====Jestliže ''x'' není 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><math>GEN B:  \varphi \implies \psi \vdash \exists x \varphi \implies \psi</math>
+
=== Odvozovací pravidla ===
 +
 
 +
==== Modus ponens ====
 +
<math>\varphi, (\varphi \implies \psi) \vdash \psi</math>
 +
 
 +
== Hilbertovský predikátový kalkulus ==
 +
 
 +
=== Predikátové axiomy ===
 +
 
 +
==== Axiomy specifikace ====
 +
Jesliže term ''t'' je [[Substituce|substituovatelný]] za ''x'' ve formuli <math> \varphi </math>, můžeme použít následující axiomy, též nazývané jako '''axiomy substituce''': <br />
 +
<math>B_1:  \forall x \varphi \implies \varphi x (t)</math>
 +
<math>B_2:  \varphi x (t) \implies \exists x \varphi</math>
 +
 
 +
=== Odvozovací pravidla ===
 +
 
 +
==== Pravidla generalizace ====
 +
Jestliže ''x'' není 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>
 +
<math>GEN B:  \varphi \implies \psi \vdash \exists x \varphi \implies \psi</math>
  
 
== Důkaz v H ==
 
== Důkaz v H ==
== Odkazy ===== Zdroje ===<references/>=== Související články ===
+
 
 +
== Odkazy ==
 +
 
 +
=== Zdroje ===
 +
 
 +
<references/>
 +
 
 +
=== Související články ===

Verze z 15. 9. 2014, 13:34

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 teda 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








Odvozovací pravidla

Modus ponens

Hilbertovský predikátový kalkulus

Predikátové axiomy

Axiomy specifikace

Jesliže term t je substituovatelný za x ve formuli , můžeme použít následující axiomy, též nazývané jako axiomy substituce:

Odvozovací pravidla

Pravidla generalizace

Jestliže x není volná proměnná v , můžeme použít následující pravidla:

Důkaz v H

Odkazy

Zdroje

  1. VAVREČKOVÁ Šárka. Logika a logické programování. (2005).

Související články