Naturlig konklusion

Naturlig inferens  ( naturlig inferens ) er en type logisk beregning , der bruger inferensregler til at bevise udsagn , der er tæt på de sædvanlige meningsfulde metoder til ræsonnement.

For første gang blev sådanne beregninger oprettet i 1934 uafhængigt af Gentsen og Yaskovsky . Sammen med den sekvente calculus tilhører de Gentzen-typen , da de er baseret på en ikke-aksiomatisk tilgang (i modsætning til Hilbert calculus , som bruger udviklede sæt af aksiomer og et minimum af slutningsregler). De mest berømte naturlige inferenssystemer er dem, der er udviklet af Gentzen (til den klassiske version af prædikatregningen ) og (til den intuitionistiske prædikatregning).

Inferensregler i beregning :

• konjunktion introduktion : ("hvis sandt og , så kan vi konkludere ");
• konjunktion undtagelse: og ;
• disjunction introduktion : og ;
• disjunktion undtagelse: ("hvis det er sandt , fra er udledt og fra er udledt , så kan vi konkludere ");
• introduktion af den universelle kvantifier : ;
• universel kvantifier undtagelse: ;
• introduktion af den eksistentielle kvantifier : ;
• udelukkelse af den eksistentielle kvantifier: ;
• implikation introduktion : ;
• eliminering af implikation ( modus ponens ): ;
• negation introduktion : ;
• negation undtagelse: ;
• afledning fra en falsk udsagn : .

Det klassiske system opnås ved at tilføje et aksiom til disse slutningsregler eller ved at tilføje dobbeltnegationsreglen .

Litteratur

• Gentzen G. Inference Studies = Untersuchungen über das logische Schließen // Mathematische Zeitschrift, Bd. 39 (1934–1935), S. 405–431  // Idelson A. V., Mints G. E. Mathematical theory of inference / oversat af A. V. Idelson. - M . : Nauka, 1967. - S. 9-76 .
• Getmanova A. D. Logic. - Boghuset "Universitetet", 1998. - 480 s.
• Zinoviev A. A.  Propositionel logik og slutningsteori. - Peter, 2015. - 937 s.
• Pravits D. naturlig konklusion. Evidensbaseret forskning / oversættelse af P. Bystrov. - Laurie, 1997.