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í:

Kde , a 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: , je-li term t substituovatelný za x do .
  • Axiom -distribuce: , není-li proměnná x volná ve .

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]

  • , kde R je libovolný relační symbol jazyka L.
  • , 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.

  • Pravidlo modus ponens: Z odvoď ;
  • Pravidlo generalizace: Z odvoď .

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

Za důkaz nějakého tvrzení 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 č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]