Natuurlijke deductie

Natuurlijke deductie is een methode om via deductie met noodzakelijkheid de geldigheid van een redenering conform vastgestelde regels te bewijzen in de logica. Het model zou gebaseerd zijn op een "natuurlijke" vorm van redeneren. Systemen van natuurlijke deductie zijn ontwikkeld voor verschillende vormen van logica, waaronder de propositielogica en de predicatenlogica.

Regels

Een bewijsvoering in de logica gaat uit van premissen. Op die premissen worden logische regels toegepast, waardoor nieuwe feiten worden afgeleid. Zo komt men stap voor stap tot het gewenste resultaat. Een kenmerk van natuurlijke deductie is dat tijdens de bewijsvoering nieuwe aannames worden gedaan en weer ingetrokken. Hierdoor ontstaan deelbewijzen. De regels van natuurlijke deductie kunnen worden ingedeeld in introductieregels, regels die een bepaalde logische operator introduceren, en eliminatieregels, regels die een logische operator gebruiken.

De gebruikte logische regels worden aangegeven door een horizontale streep. Boven de streep staan de precondities voor het toepassen van de regel en onder de streep de conclusies. Links van de streep wordt de naam van de regel geplaatst.

Propositielogica

De logische regels voor de propositielogica zijn de volgende:

Conjunctie-introductie: $\wedge \mathrm {I} \ {\frac {P\quad Q}{P\wedge Q}}$ Als de uitspraken P en Q gelden, dan ook de uitspraak "P en Q".	Conjunctie-eliminatie: $\wedge \mathrm {EL} \ {\frac {P\wedge Q}{P}}\qquad \wedge \mathrm {ER} \ {\frac {P\wedge Q}{Q}}$ Als de uitspraak "P en Q" geldt, dan ook de uitspraken P en Q.
Disjunctie-introductie: $\vee \mathrm {IL} \ {\frac {P}{P\vee Q}}\qquad \vee \mathrm {IR} \ {\frac {Q}{P\vee Q}}$ Als de uitspraak P geldt of de uitspraak Q, dan ook de uitspraak "P of Q".	Disjunctie-eliminatie: $\vee \mathrm {E} \ {\frac {P\vee Q\quad [P]R\quad [Q]R}{R}}$ Als de uitspraak "P of Q" geldt, en met extra aanname P kan R afgeleid worden, en met extra aanname Q kan ook R afgeleid worden, dan geldt R.
Implicatie-introductie: ${\mathord {\to }}\mathrm {I} \ {\frac {[P]Q}{P\to Q}}$ Als met aanname P de uitspraak Q afgeleid kan worden, dan geldt de uitspraak "als P dan Q".	Implicatie-eliminatie (modus ponens): ${\mathord {\to }}\mathrm {E} \ {\frac {P\quad P\to Q}{Q}}$ Als P geldt en "als P dan Q", dan geldt ook Q.
Negatie-introductie: $\neg \mathrm {I} \ {\frac {[P]Q\wedge \neg Q}{\neg P}}$ Als uit de aanname dat P geldt een tegenspraak kan worden afgeleid, dan geldt "niet P".	Negatie-eliminatie: $\neg \mathrm {E} \ {\frac {\neg \neg P}{P}}$ Uit "niet niet P" volgt P.

Sommige systemen van natuurlijke deductie bevatten in plaats van de negatie-eliminatieregel de reductio ad absurdum-regel

${\text{RAA}}\ {\frac {[\neg P]Q\wedge \neg Q}{P}}$

die zegt, dat, als uit de aanname dat "niet P" een tegenspraak volgt, P afgeleid kan worden. Uit negatie-eliminatie en de andere regels volgt de reductio ad absurdum-regel als afgeleide regel, en andersom. Dat betekent dat met beide varianten dezelfde uitspraken kunnen worden afgeleid. Zowel de negatie-eliminatieregel als de reductio ad absurdum-regel worden in de intuïtionistische logica niet geaccepteerd.

Voorbeeld

Laat p een propositievariabele zijn. Hieronder wordt met behulp van natuurlijke deductie bewezen dat de wet van de uitgesloten derde, p ∨ ¬p, geldt.

Stap	Aannames	Uitspraak	Rechtvaardiging
1	1	¬(p ∨ ¬p)	Aanname
2	2	p	Aanname
3	2	p ∨ ¬p	∨I,2
4	1,2	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	∧I,1,3
5	1	¬p	¬I,4,[2]
6	1	p ∨ ¬p	∨I,5
7	1	(p ∨ ¬p) ∧ ¬(p ∨ ¬p)	∧I,1,6
8		¬¬(p ∨ ¬p)	¬I,7,[1]
9		p ∨ ¬p	¬E,8

Predicatenlogica

Voor predicatenlogica gelden, behalve de bovengenoemde regels, ook de volgende regels. Hieronder staat P[x\a] voor de formule P waarin alle (vrije) voorkomens van x door a vervangen worden.

Introductie van universele kwantor (universele generalisatie): $\forall \mathrm {I} \ {\frac {P[x/a]}{\forall x.P}}$ waarbij a niet in de openstaande aannames voorkomt Als P(a) geldt, waarbij we niks over het object a hebben aangenomen, dan geldt "voor alle objecten x: P(x)".	Eliminatie van universele kwantor (universele instantiatie): $\forall \mathrm {E} \ {\frac {\forall x.P}{P[x/a]}}$ Als P voor alle objecten geldt, dan geldt het ook voor het object a.
Introductie van existentiële kwantor (existentiële generalisatie): $\exists \mathrm {I} \ {\frac {P[x/a]}{\exists x.P}}$ Als P voor het object a geldt, dat geldt ook "Er is een object x waarvoor geldt dat P(x).	Eliminatie van existentiële kwantor: $\exists \mathrm {E} \ {\frac {\exists x.P\quad [P[x/a]]Q}{Q}}$ waarbij a niet in de openstaande aannames of in Q voorkomt Als "er is een x zodat P(x)" geldt, en uit de aanname dat P(a) (waarbij niks over a wordt aangenomen) volgt Q, dan geldt Q.

Voor de predicatenlogica met gelijkheid kunnen bovendien de volgende regels gebruikt worden:

Gelijkheidsintroductie: ${\mathord {=}}\mathrm {I} \ {\frac {}{a=a}}$ Alles is gelijk aan zichzelf.

Gelijkheidseliminatie: ${\mathord {=}}\mathrm {E} \ {\frac {a=b\quad P(a)}{P(b)}}$ Als predicaat P geldt voor object a, en a is gelijk aan b, dan geldt P ook voor b.

Zie ook

• Logische wetten
• Systeem van Fitch

Bronnen, noten en/of referenties

• Jon Barwise, John Etchemendy, The Language of First-Order Logic. University of Chicago Press, 1993.
• Prof. dr. W.R. de Jong, Basisboek Logica, Argumentatie en formele structuur. Amsterdam: Boom, 2005. ISBN 9789085060673
• L.T.F. Gamut, Logic, Language and Meaning. Utrecht: Het Spectrum, 1991