Formal Proof Systems - Applications

TheoremResolution Refutation Completeness

The resolution method is refutation complete: if a set $S$ of clauses is unsatisfiable, then the empty clause $\square$ can be derived from $S$ by resolution.

Conversely, if $\square$ can be derived by resolution from $S$ , then $S$ is unsatisfiable.

Resolution forms the basis for modern automated theorem proving. Its completeness, proved by Robinson in 1965, revolutionized automated reasoning by providing a simple, powerful inference rule.

Proof Sketch: The completeness proof uses Herbrand's theorem and the compactness theorem. If $S$ is unsatisfiable, there's a finite Herbrand interpretation where all ground instances of clauses in $S$ are false. Resolution can derive a contradiction from these ground instances, which lifts to a refutation of $S$ itself.

ExampleSAT Solving via Resolution

Modern SAT solvers (DPLL, CDCL) are based on resolution with sophisticated heuristics:

Unit propagation: If a clause becomes a single literal, assign that literal true
Pure literal elimination: If a variable appears only positively (or only negatively), assign it appropriately
Conflict-driven clause learning: When a conflict is found, learn a new clause capturing the reason for the conflict
Backtracking: Undo assignments when conflicts arise

These techniques make SAT solvers remarkably efficient, solving industrial problems with millions of variables.

TheoremDeduction Theorem (Meta-Theorem)

For many proof systems (including Hilbert-style and natural deduction):

\Gamma, \phi \vdash \psi \quad \text{if and only if} \quad \Gamma \vdash \phi \to \psi

This theorem justifies the common proof technique of assuming a hypothesis, deriving the conclusion, and concluding the implication.

The deduction theorem holds for classical logic but fails for some non-classical logics, making it a distinguishing feature of classical reasoning.

TheoremEquivalence of Proof Systems

For first-order logic, the following proof systems are equivalent (prove the same set of formulas):

Hilbert-style systems
Natural deduction
Sequent calculus
Resolution (for refutation)
Tableau methods

Each has $\Gamma \vdash \phi$ in one system if and only if $\Gamma \vdash \phi$ in any other.

ExampleTranslation Between Systems

A natural deduction proof of $\phi \to \psi$ can be converted to:

Hilbert-style: Replace each inference rule with a combination of axiom applications and modus ponens
Sequent calculus: Each natural deduction rule corresponds to a sequent calculus rule
Resolution: Skolemize $\neg(\phi \to \psi) = \phi \land \neg \psi$ , convert to CNF, apply resolution

The translations preserve provability but may change proof size dramatically.

TheoremCraig's Interpolation (via Cut Elimination)

Craig's interpolation theorem can be proved using cut elimination in sequent calculus. If $\phi \models \psi$ , construct a cut-free proof of $\phi \Rightarrow \psi$ . The interpolant can be extracted from this proof by analyzing the formulas appearing on both sides of sequents, using the subformula property to ensure it uses only common vocabulary.

Remark

The cut-elimination approach to interpolation demonstrates the power of structural proof theory. By analyzing the form of proofs rather than their semantic content, we can extract interpolants constructively. This technique extends to many logics beyond first-order, providing uniform methods for obtaining interpolation results.

TheoremCurry-Howard Correspondence

There is a deep correspondence between:

Proof systems (natural deduction, sequent calculus)
Type systems in programming languages
Categories in category theory

Specifically:

Propositions correspond to types
Proofs correspond to programs
Proof normalization corresponds to program evaluation

This "propositions-as-types" paradigm unifies logic, computation, and mathematics.

ExampleCurry-Howard in Practice

The proof of $A \land B \to B \land A$ corresponds to the program:

swap : (A × B) → (B × A)
swap (a, b) = (b, a)

The proof technique (eliminate the pair, reintroduce in opposite order) exactly matches the program structure. This correspondence powers proof assistants like Coq and Agda, where proofs are programs and type-checking verifies correctness.

These applications show that formal proof systems are not merely theoretical abstractions but practical tools with profound connections to computation, type theory, and verified software.