Naturlig deduktion: definition, historie og grundlæggende regler
Naturlig deduktion: Få en klar introduktion til definition, historien fra 1920'ernes Polen og de grundlæggende slutningsregler for studerende og logikinteresserede.
Naturlig deduktion er en gren af matematisk logik, der blev udviklet i Polen i 1920'erne og 30'erne. Metoden er beregnet til at udtrykke slutningsregler, som ligger tæt på den måde, mennesker "naturligt" ræsonnerer på: man fører midlertidige antagelser, udleder konsekvenser og eventuelt afviser eller aflader (discharger) antagelser for at få gyldige slutninger uden unødvendige mellemtrin.
Historisk baggrund
Ideen om en mere naturalistisk behandling af logiske slutninger blev tidligt fremført i Polen. Jaśkowski blev ansporet af en række seminarer i Polen i 1926 af Łukasiewicz, som gik ind for en mere naturlig behandling af logikken, og han foretog de første forsøg på at formulere en sådan deduktion. I 1929 foreslog han første gang at bruge en diagrammatisk notation, og han opdaterede sit forslag i artikler i 1934 og 1935.
Samtidig og uafhængigt præsenterede Gerhard Gentzen (i midten af 1930'erne) en formel behandling af naturlig deduktion sammen med sin sequent-kalkyle. Begge tilgange — Jaśkowskis bokssystem, Gentzens træ- og sequent-tilgange — har haft stor indflydelse på udviklingen af moderne bevisteori.
Hvad karakteriserer naturlig deduktion?
- Regelbaseret: Hver logisk forbindelsesformer har typisk to slags regler, en introduktionsregel (hvordan man får forbindelsen) og en elimineringsregel (hvordan man bruger forbindelsen).
- Antagelser og underbeviser: Beviser skrives ofte ved midlertidigt at antage en formel og derefter udlede noget under denne antagelse. Når man er færdig, kan antagelsen aflades og bruges til at få en implikation eller lignende.
- Forskellige notationer: Jaśkowskis boks- eller indrykningsstil, Gentzens træstruktur og den såkaldte Fitch-stil er almindelige måder at repræsentere naturlige deduktioner på.
Grundlæggende regler (eksempler)
Nedenfor er de mest almindelige introduktions- og elimineringsregler for de klassiske forbindelser. Forkortelserne I (introduction) og E (elimination) angiver regeltypen.
- Konjunktion (∧): ∧I (fra A og B udled A ∧ B); ∧E (fra A ∧ B udled A, og fra A ∧ B udled B).
- Disjunktion (∨): ∨I (fra A udled A ∨ B eller fra B udled A ∨ B); ∨E (fra A ∨ B, hvis A→C under antagelse A og B→C under antagelse B, så konkludér C — "bevis ved cases").
- Implikation (→): →I (antag A, udled B; afløs antagelsen og få A→B — kaldet "conditional proof"); →E (modus ponens: fra A→B og A udled B).
- Negation (¬) og kontradiktion (⊥): ¬I (antag A, vis ⊥; afløs for at få ¬A). ¬E (fra A og ¬A få ⊥). Ofte bruges ⊥ som symbolet for kontradiktion/falsum.
- Kvantorer (∀, ∃): Der findes særlige regler for universal- og eksistenskvantifikatorer, herunder betingelser for fri variabelers brug og indførsel/elimineringsrestriktioner.
Eksempel på et simpelt bevis
Bevis for A → A (identitet):
- Antag A. (midlertidig antagelse)
- Fra antagelsen følger A. (trivielt)
- Aflad antagelsen og få A → A ved →I.
Klassisk vs. intuitionistisk naturlig deduktion
Naturlig deduktion kan formuleres både for intuitionistisk logik (konstruerbar logik) og for klassisk logik. Forskellen ligger især i hvilke ekstra regler der tillades:
- I intuitionistisk logik undlader man typisk regler som det udelukkede tredje (A ∨ ¬A) og klassisk reductio (eksempelvis en ubegrænset version af ¬¬A → A).
- I klassisk logik kan man tillægge en regel som reductio ad absurdum (RAA) eller bruge dobbelt negationseliminering for at få klassiske slutninger.
Vigtige teoretiske resultater og anvendelser
- Normalisering: Prawitz og andre viste, at intuitionistiske naturlige deduktioner kan normaliseres — det vil sige, unødvendige "detours" i beviser kan fjernes. Normalisering svarer i praksis til at gøre beviser mere direkte og kortfattede.
- Curry–Howard-korrespondancen: Naturlig deduktion står centralt i forbindelsen mellem beviser og programmer; implikationer svarer til funktionstyper, og beviser til programmer.
- Bevisteori og automatisering: Naturlig deduktion er grundlæggende for formelle bevissystemer, type-systemer i programmeringssprog og automatiserede bevisassistenter (proof assistants).
Notationsvarianter
De mest udbredte former for præsentation er:
- Jaśkowski-bokse/indrykning: Delbeviser skrives i bokse eller som indrykkede blokke der viser midlertidige antagelser.
- Fitch-stil: En linær fremstilling med indrykninger og markering af afløsning af antagelser.
- Tresny træer (Gentzen): Beviser vises som træer hvor rødderne er antagelser og grenene afsluttes med konklusioner; dette er tæt på sequent-kalkylen.
Samlet set tilbyder naturlig deduktion et fleksibelt, intuitivt og teoretisk frugtbart rammeværk til at beskrive og analysere logiske slutninger — både i rent teoretiske sammenhænge og i praktiske anvendelser som bevisassistenter og type-teori.
Søge