Naturlig slutledning är en gren av matematisk logik som utvecklades i Polen på 1920- och 30-talen. Den är avsedd att uttrycka slutledningsregler som är nära besläktade med det "naturliga" sättet att resonera.

På grund av Łukasiewiczs seminarier i Polen 1926, där han förespråkade en mer naturlig behandling av logiken, gjorde Jaśkowski de första försöken att definiera en mer naturlig deduktion. År 1929 föreslog han först att man skulle använda en diagrammatisk notation, och senare uppdaterade han sitt förslag i artiklar 1934 och 1935.

Vad är naturlig slutledning?

Naturlig slutledning (på engelska "natural deduction") är ett formellt system för att skriva upp och manipulera bevis på ett sätt som liknar vardagligt logiskt tänkande. Systemet fokuserar på två typer av regler för varje logisk konstruktion: introduktionsregler (hur man inför en formel av en viss form i ett bevis) och elimineringsregler (hur man använder en sådan formel för att härleda något annat).

Grundläggande idéer och notationer

  • Antaganden och subbevis – Ett typiskt kännetecken är användningen av tillfälliga antaganden (ibland inom "boxar" eller underträd) som senare kan "avslutas" och därmed leda till en slutsats där antagandet är borttaget (dischargerat). Detta används t.ex. vid bevis av implikationer.
  • Flera notationer – Olika stilistiska varianter finns: Jaśkowskis boxnotation, Gentzens träd- eller trädliknande presentation och den så kallade Fitch-stilen som ofta används i undervisningssammanhang.
  • Introduktions- och elimineringsregler – För vanliga logiska tecken förekommer t.ex.:
    • Konjunktion (A ∧ B): ∧-intro (från A och B härled A ∧ B); ∧-elim (från A ∧ B härled A eller B).
    • Disjunktion (A ∨ B): ∨-intro (från A härled A ∨ B); ∨-elim kräver subbevis från båda alternativen för att nå en gemensam slutsats.
    • Implikation (A → B): →-intro (anta A, visa B, slutsatsen blir A → B); →-elim är modus ponens (från A → B och A, härled B).
    • Negation och falsum: ¬A definieras ofta som A → ⊥; bevis med motsägelse och uteslutning av möjligheter ingår.
    • Kvantifikatorer i predikatlogik: ∀-intro/elim och ∃-intro/elim med restriktioner för fria variabler vid generalisering.

Exempel (enkelt)

Bevisa A → A (reflexivitet för implikation) i naturlig slutledning:

1. Anta A. (antagande)
2. Från 1 följer A. (identitet)
3. Därmed, genom →-intro och borttagning av antagandet, får vi A → A.

Historik och utveckling

Jaśkowski var en tidig pionjär som försökte formalisera ett "naturligare" sätt att resonera än de då vanliga axiomatiska systemen. Samtidigt (och oberoende) utvecklade Gerhard Gentzen i Tyskland 1934 ett system för naturlig slutledning och introducerade även sequentkalkylen. Båda angreppssätten betonade introduktions- och elimineringsregler och hanteringen av antaganden inom subbevis.

Senare arbete, särskilt av Dag Prawitz, gav en djupare bevisteoretisk analys av naturlig slutledning: normaliseringssatser (att bevis kan reduceras till en normalform utan "onödiga" steg) och relationer till cut-eliminering i sequentkalkylen är centrala resultat inom området.

Betydelse och tillämpningar

  • Naturlig slutledning utgör grunden för mycket av den moderna bevisteorin och används i studier av bevisstrukturer och bevisomvandlingar.
  • Kontakt med datavetenskap: via Curry–Howard-sambandet relateras naturlig slutledning till typteori och lambda-kalkyl — bevis blir program och formler blir typer.
  • Praktiska användningar finns i formella bevisassistenter (t.ex. Coq, Isabelle, Agda) och i undervisning i logik eftersom systemet speglar intuitivt resonemang.

Vidare läsning

För den som vill fördjupa sig rekommenderas klassiska referenser om Gentzen och Jaśkowski, samt Prawitz arbete om naturlig slutledning och normalisering. Moderna läroböcker i logik och bevisteori presenterar ofta naturlig slutledning tidigt tack vare dess pedagogiska tydlighet och koppling till typteori.