Definition:Natural Deduction

Definition

Natural Deduction is a technique for deducing valid sequents from other valid sequents by applying precisely defined proof rules, each of which themselves are either "self-evident" axioms or themselves derived from other valid sequents, by a technique called logical inference.

Proof Rules

The following rules are often treated as the axioms of PropLog. Some of them are "obvious", but they still need to be stated formally. Others are more subtle.

This is not the only valid analysis of this subject. There are other systems which use other proof rules, but these ones are straightforward and are easy to get to grips with. It needs to be pointed out that the axioms described in this section do not constitute a minimal set by any means. However, the fewer the axioms, the more complicated the arguments are, and the more difficult they are to establish the truth of them.

Also note that premises of an argument are considered to be assumptions themselves.

Axioms of Natural Deduction

The Rule of Assumption

An assumption may be introduced at any stage of an argument.

The Rule of Conjunction

If we can conclude both $p$ and $q$, we may infer the compound statement $p \land q$:

$p, q \vdash p \land q$

The Rule of Simplification

1. If we can conclude $p \land q$, then we may infer $p$: $p \land q \vdash p$
2. If we can conclude $p \land q$, then we may infer $q$: $p \land q \vdash q$

The Rule of Addition

1. If we can conclude $p$, then we may infer $p \lor q$: $p \vdash p \lor q$
2. If we can conclude $p$, then we may infer $q \lor p$: $p \vdash q \lor p$

The Rule of Or-Elimination

If we can conclude $p \lor q$, and:

1. By making the assumption $p$, we can conclude $r$
2. By making the assumption $q$, we can conclude $r$

then we may infer $r$:

$\displaystyle p \lor q, \left({p \vdash r}\right), \left({q \vdash r}\right) \vdash r$

Modus Ponendo Ponens

If we can conclude $p \implies q$, and we can also conclude $p$, then we may infer $q$:

$p \implies q, p \vdash q$

The Rule of Implication

If, by making an assumption $p$, we can conclude $q$ as a consequence, we may infer $p \implies q$:

$\left({p \vdash q}\right) \vdash p \implies q$

The Rule of Not-Elimination

If we can conclude both $p$ and $\neg p$, we may infer a contradiction:

$p, \neg p \vdash \bot$

The Rule of Proof By Contradiction

If, by making an assumption $p$, we can infer a contradiction as a consequence, then we may infer $\neg p$:

$\left({p \vdash \bot}\right) \vdash \neg p$

The conclusion does not depend upon the assumption $p$.

The Rule of Bottom-Elimination

If we can conclude a contradiction, we may infer any statement:

$\bot \vdash p$

The Law of the Excluded Middle

All statements have a truth value of either true or false:

$\vdash p \lor \neg p$

Otherwise known as:

• (Principium) tertium non datur, Latin for third not given, that is, a third possibility is not possible;
• Principium tertii exclusi, the Principle of the Excluded Third (PET).

Different logical schools

Certain schools of logic have investigated the situation of what happens when certain of the above proof rules are disallowed.

• Johansson's Minimal Calculus allows all the above axioms except the Rule of Bottom-Elimination and the Law of the Excluded Middle.

• Intuitionist Propositional Calculus allows all the above axioms except the Law of the Excluded Middle.

• Classical Propositional Calculus is the school of propositional logic which allows all the above rules.

Sources

• Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2, \ \S 1.2.3$