Naturlig deduksjon

Naturlig deduksjon kan i logikk og bevisteori referere til både Gerhard Gentzens og Jan Łukasiewicz' opprinnelige logiske kalkyler, eller til den generelle presentasjonen av logiske systemer som de innførte. Før introduksjonen av naturlig deduksjon var logiske systemer basert på en mengde aksiomer og noen få regler, kjent som Hilbert systemer. I artikkelen hvor Gentzen presenterer sin naturlig deduksjons-system, uttrykker han et ønske om at bevisene skal ligne hvordan matematiske bevis ser ut, og han identifiserer ressonering fra antagelser som et viktig aspekt. I naturlig deduksjon er det ingen aksiomer, men derimot flere ressonerings-regler, sammen med hypotetiske antagelser.

Gentzens naturlige deduksjon, NJ

Gentzen definerte først systemet NJ, som er en sunn og komplett logisk kalkyle for førsteordens intuitionistisk predikatlogikk. Termer og formlene for det logiske systemet er definert som, hvor konstanter $c$, funksjonssymoboler $f$ og relasjonssymboler $R$ er bestemt av et førsteordens språk:

$t,s::=x\mid c\mid f(t_{1},\ldots ,t_{n})$

$A,B,F::=\top \mid \bot \mid R(t_{1},\ldots ,t_{n})\mid A\land B\mid A\lor B\mid A\supset B\mid \forall x.\,A\mid \exists x.\,A$

Se artikkelen førsteordens logikk for mer informasjon om formler og termer. I naturlig deduksjon er det vanlig å la negasjon være et definert konnektiv: $\neg A\equiv A\supset \bot$.

Konnektiv	Introduksjon	Eliminasjon
$\top$	${} \over \vdash \top$	ingen
$\bot$	ingen	$\vdash \bot \over \vdash A$
$\land$	$\vdash A\quad \vdash B \over \vdash A\land B$	$\vdash A\land B \over \vdash A$ $\vdash A\land B \over \vdash B$
$\lor$	$\vdash A \over \vdash A\lor B$ $\vdash B \over \vdash A\lor B$	${\cfrac {\begin{matrix}&{\overline {\vdash A}}&{\overline {\vdash B}}\\&\vdots &\vdots \\\vdash A\lor B&\vdash C&\vdash C\end{matrix}}{\vdash C}}$
$\supset$	${\begin{matrix}{\overline {\vdash A}}\\\vdots \\\vdash B\\{\overline {\vdash A\supset B}}\end{matrix}}$	$\vdash A\quad \vdash A\supset B \over \vdash B$
$\forall$	${\vdash A \over \vdash \forall x.\,A}*$	$\vdash \forall x.\;A \over \vdash A[t/x]$
$\exists$	$\vdash A[t/x] \over \vdash \exists x.\,A$	${{\begin{matrix}&{\overline {\vdash A}}\\&\vdots \\\exists x.\,A&C\\\end{matrix}} \over \vdash C}*$

med følgende begrensinger på utledningene: $*$ variabelen $x$ kan ikke forekomme fritt i en åpen antagelse som denne utledningen avhenger av, og i tilfellet med eliminasjon av $\exists$, så kan ikke $x$ forekomme i $C$.

Konsistent

Gentzens naturlig deduksjon, NJ, er konsistent, i den forstand at det ikke finnes noen derivasjon for $\vdash \bot$ fra ingen antagelser.

Da Gentzen publiserte NJ, greide han ikke å bevise at NJ er konsistent, og han konstruerte derfor en annen kalkyle LJ, sekventkalkyle, som han beviste var logisk ekvivalent med NJ, og som han beviste var konsistent. I ettertid har konsistensen til NJ blitt bevist direkte, ved å normalisere bevis, som har en tett sammenheng med å redusere typede lambdatermer, gjennom Curry-Howard korrespondansen.

Gentzens naturlig deduksjon, NK

Samtidig som Gentzen presenterte NJ presenterte han også NK, som er nøyaktig som NJ, men med en ekstra regel, som tilsvarer motsigelsesbevis:

${\begin{matrix}\vdash \neg A\\\vdots \\\vdash \bot \end{matrix}} \over \vdash A$

Gentzen konstruerte også sekventkalkylen LK, og NK er også konsistent.

Litteratur

• Gerhald Gentzen. Untersuchungen über das logische Schlissen", 1934. (Oversatt til engelsk av M.E. Szabo, Investigations Into Logical Deduction, 1964).