Hilbertovský kalkul

Verze z 15. 9. 2014, 12: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 ===






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