1. Natural Deduction Rules

Natural Deduction Rules

Natural Deduction

Natural deduction is a type of forward reasoning proof system: the objective is to derive the conclusion of the argument, starting from its premises.

There are two ways of generating new conclusions in natural deduction: ?

• We either eliminate a connective from a formula in the proof to generate a new conclusion (via a connective elimination rule)
• We produce a new conclusion with a connective, by combining formulas in the proof (via a connective introduction rule)

Link to original

We start with a basic set of rules, that is complete. By complete, we mean that it is sufficient to prove any valid argument.

Our rules will either eliminate or introduce a connective, our proof system will have a pair of rules for each connective of the language.

• $⊝I$ will be used to designate the introduction of the connective $⊝$. For instance, $(\wedge I)$ will be used to denote the rule that introduces the connective $\wedge$.
• $⊝E$ will be used to designate the elimination of the connective $⊝$. For instance, $(\wedge E)$ will be used to denote the rule that eliminates the connective $\wedge$.

We also follow 2. Forward Reasoning Systems > Deduction Theorem#Notes about proofs.

Rules for $\wedge$, $\vee$, and $\neg$

Rules for conjunction ($\wedge$)

Natural Deduction rules for conjunction

$A\wedge B$ is only true when both $A$ and $B$ are true. Similarly, whenever we know that $A\wedge B$ is true, we know that $A$ and $B$ are both true. This gives us ($\wedge I$) and ($\vee E$) rules as: ?

$$\frac{A,B}{A\wedge B}(\wedge I)\frac{A\wedge B}{A}\text{ and }\frac{A\wedge B}{B}(\wedge E)$$Link to original

Introduction of disjunction ($\vee I$)

Natural Deduction introduction of disjunction

We can obtain $A\vee B$ as long as at least one of $A$ and $B$ is true. This gives us the introduction ($\vee I$) rules: ?

$$\frac{A}{A\vee B}\text{ and }\frac{B}{A\vee B}(\vee I)$$Link to original

title: Example 1: Prove that $A \land B \vdash B \lor C$
$$
	\begin{aligned}
		&1. &&A \land B &&\text{data} \\
		&2. &&B &&\text{from } (1.) \text{ and } (\land E) \\
		&3. &&B \lor C &&\text{from } (2.) \text{ and } (\lor I)
	\end{aligned}
$$

Elimination of disjunction ($\vee E$)

Natural Deduction elimination of disjunction

The first $(\vee E)$ we present is an indirect rule. We can eliminate a dis-junction $A\vee B$ by showing that some formula $C$ follows from both $A$ and $B$, so whichever of $A$ or $B$ is the case, $C$ will hold: ?

$$\frac{A\to C,B\to C,A\vee B}{C}(\vee E)$$Link to original

title: Example 2: Prove that $A, A \rightarrow (B \lor C), B \rightarrow D, C \rightarrow D \vdash D$
$$
	\begin{aligned}
		&1. &&A &&\text{data} \\
		&2. &&A \rightarrow (B \lor C) &&\text{data} \\
		&3. &&B \rightarrow D &&\text{data} \\
		&4. &&C \rightarrow D &&\text{data} \\
		&5. &&B \lor C &&\text{since } (1.), (2.) \text{ and } (\rightarrow E) \\
		&6. &&D &&\text{since } (5.), (3.), (4.) \text{ and } (\lor E)
	\end{aligned}
$$

Rules for negation ($\neg$)

Natural Deduction rules for negation

The rules for negation are also done indirectly and can be tricky. In order to conclude $\neg A$, we must show that if $A$ were the case, then we would reach a contradiction. We can also use the same reasoning to eliminate $\neg$ by starting with the negated formula, $\neg A$. Hence: ?

$$\frac{A\to B,A\to \neg B}{\neg A}(\neg I)\frac{\neg A\to B,\neg A\to \neg B}{A}(\neg E)$$Link to original

title: Example 3: Prove that $A \rightarrow B, A \rightarrow \neg B, C \vdash \neg A \land C$
$$
	\begin{aligned}
		&1. &&A \rightarrow B &&\text{data} \\
		&2. &&A \rightarrow \neg B &&\text{data} \\
		&3. &&C &&\text{data} \\
		&4. &&\neg A &&\text{since } (1.), (2.), and (\neg I) \\
		&5. &&\neg A \land C &&\text{since } (3.), (4.), and (\land I)
	\end{aligned}
$$

Rules for biconditional ($⟺$)

Natural Deduction rules for biconditional

When dealing with the biconditional, $⟺$, there is two natural deduction rules, one for introduction and elimination: ?

$$\frac{A\to B,B\to A}{A⟺B}(⟺I)\frac{A⟺B}{(A\to B)\wedge (B\to A)}(⟺E)$$Link to original

