Hilbertovský kalkulus

Z Wikipedie, otevřené encyklopedie
Skočit na: Navigace, Hledání

Hilbertovský kalkulus (také hilbertovský klasický kalkulus) je jeden z logických kalkulů, kterými se zabývá logika. Jde o kalkulus jednoznačně nejpoužívanější; je v něm formalizována celá matematika. Nazván byl po německém matematikovi Davidu Hilbertovi, který podobný kalkulus poprvé zavedl. Jiným typem logického kalkulu je například gentzenovský kalkulus.

Definice[editovat | editovat zdroj]

Hilbertovský kalkulus je možné rozlišit na verze pro výrokovou a predikátovou logiku.

Výrokové axiomy[editovat | editovat zdroj]

Výrokový hilbertovský kalkulus je tvořen následujícími výrokovými axiomy a odvozovacím pravidlem modus ponens (viz dále). Tato soustava axiomů se také souhrnně nazývá axiomy výrokové logiky; tedy za axiomy výrokové logiky jsou (není-li řečeno jinak) považovány axiomy výrokového hilbertovského kalkulu. Výrokové axiomy jsou následující:

  • \varphi \implies (\psi \implies \varphi)
  • (\varphi \implies (\psi \implies \chi)) \implies ((\varphi \implies \psi) \implies (\varphi \implies \chi))
  • (\lnot \varphi \implies \lnot \psi) \implies (\psi \implies \varphi)

Kde  \varphi ,  \psi a  \chi jsou libovolné formule jazyka L.

Axiomy pro predikátovou logiku[editovat | editovat zdroj]

Predikátový hilbertovský kalkulus obsahuje všechny výrokové axiomy, dvě odvozovací pravidla – modus ponens a generalizace (viz dále) a také následující predikátové axiomy. Systém těchto axiomů se podobně jako u výrokové verze nazývá souhrnně axiomy predikátové logiky (prvního řádu). Predikátové axiomy hilbertovského kalkulu jsou:

  • Axiom substituce: (\forall x)(\varphi (x,y_{1},...,y_{n})) \implies \varphi (x/t,y_{1},...,y_{n}), je-li term t substituovatelný za x do \varphi.
  • Axiom \forall-distribuce: ((\forall x )(\varphi \implies \psi)) \implies (\varphi \implies (\forall x) \psi), není-li proměnná x volná ve \varphi.

V případě predikátové logiky prvního řádu s rovností se k axiomům predikátové logiky prvního řádu přidávají ještě axiomy pro rovnost.

Axiomy rovnosti[editovat | editovat zdroj]

  • (\forall x) (x=x)
  • (x_{1}=y_{1} \and ... \and x_{n}=y_{n}) \implies (R(x_{1},...,x_{n}) \implies R(y_{1},...,y_{n})), kde R je libovolný relační symbol jazyka L.
  • (x_{1}=y_{1} \and ... \and x_{n}=y_{n}) \implies (F(x_{1},...,x_{n})=F(y_{1},...,y_{n})), kde F je libovolný funkční symbol jazyka L.

Odvozovací pravidla[editovat | editovat zdroj]

Velkou roli v axiomatizaci logiky hrají takzvaná odvozovací pravidla, která nejsou žádným druhem axiomů, ale pro svůj blízký vztah k nim se mezi ně někdy zařazují. Odvozovací pravidla jsou dvě, jedno pro výrokovou i predikátovou logiku (Modus Ponens), druhé jen pro predikátovou logiku.

Důkaz v hilbertovském kalkulu[editovat | editovat zdroj]

Za důkaz nějakého tvrzení \, \varphi v jazyce L v teorii T ve výrokové resp. predikátové logice je pak považována libovolná posloupnost formulí jazyka L, jejímž je \, \varphi členem a splňující, že pro každý její člen C platí alespoň jedna z následujících podmínek:

  • C je logický axiom (případně axiom rovnosti)
  • C je vlastní axiom teorie T
  • C je odvozen z předchozích členů resp. předchozího členu posloupnosti podle pravidla Modus Ponens resp. pravidla generalizace.

Odkazy[editovat | editovat zdroj]

Související články[editovat | editovat zdroj]

Literatura[editovat | editovat zdroj]