Luonnollinen päättely

Luonnollinen päättely on matemaattisen logiikan menetelmä tehdä johtopäätöksiä todeksi oletetusta tiedosta. Sitä käytetään erityisesti propositiologiikassa ja predikaattilogiikassa päättelemään oletuksista uuden lauseen todeksi käsittelemällä lauseita sekä niiden välisiä ja sisäisiä suhteita. Luonnollinen päättely tunnetaan myös Gentzenin päättelysääntöjärjestelmänä matemaatikko Gerhard Gentzenin mukaan.

Säännöt muokkaa

Luonnollisessa päättelyssä johdetaan johtopäätös   todeksi oletetuista lauseista  . Jos kyseinen päätös on mahdollinen, kirjoitetaan tehtävä  . Johtopäätös saadaan tuomalla ja eliminoimalla oletuksissa esiintyviä konnektiiveja ja kvanttoreita tietyillä säännöillä.

Oletukset kirjoitetaan viivan ylle, säännöllä saatu johtopäätös viivan alle. Viivan viereen merkitään sääntö, jota käytetään, kirjoittamalla merkin jota sääntö käsittelee ja kirjaimen   tai   riippuen, onko käytössä tuonti- vai eliminointisääntö. Päättelyä voi jatkaa ja tulokseen soveltaa lisää sääntöjä, jos johtopäätös ei seuraa heti oletuksista.

Hakasuluissa merkitty oletus on väliaikainen oletus, jonka ei tarvitse kuulua tunnettuihin oletuksiin, mutta ehtona sen käytölle täytyy hylätä oletus päättelyn aikana. Hylkääminen tapahtuu säännön soveltamisen aikana, ja hylätessä väliaikainen oletus ja sen sääntö numeroidaan merkitsemään, koska hylkääminen tapahtuu.

Propositiologiikassa on ainoastaan konnektiiveja lauseiden välillä. Luonnollisessa päättelyssä ovat konjunktio, disjunktio, implikaatio, ekvivalenssi ja negaatio. Jokaiselle on olemassa oma tuontisääntönsä ja eliminointisääntönsä:

 


 


 


 


 

Predikaattilogiikassa edellisten konnektiivien lisäksi on mallin alkioita ja kvanttoreita vaikuttamassa kaavoihin. Kummallekin kvanttorille, universaalikvanttorille ja eksistenssikvanttorille on myös omat tuonti- ja eliminointisääntönsä, ja toisin kuin konnektiivien säännöissä, niiden käyttöihin liittyy tiettyjä alkion ehtoja:

 


 

Ehdot: *)   ei saa olla vapaa hylkäämättömissä oletuksissa, joista on johdettu  . **)   on vapaa lauseessa   ei saa olla vapaa lauseessa   eikä hylkäämättömissä oletuksissa, paitsi lauseessa  .

Jos päättelysysteemiin halutaan tuoda uusia konnektiiveja, niiden päättelysääntöjä koskevat tietyt rajoitukset, joita kutsutaan loogisen harmonian vaatimukseksi.

Eheys muokkaa

Luonnollisen päättelyn   sanotaan olevan eheä, jos johtopäätös kyetään päättelemään oletuksista. Propositiologiikalle ja predikaattilogiikalle on omat eheyslauseensa, jotka kertovat luonnollisen päättelyn olevan eheä.

Propositiologiikassa eheyslause sanoo, että jos lauseen   voi johtaa oletuksista   ja kaikkien oletusten totuusarvot ovat 1, myös johtopäätöksen totuusarvo on 1.

Predikaattilogiikassa eheyslause sanoo, että jos lauseen   voi johtaa oletuksista   ja tulkintajono   toteuttaa kaikki oletukset mallissa  ,   toteuttaa myös johtopäätöksen mallissa  .

Kirjallisuutta muokkaa

Miettinen, Seppo K.: Logiikka: Perusteet. Helsinki: Gaudeamus, 2002. ISBN 951-662-865-6.

Väänänen, Jouko, Logiikka I, luentomonisteet, Helsingin yliopisto, kevät 2010.

Katso myös muokkaa