Implication Introduction and Elimination

Elimination of the Implication ($\to E$)

Modus ponens

Modus ponens comes from the Latin “method of affirming (the antecedent)”. Sometimes referred to as “elimination of the implication” ($\to E$): ?

$$\frac{A,A\to B}{B}(\to E)\text{ or "modus ponens"}$$

For example, if A was born in Britain, they are British. A was born in Britain. Therefore, A is British.

Link to original

title: Example 4: Prove $A \land C, A \rightarrow B \vdash B$
$$
	\begin{aligned}
		&1. &&A \land C &&\text{data} \\
		&2. &&A \rightarrow B &&\text{data} \\
		&3. &&A &&\text{since } (1.) \text{ and } (\land E) \\
		&4. &&B &&\text{since } (3.), (2.) \text{ and } (\rightarrow E)
	\end{aligned}
$$

Introduction of the Implication ($\to I$)

Natural Deduction introduction of implication

If we want to derive $A\to B$ from some premises, then we must show that these premises together with $A$ imply $B$. ?

$$\frac{\text{premises}}{A\to B},\text{if }\frac{\text{premises},A}{B}(\to I)$$

The proof that $B$ follows from the addition of $A$ to premises is done in a separate subcomputation box.

Link to original

Subcomputations

Subcomputation box

A subcomputation box defines a sub-proof that is dependent on an extra assumption.

The box demonstrates that the consequent of the implication is a valid conclusion under the assumption that the antecedent is true. Our goal is to justify the derivation of the implication:

• If the assumption is true, then the box provides valid proof of the consequent, therefore the implication holds.
• If the assumption is false, the implication will hold anyway because an implication is true when its antecdent is false. (refer to $\to$ truth table)

Hence, if a box manages to show the conclusion, the implication will be true whether or not the extra assumption is true, and therefore true under the original circumstances.

Link to original

title: Example 5: Prove $A \rightarrow B, B \rightarrow C \vdash A \rightarrow C$
$$
	\begin{array}{c}
		\begin{aligned}
			&1. &&A \rightarrow B &&\text{data} \\
			&2. &&B \rightarrow C &&\text{data} \\
			&3. &&A \rightarrow C &&(\rightarrow I) \text{ from the subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{C} \\
				&3.1. &&A &&\text{assumption} \\
				&3.2. &&B &&\text{from } (3.1), (1.) \text{ and } (\rightarrow E) \\
				&3.3. &&C &&\text{from } (3.2), (2.) \text{ and } (\rightarrow E)
			\end{aligned}
		}
	\end{array}
$$
 
You can think of the box as proof that $A \rightarrow C$ under the assumption that $A \rightarrow B$ and $B \rightarrow C$.

Using subcomputation boxes

In order to correctly perform a subcomputation, we follow these rules:

• The assumption at the beginning of a box may only be used in the box.
• Any conclusions previously available, including premises and formulas derived can also be used inside the box.
• Any conclusion obtained inside the box that depends on the box’s initial assumption cannot be used on its own. (for example, as with example 5 above, $C$ cannot be used on its own as it relies on the assumption of $A$)

title: Example 6: Prove $A \rightarrow B \vdash \neg B \rightarrow \neg A$
$$
	\begin{array}{c}
		\begin{aligned}
			&1. &&A \rightarrow B &&\text{data} \\
			&2. &&\neg B \rightarrow \neg A &&(\rightarrow I) \text{ from the subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				\begin{aligned}
					& && && &&\underline{\neg A} \\
					&2.1. &&\neg B &&\text{assumption} \\
					&2.2. &&A \rightarrow \neg B &&(\rightarrow I) \text{ from the subcomputation below}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{\neg B} \\
						&2.2.1. &&A &&\text{assumption} \\
						&2.2.2. &&\neg B &&\text{since } (2.1)
					\end{aligned}
				} \\
				\begin{aligned}
					&\neg A && &&\text{from } (1.), (2.2), \text{ and } (\neg I) \\
				\end{aligned}
			\end{aligned}
		}
	\end{array}
$$
 
You can think of the box as proof that $A \rightarrow C$ under the assumption that $A \rightarrow B$ and $B \rightarrow C$.

Link to original

2. Examples using the basic rules

Examples using the basic rules

title: Example 1: Show that $(A \lor B) \rightarrow C \vdash (A \rightarrow C) \land (B \rightarrow C)$.
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&(A \lor B) \rightarrow C &&\text{data} \\
			&2. &&(A \rightarrow C) &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{C} \\
				&2.1 &&A &&\text{assumption} \\
				&2.2 &&A \lor B &&\text{from } (2.1) \text{ and } (\lor I) \\
				&2.3 &&C &&\text{from } (2.2), (1.) \text{ and } (\rightarrow E)
			\end{aligned}
		} \\
		\begin{aligned}
			&3. &&(B \rightarrow C) &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{C} \\
				&3.1 &&B &&\text{assumption} \\
				&3.2 &&A \lor B &&\text{from } (2.1) \text{ and } (\lor I) \\
				&3.3 &&C &&\text{from } (3.2), (1.) \text{ and } (\rightarrow E)
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&(A \rightarrow C) \land (B \rightarrow C) &&\text{from } (2.), (3.) \text{ and } (\land I)
		\end{aligned}
	\end{array}
