Gentzenovský formální systém výrokové logiky

Úvod

Pro tablovou metodu zjišťování splnitelnosti výrokové formule je charakteristické vytváření určitých sekvencí podformulí zkoumané v každé z větví sémantického tabla podle pravidel vycházejících z vlastností formačních spojek těchto podformulí. Pravidla, podle nichž se posloupnost sekvencí vytváří, lze převést v pravidla spojování sekvencí podformulí ve výsledné formule. Na tom je založen gentzenovský formální systém výrokové logiky.

Gentzenovský formální systém

Gentzenovský systém disponuje narozdíl od Hilbertovského (tři axiomy a jedno pravidlo) pouze jedním axiomem a řadou odvozovacích pravidel tvaru:

S1, ..., Sn

S

Axiom gentzenovského formálního systému výrokové logiky je množina formulí U obsahující komplementární pár atomických formulí {p,p} U.

Odvozovací pravidla gentzenovského systému jsou dvojího druhu:

a)      -pravidla daná schématem

a tabulkou

b)     -pravidla daná schématem

a tabulkou

Tomuto systému se říká přirozená dedukce, neboť do značné míry vystihuje způsob přirozeného deduktivního uvažování.

Shrnutí:

Dedukce je tedy logické usuzování, při kterém musí závěr plynout z předpokladů. Při dedukci musí být pravdivá (platit) implikace (pravidlo) a předpoklad; z toho můžeme jednoznačně odvodit i pravdivost závěru (modus ponens). Analogicky, pokud budeme předpokládat, že platí implikace a neplatí závěr, můžeme jednoznačně odvodit nepravdivost předpokladu (modus tollens). Dedukce je tedy způsob usuzování, které zachovává pravdu (truth preserving reasoning). Podrobnější informace lze nalézt v [5, 19].