Hilbertovský kalkul

Verze z 15. 9. 2014, 13:30, kterou vytvořil Veronika.Kovrzkova (diskuse | příspěvky) (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…“)
(rozdíl) ← Starší verze | zobrazit aktuální verzi (rozdíl) | Novější verze → (rozdíl)

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 ===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 $$(\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 $$\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 ======= 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, též nazývané jako axiomy substituce:
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 ======= 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

Odkazy ===== Zdroje ===
  1. VAVREČKOVÁ Šárka. Logika a logické programování. (2005).
=== Související články =