13.3 Normal Forms

Normal forms for proofs are simplified shapes of derivations. The aim is to remove unnecessary detours and expose the essential structure of a proof.

In propositional logic, formulas have normal forms such as CNF and DNF. In proof theory, proofs can also have normal forms. A proof may be correct but still contain redundant steps. Normalization rewrites the proof into a cleaner form.

Detours in Proofs

A detour occurs when a proof introduces a connective and then immediately eliminates it.

For example, suppose we have proofs of $A$ and $B$. We may introduce a conjunction:

Then we may immediately eliminate the conjunction to recover $A$:

This is valid, but wasteful. The proof goes from $A$ and $B$ to $A \land B$, then back to $A$. We could have used the proof of $A$ directly.

So the proof reduces to:

This is the basic idea of proof normalization.

Introduction and Elimination Rules

Natural deduction often organizes rules into pairs.

An introduction rule explains how to prove a connective.

An elimination rule explains how to use a connective.

For conjunction, the introduction rule is:

The elimination rules are:

and:

A normal proof avoids the pattern where a formula is introduced only to be immediately eliminated.

Example: Conjunction Reduction

Consider the proof:

This first proves $A \land B$, then extracts $B$.

The detour can be removed. The normalized proof is simply:

The original proof and the normalized proof have the same conclusion, but the normalized proof is shorter.

Example: Implication Reduction

Implication has a similar pattern.

Implication introduction has the form:

Implication elimination is modus ponens:

A detour appears when we first prove $A \to B$ by assuming $A$ and deriving $B$, and then immediately apply that implication to a proof of $A$.

The shape is:

Normalization removes the detour by substituting the proof of $A$ into the places where the temporary assumption $A$ was used.

This is the proof-theoretic version of function application.

Normal Proofs

A proof is normal when it contains no reducible detours of this kind.

Informally, in a normal proof:

• formulas are not introduced and immediately eliminated
• temporary assumptions are used in a disciplined way
• the proof follows the structure of the conclusion more directly

Normal proofs are easier to analyze because their structure is more predictable.

Subformula Property

Many normalized proofs satisfy the subformula property.

This means that every formula appearing in the proof is a subformula of either:

or:

where the proof establishes:

A subformula is a formula that occurs inside another formula.

For example, the subformulas of:

include:

and the whole formula:

The subformula property is important because it limits what can appear in a normal proof. It says that a normal proof does not need unrelated intermediate formulas.

Normalization Theorem

A typical normalization theorem says:

If there is a proof of $A$ from assumptions $\Gamma$, then there is a normal proof of $A$ from $\Gamma$.

In symbols:

This does not say that every proof is already normal. It says every proof can be transformed into a normal one.

Why Normal Forms Matter

Normal forms make proof systems more transparent.

They help us prove consistency. If every proof can be normalized, and no normal proof of contradiction exists, then the system is consistent.

They help with proof search. If we know that a normal proof exists whenever any proof exists, then we can search only among normal proofs.

They also connect logic with computation. Under the Curry-Howard correspondence, proof normalization corresponds to program evaluation. Removing a proof detour is like reducing a computation step.

For example, applying a function to an argument and then evaluating the body corresponds to implication normalization.

Thus proof normalization is not just a cleanup procedure. It reveals the computational content of logical reasoning.