# 3.1 Natural Deduction

Natural deduction is a proof system designed to reflect the way reasoning is carried out in ordinary mathematical arguments, where conclusions are obtained from assumptions by applying rules that correspond directly to the meaning of logical connectives.

In this system, proofs are constructed step by step, and each step is justified either by an assumption or by applying an inference rule to earlier steps, so that the entire derivation forms a structured argument whose correctness can be checked mechanically.

### Judgments and Derivations

A derivation is a finite sequence of formulas:
$$
A_1, A_2, \dots, A_n
$$

where each formula $A_i$ is either an assumption or follows from earlier formulas by applying an inference rule.

If there exists a derivation of a formula $A$ from a set of assumptions $\Gamma$, we write:
$$
\Gamma \vdash A
$$

This notation expresses that $A$ is provable from $\Gamma$ within the proof system.

In natural deduction, proofs are often written in a tree like or indented form, where assumptions may be introduced temporarily and later discharged.

### Introduction and Elimination Rules

Each logical connective is governed by two kinds of rules, called introduction rules and elimination rules.

An introduction rule explains how to prove a formula involving a connective, while an elimination rule explains how to use such a formula once it has been established.

This design reflects the meaning of each connective and ensures that reasoning remains aligned with semantics.

### Conjunction

The introduction rule for conjunction states that if both $A$ and $B$ have been proved, then their conjunction may be concluded:
$$
\frac{A \qquad B}{A \land B}
$$

The elimination rules state that from a conjunction one may extract either component:
$$
\frac{A \land B}{A}
\qquad
\frac{A \land B}{B}
$$

These rules express that a conjunction is true exactly when both of its parts are true.

### Implication

The introduction rule for implication captures the idea of conditional reasoning.

If, under the temporary assumption that $A$ holds, one can derive $B$, then one may conclude:
$$
A \to B
$$

This is written schematically as:
$$
\frac{[A] \ \vdots \ B}{A \to B}
$$

where the assumption $A$ is discharged after deriving $B$.

The elimination rule for implication is modus ponens:
$$
\frac{A \qquad A \to B}{B}
$$

This rule allows one to apply an implication once its premise has been established.

### Disjunction

The introduction rules for disjunction state that if one of the disjuncts is known, then the disjunction may be concluded:
$$
\frac{A}{A \lor B}
\qquad
\frac{B}{A \lor B}
$$

The elimination rule for disjunction expresses reasoning by cases.

If $A \lor B$ is known, and from $A$ one can derive $C$, and from $B$ one can also derive $C$, then $C$ may be concluded:
$$
\frac{A \lor B \qquad [A] \ \vdots \ C \qquad [B] \ \vdots \ C}{C}
$$

This rule formalizes the idea that if a conclusion follows in all possible cases, then it holds unconditionally.

### Negation

Negation is treated in terms of contradiction.

The introduction rule for negation states that if assuming $A$ leads to a contradiction, then $¬A$ may be concluded:
$$
\frac{[A] \ \vdots \ \bot}{¬A}
$$

The elimination rule states that from $A$ and $¬A$ one may derive a contradiction:
$$
\frac{A \qquad ¬A}{\bot}
$$

In classical logic, one may also derive any formula from a contradiction:
$$
\frac{\bot}{A}
$$

This rule is sometimes called explosion, and it reflects that a contradiction has no consistent truth assignment.

### Example 3.1

We derive:
$$
\{p \to q, p\} \vdash q
$$

The derivation proceeds as follows.

From the assumptions we have:
$$
p \to q
$$
and:
$$
p
$$

Applying modus ponens, we conclude:
$$
q
$$

This is a direct application of the implication elimination rule.

### Example 3.2

We derive:
$$
\vdash p \to (q \to p)
$$

Assume:
$$
p
$$

Under this assumption, assume:
$$
q
$$

From the assumption $p$, we already have:
$$
p
$$

Thus we may conclude:
$$
q \to p
$$
by implication introduction, discharging the assumption $q$.

Now we conclude:
$$
p \to (q \to p)
$$
by implication introduction, discharging the assumption $p$.

This derivation illustrates how assumptions are introduced temporarily and then removed once they have served their role.

### Lemma 3.3 (Weakening)

If:
$$
\Gamma \vdash A
$$
and:
$$
\Gamma \subseteq \Delta
$$
then:
$$
\Delta \vdash A
$$

Proof

Any derivation from $\Gamma$ is also a derivation from $\Delta$, since every assumption used in the derivation belongs to $\Delta$, so the same sequence of steps remains valid.

### Lemma 3.4 (Deduction Theorem)

If:
$$
\Gamma, A \vdash B
$$
then:
$$
\Gamma \vdash A \to B
$$

Proof

The proof follows the structure of implication introduction, since a derivation of $B$ from $\Gamma$ together with the temporary assumption $A$ may be transformed into a derivation of $A \to B$ from $\Gamma$ by discharging the assumption $A$.

This theorem connects derivability with implication and plays a central role in proof theory.

### Structure of Proofs

Natural deduction proofs can be represented as trees in which each node corresponds to a formula and each edge corresponds to the application of a rule.

The leaves of the tree are assumptions, and the root is the final conclusion, and the structure of the tree reflects the logical dependencies between different parts of the proof.

This representation emphasizes that proofs are not merely sequences of formulas but structured objects that encode the flow of reasoning.

### Connection with Semantics

Natural deduction is designed so that its rules preserve truth under every valuation, which ensures that any formula that can be derived from a set of assumptions is a semantic consequence of those assumptions.

This property is the basis of soundness, which will be studied in detail later, and it ensures that formal proofs correspond to valid reasoning about truth.