Luonnollinen johtopäätös

Luonnollinen päätelmä  ( luonnollinen päättely ) on eräänlainen looginen laskelma , joka käyttää päättelysääntöjä todistamaan väitteet , jotka ovat lähellä tavanomaisia ​​mielekkäitä päättelymenetelmiä.

Ensimmäisen kerran tällaiset laskelmat loivat vuonna 1934 itsenäisesti Gentsen ja Yaskovsky . Yhdessä peräkkäisten laskelmien kanssa ne kuuluvat Gentzen-tyyppiin , koska ne perustuvat ei-aksiomaattiseen lähestymistapaan (toisin kuin Hilbert-laskennassa , joka käyttää kehitettyjä aksioomijoukkoja ja vähimmäispäättelysääntöjä). Tunnetuimmat luonnolliset päättelyjärjestelmät ovat Gentzenin kehittämät ( predikaattilaskennan klassiselle versiolle ) ja ( intuitionistiselle predikaattilaskulle).

Päättelysäännöt laskennassa :

• yhdyssanan esittely : ("jos tosi ja , niin voimme päätellä ");
• konjunktio poikkeus: ja ;
• disjunktion esittely : ja ;
• disjunktion poikkeus: ("jos se on totta , mistä johdetaan ja mistä on päätelty , niin voimme päätellä ");
• yleisen kvantisaattorin käyttöönotto : ;
• universaali kvantori poikkeus: ;
• eksistentiaalisen kvantorin esittely : ;
• eksistentiaalisen kvantorin poissulkeminen: ;
• implikaatio johdanto : ;
• implikaatioiden eliminointi ( modus ponens ): ;
• negatiivinen esittely : ;
• negatiivinen poikkeus: ;
• johtopäätös väärästä väitteestä : .

Klassinen järjestelmä saadaan lisäämällä aksiooma näihin päättelysääntöihin tai lisäämällä kaksoisnegataatiosääntö .

Kirjallisuus

• 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. Matemaattinen päättelyteoria / kääntänyt A. V. Idelson. - M .: Nauka, 1967. - S. 9-76 .
• Getmanova A. D. Logiikka. - Kirjatalo "Yliopisto", 1998. - 480 s.
• Zinovjev A. A.  Propositiologiikka ja johtopäätösteoria. - Pietari, 2015. - 937 s.
• Pravits D. luonnollinen johtopäätös. Todisteisiin perustuva tutkimus / käännös P. Bystrov. - Laurie, 1997.