Otevřít hlavní menu

Hilbertovský kalkulus

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.

DefiniceEditovat

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

Výrokové axiomyEditovat

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 logikuEditovat

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 rovnostiEditovat

  •  
  •  , kde R je libovolný relační symbol jazyka L.
  •  , kde F je libovolný funkční symbol jazyka L.

Odvozovací pravidlaEditovat

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 kalkuluEditovat

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.

OdkazyEditovat

Související článkyEditovat

LiteraturaEditovat