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.

Definice

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

Výrokové axiomy

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

• ${\displaystyle \varphi \implies (\psi \implies \varphi )}$
• ${\displaystyle (\varphi \implies (\psi \implies \chi ))\implies ((\varphi \implies \psi )\implies (\varphi \implies \chi ))}$
• ${\displaystyle (\lnot \varphi \implies \lnot \psi )\implies (\psi \implies \varphi )}$

Kde ${\displaystyle \varphi }$, ${\displaystyle \psi }$ a ${\displaystyle \chi }$ jsou libovolné formule jazyka L.

Axiomy pro predikátovou logiku

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: ${\displaystyle (\forall x)(\varphi (x,y_{1},...,y_{n}))\implies \varphi (x/t,y_{1},...,y_{n})}$, je-li term t substituovatelný za x do ${\displaystyle \varphi }$.
• Axiom ${\displaystyle \forall }$-distribuce: ${\displaystyle ((\forall x)(\varphi \implies \psi ))\implies (\varphi \implies (\forall x)\psi )}$, není-li proměnná x volná ve ${\displaystyle \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

• ${\displaystyle (\forall x)(x=x)}$
• ${\displaystyle (x_{1}=y_{1}\land ...\land 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.
• ${\displaystyle (x_{1}=y_{1}\land ...\land 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

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 ${\displaystyle \varphi ,\varphi \implies \psi }$ odvoď ${\displaystyle \,\psi }$;
• Pravidlo generalizace: Z ${\displaystyle \varphi }$ odvoď ${\displaystyle (\forall x)\varphi }$.

Důkaz v hilbertovském kalkulu

Za důkaz nějakého tvrzení ${\displaystyle \,\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 ${\displaystyle \,\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

Související články

• Gentzenovský kalkulus

Literatura

• ŠVEJDAR, Vítězslav. Logika, neúplnost, složitost a nutnost. Praha: Academia, 2002. ISBN 80-200-1005-X.