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

Luonnollisessa päättelyssä johdetaan johtopäätös $B$ todeksi oletetuista lauseista $A_{1},...,A_{n}$. Jos kyseinen päätös on mahdollinen, kirjoitetaan tehtävä $\{A_{1},...,A_{n}\}\vdash B$. 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 $T$ tai $E$ 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ä:

${\frac {\begin{matrix}A&B\end{matrix}}{A\land B}}\ \land T\qquad {\frac {A\land B}{A}}\ \land E\quad {\frac {A\land B}{B}}\ \land E$

${\frac {A}{A\vee B}}\ \vee T\quad {\frac {B}{A\vee B}}\ \vee T\qquad {\frac {\begin{matrix}A\vee B&{\begin{matrix}{[A]^{1}\ }\\\vdots \\C\ \end{matrix}}&{\begin{matrix}{[B]^{1}\ }\\\vdots \\C\ \end{matrix}}\end{matrix}}{C}}\ \vee E,1$

${\frac {\begin{matrix}{[A]^{1}\ }\\\vdots \\B\ \end{matrix}}{A\rightarrow B}}\ \rightarrow T,1\qquad {\frac {\begin{matrix}A\rightarrow B&A\end{matrix}}{B}}\rightarrow E$

${\frac {\begin{matrix}{\begin{matrix}{[A]^{1}\ }\\\vdots \\B\ \end{matrix}}&{\begin{matrix}{[B]^{1}\ }\\\vdots \\A\ \end{matrix}}\end{matrix}}{A\leftrightarrow B}}\ \leftrightarrow T,1\qquad {\frac {\begin{matrix}A\leftrightarrow B&A\end{matrix}}{B}}\leftrightarrow E\quad {\frac {\begin{matrix}A\leftrightarrow B&B\end{matrix}}{A}}\leftrightarrow E$

${\frac {\begin{matrix}{\begin{matrix}{[A]^{1}\ }\\\vdots \\B\land \neg B\ \end{matrix}}\end{matrix}}{\neg A}}\ \neg T,1\qquad {\frac {\neg \neg A}{A}}\ \neg E$

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:

${\frac {A}{\forall xA}}\ \forall T(*\qquad {\frac {\forall xA}{A(t/x)}}\ \forall E(**$

${\frac {A(t/x)}{\exists xA}}\ \exists T(**\qquad {\frac {\begin{matrix}\exists xA&{\begin{matrix}{[A]^{1}\ }\\\vdots \\B\ \end{matrix}}\end{matrix}}{B}}\ \exists E,1(***$

Ehdot: *) $x$ ei saa olla vapaa hylkäämättömissä oletuksissa, joista on johdettu $A$. **) $t$ on vapaa lauseessa $Amath>.***)<math>x\!$ ei saa olla vapaa lauseessa $B$ eikä hylkäämättömissä oletuksissa, paitsi lauseessa $A$.

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

Eheys

Luonnollisen päättelyn $\{A_{1},...,A_{n}\}\vdash B$ 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 $B$ voi johtaa oletuksista $\{A_{1},...,A_{n}\}$ ja kaikkien oletusten totuusarvot ovat 1, myös johtopäätöksen totuusarvo on 1.

Predikaattilogiikassa eheyslause sanoo, että jos lauseen $B$ voi johtaa oletuksista $\{A_{1},...,A_{n}\}$ ja tulkintajono $s$ toteuttaa kaikki oletukset mallissa $M$, $s$ toteuttaa myös johtopäätöksen mallissa $M$.

Kirjallisuutta

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

• Propositiologiikka
• Predikaattilogiikka