π“œ

Math Notes

University Mathematics

ConceptComplete

Formal Proof Systems - Examples and Constructions

Concrete examples illustrate how different proof systems construct derivations and how automated reasoning systems implement these ideas.

ExampleNatural Deduction Proof

Prove (p→q)→((q→r)→(p→r))(p \to q) \to ((q \to r) \to (p \to r)) using natural deduction:

1. [p β†’ q]ΒΉ         (assumption)
2.   [q β†’ r]Β²       (assumption)
3.     [p]Β³         (assumption)
4.     q            (β†’-elim, 1, 3)
5.     r            (β†’-elim, 2, 4)
6.   p β†’ r          (β†’-introΒ³, 3-5)
7. (q β†’ r) β†’ (p β†’ r) (β†’-introΒ², 2-6)
8. (p β†’ q) β†’ ((q β†’ r) β†’ (p β†’ r)) (β†’-introΒΉ, 1-7)

Each assumption is eventually discharged by an introduction rule, indicated by the superscript numbers. The proof tree structure makes the logical flow transparent.

ExampleHilbert-Style Proof

Prove (p→(q→r))→((p→q)→(p→r))(p \to (q \to r)) \to ((p \to q) \to (p \to r)) using Hilbert axioms:

  1. Ο•β†’(Οˆβ†’Ο•)\phi \to (\psi \to \phi) (Axiom 1)
  2. (Ο•β†’(Οˆβ†’Ο‡))β†’((Ο•β†’Οˆ)β†’(Ο•β†’Ο‡))(\phi \to (\psi \to \chi)) \to ((\phi \to \psi) \to (\phi \to \chi)) (Axiom 2)
  3. Instance of Axiom 2: (p→(q→r))→((p→q)→(p→r))(p \to (q \to r)) \to ((p \to q) \to (p \to r))

This is actually an axiom instance! Hilbert systems excel when the desired formula matches an axiom schema. For formulas that don't, proofs can be quite long and unintuitive.

DefinitionResolution Principle

Resolution is a refutation-based proof method. To prove Ξ“βŠ¨Ο•\Gamma \models \phi, we show Ξ“βˆͺ{¬ϕ}\Gamma \cup \{\neg \phi\} is unsatisfiable by deriving the empty clause (contradiction).

Given clauses (disjunctions of literals):

C1=L1βˆ¨β‹―βˆ¨Liβˆ¨β‹―βˆ¨LmC_1 = L_1 \lor \cdots \lor L_i \lor \cdots \lor L_mC2=K1βˆ¨β‹―βˆ¨Β¬Liβˆ¨β‹―βˆ¨KnC_2 = K_1 \lor \cdots \lor \neg L_i \lor \cdots \lor K_n

The resolvent is:

C=L1βˆ¨β‹―βˆ¨Liβˆ’1∨Li+1βˆ¨β‹―βˆ¨Lm∨K1βˆ¨β‹―βˆ¨Kjβˆ’1∨Kj+1βˆ¨β‹―βˆ¨KnC = L_1 \lor \cdots \lor L_{i-1} \lor L_{i+1} \lor \cdots \lor L_m \lor K_1 \lor \cdots \lor K_{j-1} \lor K_{j+1} \lor \cdots \lor K_n

Resolution is refutation complete: if Ξ“\Gamma is unsatisfiable, repeated resolution derives the empty clause β–‘\square.

ExampleResolution Proof

Prove (p∨q),(¬p∨r),(¬q∨r)⊨r(p \lor q), (\neg p \lor r), (\neg q \lor r) \models r:

Show {(p∨q),(¬p∨r),(¬q∨r),¬r}\{(p \lor q), (\neg p \lor r), (\neg q \lor r), \neg r\} is unsatisfiable:

1. p ∨ q           (premise)
2. ¬p ∨ r          (premise)
3. ¬q ∨ r          (premise)
4. Β¬r              (negated conclusion)
5. Β¬p              (resolve 2, 4 on r)
6. Β¬q              (resolve 3, 4 on r)
7. q               (resolve 1, 5 on p)
8. β–‘               (resolve 6, 7 on q - empty clause)

The empty clause proves unsatisfiability, hence the original consequence holds.

DefinitionTableau Method

The tableau method (also called analytic tableaux) systematically searches for a model of a formula by building a tree of possible truth assignments. For Ξ“βŠ¨Ο•\Gamma \models \phi, we test if Ξ“βˆͺ{¬ϕ}\Gamma \cup \{\neg \phi\} is satisfiable:

  • Decompose formulas according to their main connective
  • Ο•βˆ§Οˆ\phi \land \psi: must have both Ο•\phi and ψ\psi (single branch)
  • Ο•βˆ¨Οˆ\phi \lor \psi: have Ο•\phi or ψ\psi (branch splits into two)
  • Β¬(Ο•βˆ§Οˆ)\neg(\phi \land \psi): equivalent to Β¬Ο•βˆ¨Β¬Οˆ\neg \phi \lor \neg \psi (splits)
  • βˆ€x ϕ\forall x \, \phi: instantiate with all relevant terms
  • βˆƒx ϕ\exists x \, \phi: introduce a fresh constant (Skolemization)

A branch closes if it contains both Ο•\phi and ¬ϕ\neg \phi. The tableau proves unsatisfiability if all branches close.

Remark

Modern automated theorem provers combine these methods:

  • SAT solvers use sophisticated variants of resolution (DPLL, CDCL algorithms)
  • SMT solvers extend SAT with decision procedures for theories (arithmetic, arrays, etc.)
  • Interactive provers (Coq, Isabelle, Lean) use natural deduction or sequent calculus with tactics

The choice of proof system dramatically affects both human usability and computational efficiency.