$$

title: Example 2: Show that $A \lor B, \neg B \vdash A$.
 
In this case, we use the [[Natural Deduction elimination of disjunction]].
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&A \lor B &&\text{data} \\
			&2. &&\neg B &&\text{data} \\
			&3. &&A \rightarrow A &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&3.1 &&A &&\text{assumption} \\
				&3.2 &&A &&\text{from } (3.1)
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&B \rightarrow A &&\text{subcomputation below}
		\end{aligned} \\
		\boxed{
			\begin{array}{l}
				\begin{aligned}
					& && && &&\underline{A} \\
					&4.1 &&B &&\text{assumption} \\
					&4.2 &&\neg A \rightarrow B &&\text{subcomputation below}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{B} \\
						&4.2.1 &&\neg A &&\text{assumption} \\
						&4.2.2 &&B &&\text{from } (4.1)
					\end{aligned}
				} \\
				\begin{aligned}
					&4.3 &&\neg A \rightarrow \neg B &&\text{subcomputation below}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{\neg B} \\
						&4.3.1 &&\neg A &&\text{assumption} \\
						&4.3.2 &&\neg B &&\text{from } (2.)
					\end{aligned}
				} \\
				\begin{aligned}
					&4.4 &&A &&\text{from } (4.2), (4.3), and (\neg E)
				\end{aligned} \\
			\end{array}
		} \\
		\begin{aligned}
			&5. &&A &&\text{from } (1.), (3.), (4.), \text{ and } (\lor E)
		\end{aligned} \\
	\end{array}
$$
 
$$
	\frac{A \lor B, \neg B}{A} \, (\lor E2) \text{ will be introduced as a variant rule later}
$$

title: Example 3: Show that $\vdash \neg (A \land \neg A)$ (this shows that $\neg (A \land \neg A)$ is a tautology)
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&A \land \neg A \rightarrow A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&1.1 &&A \land \neg A &&\text{assumption} \\
				&1.2 &&A &&\text{from } (1.1) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&2. &&A \land \neg A \rightarrow \neg A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&2.1 &&A \land \neg A &&\text{assumption} \\
				&2.2 &&\neg A &&\text{from } (2.1) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&3. &&\neg (A \land \neg A) &&\text{from } (1.), (2.), and (\neg I)
		\end{aligned} \\
	\end{array}
$$

title: Example 4: Show that $A \land \neg A \vdash B$
**This shows you how to derive any conclusion from an inconsistent set.**
 
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&A \land \neg A &&\text{data} \\
			&2. &&\neg B \rightarrow A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{A} \\
				&2.1 &&\neg B &&\text{assumption} \\
				&2.2 &&A &&\text{from } (1.) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&3. &&\neg B \rightarrow \neg A &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{\neg A} \\
				&3.1 &&\neg B &&\text{assumption} \\
				&3.2 &&\neg A &&\text{from } (1.) \text{ and } (\land E)
			\end{aligned}
		} \\
		\begin{aligned}
			&4. &&B &&\text{from } (2.), (3.), and (\neg E)
		\end{aligned}
	\end{array}
$$

Link to original

3. Introducing variant rules

Variant rules

We can avoid the need for a subcomputation box if we augment our basic set of rules with an extra implication-introduction rule of the form:

$$\frac{B}{A\to B}(\to I2)$$

This variant implication-introduction rule avoids the need for a subcomputation box in the cases where the consequent of the implication is already part of the current proof.

Using the form above, we can write the proof $B⊢A\to B$ as:

$$\begin{array}{rlrlrl}& 1.& & B& & \text{data}\\ & 2.& & A\to B& & \text{from }(1.)\text{ and }(\to I2)\end{array}$$

Variant disjunction elimination rules ($\vee E1$) ($\vee E2$)

Variant disjunction elimination rules

The variant disjunction elimination rules, $\vee E1$ and $\vee E2$ are: ?

$$\frac{A\vee B,\neg A}{B}(\vee E1)\frac{A\vee B,\neg B}{A}(\vee E2)$$Link to original

Variant negation elimination rules ($\neg E1$) ($\neg E2$)

Variant negation elimination rules

The variant negation elimination rules, $\neg E1$ and $\neg E2$ are: ?

