Formal Proof Systems - Key Properties

The fundamental properties of proof systems ensure they correctly capture logical reasoning while being amenable to mathematical analysis.

DefinitionSoundness and Completeness

A proof system is:

Sound if every provable formula is valid: if $\Gamma \vdash \phi$ , then $\Gamma \models \phi$
Complete if every valid formula is provable: if $\Gamma \models \phi$ , then $\Gamma \vdash \phi$

Soundness ensures the system doesn't prove false statements; completeness ensures it can prove all true statements.

All standard proof systems for first-order logic (Hilbert-style, natural deduction, sequent calculus) are both sound and complete. This was Gödel's great achievement in 1929.

DefinitionConsistency

A set of formulas $\Gamma$ is consistent (in a proof system) if there is no formula $\phi$ such that both $\Gamma \vdash \phi$ and $\Gamma \vdash \neg \phi$ . Equivalently, $\Gamma$ does not prove every formula (doesn't prove $\bot$ ).

By soundness, if $\Gamma$ is consistent, then $\Gamma$ is satisfiable (has a model). By completeness, the converse holds: if $\Gamma$ has a model, then $\Gamma$ is consistent.

DefinitionIndependence

A formula $\phi$ is independent of a set $\Gamma$ if both $\Gamma \cup \{\phi\}$ and $\Gamma \cup \{\neg \phi\}$ are consistent. This means $\phi$ can be neither proved nor refuted from $\Gamma$ .

ExampleFamous Independence Results

The Continuum Hypothesis (CH) is independent of ZFC set theory (Gödel 1940, Cohen 1963)
The Parallel Postulate is independent of the other axioms of Euclidean geometry (leading to non-Euclidean geometries)
The Axiom of Choice is independent of the other ZF axioms (Gödel 1940, Cohen 1963)

These results show that certain mathematical questions cannot be settled by the standard axioms.

DefinitionCut Elimination

In sequent calculus, the cut rule is:

\frac{\Gamma \Rightarrow \Delta, \phi \quad \phi, \Gamma' \Rightarrow \Delta'}{\Gamma, \Gamma' \Rightarrow \Delta, \Delta'} \text{(cut)}

The cut elimination theorem (Gentzen's Hauptsatz) states that if a sequent $\Gamma \Rightarrow \Delta$ is provable using the cut rule, then it is provable without using cut.

Cut elimination has profound consequences:

Subformula property: In a cut-free proof, every formula appearing is a subformula of the conclusion or an assumption. This drastically limits the search space for proofs.
Consistency: Cut elimination provides a direct consistency proof for first-order logic by showing that the empty sequent $\Rightarrow$ (which represents a contradiction) has no cut-free proof.
Decidability: For certain fragments of logic, cut elimination yields decision procedures.

Remark

Cut elimination is analogous to normalization in typed lambda calculus and to the elimination of "lemmas" in proofs—every provable statement can be proved "directly" without auxiliary results. While this makes proofs much longer (potentially exponentially), it provides crucial theoretical insights into the structure of logical reasoning.

DefinitionDecidability and Semi-decidability

A set $S$ of formulas is:

Decidable if there is an algorithm that, given any formula $\phi$ , determines whether $\phi \in S$
Semi-decidable (or recursively enumerable) if there is an algorithm that halts with "yes" if $\phi \in S$ and may not halt if $\phi \notin S$

Key facts:

The set of valid first-order formulas is semi-decidable but not decidable (Church 1936)
The set of provable first-order formulas is semi-decidable (enumerate all proofs)
By completeness, these two sets coincide

This fundamental limitation shapes the landscape of automated reasoning and explains why fully automated theorem proving for first-order logic must be incomplete in practice.