Härledningssystem

Ett härledningssystem är ett formellt system som beskriver bevisföringen i en given kontext. Ett sådant system kan bestå av enbart axiom eller av axiom och slutledningsregler.

Ett klassiskt exempel på ett härledningssystem är David Hilberts system för satslogik, vilket består av tre axiom och en slutledningsregel:

(Axiom 1) ${\displaystyle A\to (B\to A)}$

(Axiom 2) ${\displaystyle (A\to (B\to C))\to ((A\to B)\to (A\to C))}$

(Axiom 3) ${\displaystyle (\neg A\to \neg B)\to (B\to A)}$

Slutledningsregel (Modus ponens). Av ${\displaystyle (A\to B)\land A}$ följer ${\displaystyle B}$.

För satslogik och för predikatlogik finns ett flertal härledningssystem av olika karaktär. En del av dessa är praktiskt användbara, genom att de innehåller intuitiva härledningsregler medan andra (till exempel Hilberts satslogiksystem) är formellt tunga, men lämpar sig bättre vid till exempel induktionsbevis över härledningars längd.

Två centrala egenskaper hos härledningssystem är sundhet och fullständighet.

Se även

• Härledningsbegrepp
• Härledningsregel

Källor

• Geoffrey Hunter, Metalogic An Introduction to the Metatheory of Standard First-Order Logic, MacMillan, 1971.
• A. S. Troelstra, H. Schwichtenberg, Basic proof theory (2000), Cambridge University Press, ISBN 0-521-77911-1