13.4 Consistency Proofs

A formal system should avoid proving contradictions. Consistency is the property that a system does not collapse into proving everything.

At the simplest level, a system is consistent if there is some formula $A$ such that the system does not prove both $A$ and $¬A$.

More commonly, we say that a system is consistent if there is no formula $A$ such that:

and

Equivalently, in many classical systems, consistency means that the system does not prove a contradiction:

Here $\bot$ is the symbol for contradiction or falsity.

Why Contradiction Is Dangerous

In classical logic, from a contradiction, every formula follows. This principle is called explosion.

It is usually written:

or:

So if a system proves $\bot$, then it can prove any formula $B$.

For example, it could prove:

and also prove:

Once this happens, the proof system can no longer distinguish true conclusions from false ones.

Direct Consistency

One way to prove consistency is direct. We show that no proof of contradiction can exist.

For example, suppose a proof system has a strong normalization theorem. If every proof reduces to a normal proof, and no normal proof ends with $\bot$, then the system is consistent.

The argument has this shape:

1. Assume there is a proof of $\bot$.
2. Normalize the proof.
3. The result is a normal proof of $\bot$.
4. Show that no such normal proof exists.
5. Therefore no proof of $\bot$ exists.

This kind of proof uses the structure of derivations.

Semantic Consistency

Another common method is semantic.

If we can find a model of the axioms, then the system is consistent.

Suppose a theory $T$ has a model $\mathcal{M}$. This means every axiom of $T$ is true in $\mathcal{M}$.

If the proof system is sound, then every theorem of $T$ is also true in $\mathcal{M}$.

So if $\bot$ is never true in any model, then:

The argument is:

Since:

we conclude:

This is one of the cleanest ways to prove consistency.

Example: Propositional Logic

Pure propositional logic is consistent.

To see this semantically, take any valuation $v$. No valuation makes both $p$ and $¬p$ true.

For example, if:

then:

If:

then:

So $p \land ¬p$ is false under every valuation:

Since sound proof systems prove only valid formulas, they cannot prove $p \land ¬p$.

Relative Consistency

Many important consistency proofs are relative.

A relative consistency proof shows that if one system is consistent, then another system is consistent.

The general form is:

This means: if system $S$ is consistent, then system $T$ is consistent.

For example, one may prove that if ZF set theory is consistent, then ZFC with some additional construction is consistent.

Relative consistency is common in set theory and model theory. It is useful because strong systems often cannot prove their own consistency, due to Gödel’s second incompleteness theorem.

Syntactic Consistency

A syntactic consistency proof works only with formal derivations.

It avoids appealing to external models and instead studies the rules directly.

For example, in a sequent calculus, one may prove cut-elimination. Then one shows that the empty sequent, or contradiction, cannot be derived in a cut-free proof.

The shape is:

but:

therefore:

This method is central in proof theory because it extracts consistency from the structure of proofs.

Consistency and Completeness

For first-order logic, completeness creates a useful bridge.

If a theory $T$ is syntactically consistent, then it has a model:

Conversely, if $T$ has a model, then $T$ is consistent, assuming soundness.

So for first-order logic:

This equivalence is one reason first-order logic is so central. It connects proof theory and model theory in a precise way.

Consistency Strength

Not all consistency statements are equally strong.

For a theory $T$, the statement:

usually means a formal arithmetic sentence expressing that no proof of contradiction exists in $T$.

A stronger theory may prove the consistency of a weaker theory.

For example, a sufficiently strong set theory can prove the consistency of Peano Arithmetic, assuming the set theory itself is consistent.

But by Gödel’s second incompleteness theorem, a sufficiently strong consistent theory cannot prove its own consistency:

provided $T$ satisfies the required technical conditions.

This makes consistency proofs subtle. To prove the consistency of a system, we normally reason from outside that system, or from a stronger system.