Propositielogica: Natuurlijke deductie
Contradictie-eliminatieregel
Met de redeneerregels die we tot nu toe behandeld hebben zijn er nog steeds tautologieën die we niet kunnen afleiden:
- \(\neg\, p\rightarrow (p\rightarrow q)\), bekend onder de Latijnse naam ex falso seguitur quod libet ("uit het ongerijmde volgt om het even wat"). In deze formule staat dus: Als \(p\) onwaar is, dan kan uit het waar zijn van \(p\) elke propositie \(q\) (quod libet) worden afgeleid. Met andere woorden: als in een redenering een contradictie kan worden afgeleid, dan is elke willekeurige conclusie geoorloofd.
- \(p\lor \neg\,p\), bekend als de regel van de uitgesloten derde.
In deze theoriepagina behandelen welke redeneerregel we nodig hebben om \(\neg\, p\rightarrow (p\rightarrow q)\) wel te kunnen afleiden. In de hierop volgende theoriepagina gaan we in op de redeneerregel waarmee de tautologie \(p\lor \neg\,p\) afgeleid kan worden.
Contradictie eliminatieregel De eliminatie \(\bot\,\mathrm{E}\) voor het falsum \(\bot\), dat staat voor een altijd onware propositie: \[\begin{array}{l|ll} \vdots & \vdots &\\ k &\bot & \\ \vdots & \vdots & \\ l & \varphi& \bot\,\mathrm{E}, k \end{array}\]
Met de contradictie redeneerregel kan de formule \(\neg\, p\rightarrow (p\rightarrow q)\) zonder premissen afgeleid worden:
De contractie redeneerregel is ook nodig om de tautologie \[p\lor q, \neg\, p \vdash q\] af te leiden:
Ontgrendel volledige toegang
