Definition:Natural Deduction/Technical Note

Technical Note on Natural Deduction

In order to make the use of the proof rules of natural deduction in a tableau proof on $\mathsf{Pr} \infty \mathsf{fWiki}$, the following templates have been developed:

			Template:Premise				to invoke	the Rule of Assumption for a premise
			Template:Assumption				to invoke	the Rule of Assumption for a non-premise assumption
			Template:Conjunction				to invoke	the Rule of Conjunction
			Template:Simplification				to invoke	the Rule of Simplification
			Template:Addition				to invoke	the Rule of Addition
			Template:ProofByCases				to invoke	Proof by Cases
			Template:ModusPonens				to invoke	Modus Ponendo Ponens
			Template:ModusTollens				to invoke	Modus Tollendo Tollens
			Template:ModusPonendoTollens				to invoke	Modus Ponendo Tollens
			Template:ModusTollendoPonens				to invoke	Modus Tollendo Ponens
			Template:Implication				to invoke	the Rule of Implication
			Template:DoubleNegIntro				to invoke	Double Negation Introduction
			Template:DoubleNegElimination				to invoke	Double Negation Elimination
			Template:BiconditionalIntro				to invoke	Biconditional Introduction
			Template:BiconditionalElimination				to invoke	Biconditional Elimination
			Template:NonContradiction				to invoke	the Principle of Non-Contradiction
			Template:Contradiction				to invoke	Proof by Contradiction
			Template:Explosion				to invoke	the Rule of Explosion
			Template:ExcludedMiddle				to invoke	the Law of Excluded Middle
			Template:Reductio				to invoke	Reductio ad Absurdum

For convenience, other templates are also available, for the following derived rules:

			Template:Commutation				to invoke	the Rule of Commutation
			Template:DeMorgan				to invoke	an instance of De Morgan's Laws
			Template:Idempotence				to invoke	the Rule of Idempotence
			Template:IdentityLaw				to invoke	the Law of Identity

For the other general proof rules, there exist the following templates:

			Template:SequentIntro				to invoke	the Rule of Sequent Introduction
			Template:TheoremIntro				to invoke	the Rule of Theorem Introduction
			Template:Substitution				to invoke	the Rule of Substitution