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$.