Hilbertovský kalkulus

Technology

12 hours ago

Author

Albert Flores

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. +more 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

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). +more 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

(\forall x) (x=x) * (x_{1}=y_{1} \land . \land x_{n}=y_{n}) \implies (R(x_{1},. +more,x_{n}) \implies R(y_{1},. ,y_{n})), kde R je libovolný relační symbol jazyka L. * (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. +more * Pravidlo modus ponens: Z \varphi , \varphi \implies \psi odvoď \,\psi; * Pravidlo generalizace: Z \varphi odvoď (\forall x) \varphi.

Důkaz v hilbertovském kalkulu

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. +more předchozího členu posloupnosti podle pravidla Modus Ponens resp. pravidla generalizace.