$$\frac{\neg \neg A}{A}(\neg E1)\frac{\neg A\to B,A\to B}{B}(\neg E2)$$Link to original

Variant implication introduction rules ($\to I1$) ($\to I2$)

Variant implication introduction rules

With $(\vee I)$, we can get from $\neg A$ to $\neg A\vee B$ and $B$ to $\neg A\vee B$, which we know are equivalent to $A\to B$. Using $(\to I1)$ we can derive an implication whose antecedent is false, and using $(\to I2)$ we can derive an implication whose consequence is true: ?

$$\frac{\neg A}{A\to B}(\to I1)\frac{B}{A\to B}(\to I2)$$Link to original

Variant implication elimination rules ($\to E1$)

Variant implication elimination rules

We can use $(\to E1)$ to write an implication in terms of disjunction and negation: ?

$$\frac{A\to B}{\neg A\vee B}(\to E1)$$Link to original

Examples

title: Example 1
The proof as below:
$$
	\begin{array}{l}
		\begin{aligned}
			&1. &&P \lor Q &&\text{data} \\
			&2. &&\neg Q &&\text{data} \\
			&3. &&P \rightarrow R &&\text{data} \\
			&4. &&P \rightarrow P &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{aligned}
				& && && &&\underline{P} \\
				&4.1 &&P &&\text{assumption} \\
				&4.2 &&P &&\text{from } (4.1)
			\end{aligned}
		} \\
		\begin{aligned}
			&5. &&Q \rightarrow P &&\text{subcomputation box}
		\end{aligned} \\
		\boxed{
			\begin{array}{l}
				\begin{aligned}
					& && && &&\underline{P} \\
					&5.1 &&Q &&\text{assumption} \\
					&5.2 &&\neg P \rightarrow Q &&\text{subcomputation box}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{Q} \\
						&5.2.1 &&\neg P &&\text{assumption} \\
						&5.2.2 &&Q &&\text{from } (5.1)
					\end{aligned}
				} \\
				\begin{aligned}
					&5.3 &&\neg P \rightarrow \neg Q &&\text{subcomputation box}
				\end{aligned} \\
				\boxed{
					\begin{aligned}
						& && && &&\underline{\neg Q} \\
						&5.3.1 &&\neg P &&\text{assumption} \\
						&5.3.2 &&\neg Q &&\text{from } (2)
					\end{aligned}
				} \\
				\begin{aligned}
					&5.4 &&\neg P &&\text{from } (5.2), (5.3), \text{ and } (\neg E)
				\end{aligned}
			\end{array}
		} \\
		\begin{aligned}
			&6. &&P &&\text{from } (1.), (4.), (5.), \text{ and } (\lor E) \\
			&7. &&R &&\text{from } (3.), (6.), \text{ and } (\rightarrow E)
		\end{aligned}
		\text{ (without variant)}		
	\end{array}
$$
 
Can be represented instead using the variant rule:
$$
	\frac{A \lor B, \neg B}{A} \, (\lor E2)
$$
 
Giving us the new proof:
$$
	\begin{aligned}
		&1. &&P \lor Q &&\text{data} \\
		&2. &&\neg Q &&\text{data} \\
		&3. &&P \rightarrow Q &&\text{data} \\
		&4. &&P &&\text{from } (1.), (2.), \text{ and } (\lor E2) \\
		&5. &&R &&\text{from } (3.), (4.), \text{ and } (\rightarrow E) \\
	\end{aligned}
	\text{ (with variant)}	
$$

title: Example 2: Show that $A \lor B, \neg B \vdash A$
$$
	\begin{aligned}
		&1. &&A \lor B &&\text{data} \\
		&2. &&\neg B &&\text{data} \\
		&3. &&A &&\text{from } (1.), (2.), \text{ and } (\lor E2) \\
	\end{aligned}
$$

title: Example 3: Show that $A \land \neg A \vdash B$
$$
	\begin{aligned}
		&1. &&A \lor \neg A &&\text{data} \\
		&2. &&A &&\text{from } (1.) \text{ and } (\land E) \\
		&3. &&\neg B \rightarrow A &&\text{from } (2.) \text{ and } (\rightarrow I2) \\
		&4. &&\neg A &&\text{from } (1.) \text{ and } (\land E) \\
		&5. &&\neg B \rightarrow \neg A &&\text{from } (4.) \text{ and } (\rightarrow I2) \\
		&6. &&B &&\text{from } (3.), (5.), \text{ and } (\neg E)
	\end{aligned}
$$

title: Example 4: Show that $\neg A, B \rightarrow C \vdash A \rightarrow C$
$$
	\begin{aligned}
		&1. &&\neg A &&\text{data} \\
		&2. &&A \rightarrow C &&\text{from } (1.) \text{ and } (\rightarrow I1)
	\end{aligned}
$$

Link to original