Naturlig deduksjon

Fra Wikipedia, den frie encyklopedi
Hopp til navigering Hopp til søk

Naturlig deduksjon kan i logikk og bevisteori referere til både Gerhard Gentzens og Jan Łukasiewiczs 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[rediger | rediger kilde]

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 , funksjonssymoboler og relasjonssymboler er bestemt av et førsteordens språk:

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: .

Konnektiv Introduksjon Eliminasjon
ingen
ingen
 
 

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

Konsistent[rediger | rediger kilde]

Gentzens naturlig deduksjon, NJ, er konsistent, i den forstand at det ikke finnes noen derivasjon for 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[rediger | rediger kilde]

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


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

Litteratur[rediger | rediger kilde]

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