Axiom

Z Wikipedie, otevřené encyklopedie

Axiom (příbuzný postulát) je základní tvrzení, které se považuje za pravdivé, aniž by k němu byl požadován důkaz. Matematické teorie lze založit na soustavách axiomů (od nichž požadujeme, aby byly vnitřně bezesporné a nezávislé, tzn. aby daná skupina axiomů neobsahovala dva vzájemně si protiřečící axiomy a současně aby nebylo možné odvodit některý z axiomů z ostatních). Tuto metodu vytváření matematických teorií označujeme jako axiomatickou a takto vytvořenou teorii za teorii formální. Pro prokazování tvrzení ve formálních teoriích slouží tzv. formální důkaz. Existuje několik druhů formálních důkazů lišících se systémy pravidel pro dokazování. Tyto systémy se nazývají kalkuly - nejznámější jsou hilbertovský a gentzenovský kalkulus (přičemž první z nich je považovaný za základní logický kalkulus celé matematiky).

[editovat] Vlastní axiomy teorie

Axiom teorie T v jazyce L je každá formule $\ \phi$ jazyka L taková, že $\phi \in T$ (tj. z formálního hlediska je teorie množina svých (vlastních) axiomů). Takové formuli se také někdy říká vlastní axiom T.

[editovat] Logické axiomy hilbertovského kalkulu

Logický axiom pro jazyk L je každá formule $\psi \in LogAx$ jazyka L, kde $\ LogAx$ je množina všech logických axiomů (jazyka L). Množina $\ LogAx$ se liší jak pro různé logické kalkuly, tak pro tentýž kalkulus u různých autorů. Jednou z nejběžnějších definicí logických axiomů pro výrokovou logiku resp. predikátovou logiku prvního řádu je tato (hilbertovský klasický kalkulus):

[editovat] Základní definice vlastností formulí

Podformulí formule $\ \phi$ je každá formule, která je částí formule $\ \phi$ .
Říkáme, že proměnná x je vázaná ve formuli $\ \phi$ , jestliže existuje podformule formule $\ \phi$ ve tvaru $(\forall x) \psi(x)$ .
Říkáme, že proměnná x je volná ve formuli $\ \phi$ , jestliže x má výskyt v nějaké podformuli $\ \psi$ , formule $\ \phi$ , takové, že $\ \psi$ není podformulí žádné formule tvaru $(\forall x)( \chi(x))$ .
Říkáme, že term t je substituovatelný za proměnnou x do formule $\ \phi$ , jestliže x není volná v žádné podformuli tvaru $(\forall y) \psi$ , kde proměnná y má výskyt v termu t.
Je-li x proměnná, t term a $\ \phi$ formule, $\ \phi(x/t)$ značí formuli, která vznikne nahrazením (substitucí) termu t za každý volný výskyt proměnné x ve $\ \phi$ .

[editovat] Výrokové axiomy

$\phi \implies (\psi \implies \phi)$
$(\phi \implies (\psi \implies \chi)) \implies ((\phi \implies \psi) \implies (\phi \implies \chi))$
$(\lnot \phi \implies \lnot \psi) \implies (\psi \implies \phi)$

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

[editovat] Axiomy pro predikátovou logiku

Všecny axiomy výrokové logiky
Axiom substituce: $(\forall x)(\phi (x,y_{1},...,y_{n})) \implies \phi (x/t,y_{1},...,y_{n})$ , je-li term t substituovatelný za x do $\ \phi$ .
Axiom $\forall$ -distribuce: $((\forall x )(\phi \implies \psi)) \implies (\phi \implies (\forall x) \psi)$ , není-li proměnná x volná ve $\ \phi$ .

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.

[editovat] Axiomy rovnosti

$(\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.

[editovat] 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 $\phi , \phi \implies \psi$ odvoď $\ \psi$ .
Pravidlo generalizace: Z $\ \phi$ odvoď $(\forall x) \phi$ .

[editovat] Důkaz v hilbertovském kalkulu

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