Reference Sheet 12: Proof Theory & the Curry-Howard Correspondence#

Target audience: Forge auditor who knows S5 modal logic, CEM, FOL, basic game theory, HoTT (Sheet 2), constructive mathematics (Sheet 10), and the contents of all other sheets but needs proof theory to understand what machine-checkable formalization requires and how to achieve it for the matheology system.

1. Orientation#

The matheology system has a formalization roadmap: proto-formal theorems th5–th11 must eventually become machine-checkable proofs. But what does “machine-checkable” actually mean? It means expressing proofs in a formal language where every step can be mechanically checked by a computer — no informal reasoning, no “it is obvious that,” no gaps. Proof theory is the mathematics of proofs themselves: what forms proofs take, how they compose, and what guarantees they provide.

The Curry-Howard correspondence is the key insight: proofs are programs, and propositions are types. A proof of A → B is a function that takes a proof of A and produces a proof of B. A proof of ∃x. P(x) is a pair: a witness w and a proof of P(w). Checking a proof is type-checking a program. This connects directly to HoTT (Sheet 2) and constructive mathematics (Sheet 10): HoTT proofs are programs in a type-theoretic proof assistant, and their correctness is checked by the type-checker automatically.

None of the existing 11 sheets address the mechanics of formalization — what a proof file looks like, what a proof assistant requires, and what guarantees the result provides. This sheet fills that gap.

2. Key Concepts#

Natural deduction. A proof system where rules are organized by logical connective, with introduction rules (how to prove a connective) and elimination rules (how to use a proved connective). Example:

  • ∧-intro: from proofs of A and B, conclude A ∧ B

  • ∧-elim: from a proof of A ∧ B, conclude A (or B)

  • →-intro: assuming A and deriving B, conclude A → B

  • →-elim (modus ponens): from A → B and A, conclude B

Proofs are trees with assumptions at leaves and the conclusion at the root.

Matheology use: The existing proofs of th1–th4 are informal natural deduction proofs. Formalization means making every rule application explicit — no implicit steps, no gaps, no “clearly.”

Sequent calculus. An alternative proof system using sequents Γ ⊢ Δ, where Γ is a list of assumptions and Δ is a list of conclusions. Rules operate on both sides of the turnstile ⊢. The advantage: proof search is more systematic in sequent calculus than in natural deduction.

Matheology use: When formalizing a complex proof, sequent calculus makes the logical structure explicit. Each step records exactly what is assumed and what is concluded. Proof assistants often use a sequent-like display: “these are your current hypotheses; this is your goal; choose a tactic.”

The Curry-Howard correspondence. The foundational isomorphism:

Logic

Type theory / Programming

Proposition A

Type A

Proof of A

Term (program) of type A

A → B

Function type A → B

A ∧ B

Product type A × B

A ∨ B

Sum type A + B

∃x:A. P(x)

Dependent pair Σ(x:A). P(x)

∀x:A. P(x)

Dependent function Π(x:A). P(x)

⊥ (false)

Empty type (no inhabitants)

Proof checking

Type checking

Matheology use: Every matheology theorem, when formalized, becomes a type. The proof becomes a program of that type. Checking the proof means running the type-checker. If the program type-checks, the proof is correct — mechanically, irrevocably, with zero trust in human judgment. This is what “machine-checkable” means.

Cut elimination (Gentzen’s Hauptsatz). In sequent calculus, the cut rule allows using a previously proved lemma: from Γ ⊢ A and A, Δ ⊢ C, conclude Γ, Δ ⊢ C. Gentzen’s theorem: every proof using cuts can be transformed into a proof without cuts (a “cut-free” proof). The cut-free proof may be much longer but has the subformula property: every formula appearing in the proof is a subformula of the conclusion or the assumptions.

Why it matters: Cut elimination guarantees that proofs can be “unfolded” — every intermediate lemma can be expanded. This means formalized proofs are self-contained: no hidden dependencies, no circular reasoning, no reliance on unproved auxiliary claims.

Normalization. The natural-deduction analogue of cut elimination. A proof is normal if no introduction rule is immediately followed by the corresponding elimination rule (no “detours”). Normalization rewrites proofs to eliminate detours. For typed lambda calculus (Curry-Howard), this is beta-reduction — simplifying programs by evaluating function applications.

Matheology use: Normalizing a proof extracts its computational content: what witness does the proof actually construct? For a constructive proof of ∃x. P(x) (Sheet 10), normalization computes the specific witness x.

Proof assistant. A software system that lets users write formal proofs in a logical framework and mechanically checks every step. The three major assistants:

  • Lean 4: Based on dependent type theory with quotient types. Good library (Mathlib). Strong automation (tactics, term-mode). Active community. Most accessible for formalization newcomers.

  • Coq: Based on the Calculus of Inductive Constructions (CIC). Very mature (30+ years). Strong in constructive mathematics and program extraction. Verbose but precise.

  • Agda: Based on Martin-Löf type theory. Closest to HoTT. Clean syntax. Less automation but very transparent — proofs look like programs.

Matheology use: The choice of proof assistant determines the logical framework, available libraries, and proof style. See Section 5 for a recommendation.

Tactic. A proof-construction command in a proof assistant. Instead of writing the proof term directly, you issue tactics that transform the proof goal step by step. Example in Lean: intro h (assume a hypothesis), exact h (provide the proof term), simp (simplify using known lemmas), ring (solve ring equations automatically).

Matheology use: Formalizing th1–th4 in a proof assistant means translating each logical step into a tactic. The assistant checks each tactic and tracks the remaining proof obligations. The formalization is complete when all obligations are discharged.

Universe levels. In type theory, the “type of all types” leads to paradoxes (Girard’s paradox, analogous to Russell’s paradox). The solution: a hierarchy of universes Type₀ : Type₁ : Type₂ : …. Terms live in types, types live in Type₀, Type₀ lives in Type₁, etc. Universe polymorphism allows definitions to work at all levels.

Matheology use: The matheology system reasons about models (which are mathematical structures) and about the system of models (which is a meta-mathematical structure). These live at different universe levels. A proof assistant enforces this hierarchy — you cannot accidentally form “the set of all models” at the wrong level.

3. Critical Theorems#

Gentzen’s Hauptsatz (cut elimination). Every proof in sequent calculus has a cut-free equivalent. For intuitionistic logic: the cut-free proof satisfies the subformula property and the disjunction property (if ⊢ A ∨ B is provable, then ⊢ A or ⊢ B is provable). Why it matters: The disjunction property is a constructivity guarantee (Sheet 10). If a formalized proof concludes A ∨ B, it must actually prove one of them — no classical dodging. For the matheology system, this means formalized th8 (“either river-of-life attractor or BABL attractor”) must actually specify which attractor a given trajectory converges to.

Strong normalization of typed lambda calculus. In the simply typed lambda calculus (and its dependent extensions used in proof assistants), every reduction sequence terminates. No proof/program loops forever. This guarantees that type-checking is decidable and that proof normalization always completes. Why it matters: The proof assistant will always terminate when checking a formalized matheology proof. You cannot accidentally write a “proof” that loops — the type system prevents it. This is the mechanistic guarantee that makes machine-checked proofs trustworthy.

Gödel’s incompleteness theorems. First: any consistent formal system containing basic arithmetic has true statements that are unprovable within the system. Second: such a system cannot prove its own consistency. Why it matters: The matheology system, once formalized, will be subject to incompleteness: there will be true statements about the formal system that the system cannot prove. This is not a deficiency but a mathematical certainty. The forge should anticipate that some HELL con-findings may be formally undecidable — neither provable nor refutable within the axiom system. Such findings require extending the axiom system (adding new axioms) rather than deriving answers from existing axioms.

De Bruijn criterion. A proof checker is trustworthy if its trusted kernel — the minimal code that must be correct for the checker to be reliable — is small enough for human audit. Lean, Coq, and Agda all have small kernels (a few thousand lines of code). Everything else (tactics, automation, libraries) is checked by the kernel and need not be trusted directly. Why it matters: The trustworthiness of a machine-checked matheology proof does not depend on trusting the proof assistant’s entire codebase — only the kernel. This is the formal analogue of the auditor’s role: trust the core, check the rest.

4. Common Pitfalls#

Expecting formalization to be a transcription. Formalization is not “typing the proof into a computer.” It requires making every implicit step explicit, every definition precise, and every appeal to intuition replaced by a formal rule. A 1-page informal proof may become 100+ lines of formal proof. The effort is in filling the gaps that human readers skip over.

Choosing the wrong proof assistant for the logic. Lean 4 excels at classical mathematics (Mathlib has extensive classical library). Agda excels at HoTT and constructive mathematics. Coq sits between them. If the matheology system adopts HoTT (Sheet 2), Agda or cubical Agda is the natural choice. If it stays classical, Lean 4 is more practical. Using the wrong assistant means fighting the tool instead of doing mathematics.

Underestimating library dependencies. Formalizing “from scratch” is enormously costly. Every definition (natural numbers, real numbers, sets, functions) must be built up. Proof assistants with large libraries (Lean’s Mathlib, Coq’s MathComp) let you start from existing formalizations of basic mathematics. If your logic (modal, mereological) is not in the library, you must build it — this is significant foundational work.

Confusing checked proofs with correct models. A machine-checked proof guarantees: if the axioms are true, then the theorem follows. It says nothing about whether the axioms are true. Formalizing th1–th4 and checking the proofs confirms that th1–th4 follow from ax1–ax14. It does not confirm that ax1–ax14 describe reality. This distinction is crucial — the forge checks logical correctness, not empirical truth.

Ignoring proof maintenance. Formal proofs depend on specific versions of proof assistant libraries. Library updates can break proofs (renamed lemmas, changed definitions). Maintaining formalized proofs is an ongoing cost, not a one-time effort. The matheology system’s versioning (VVN, Sheet 2) should extend to formalized proofs.

5. Bridge to Matheology#

Proof assistant recommendation for the matheology system.

The matheology system uses: S5 modal logic, extensional mereology (CEM), first-order predicate calculus, game-theoretic reasoning, and potentially HoTT (Sheet 2) and constructive mathematics (Sheet 10).

Primary recommendation: Lean 4.

  • Strongest library (Mathlib): Extensive formalization of algebra, topology, analysis, measure theory (relevant for ergodic theory, Sheet 6), and order theory (relevant for mereology).

  • Classical by default: PET’s classical proofs (th1–th4) formalize naturally. Classical axioms (LEM, AC) are available.

  • Active community: Largest formalization community as of 2025–2026. Fastest path to getting help.

  • Limitation: No native HoTT support. If HoTT becomes central, cubical Agda is better.

Secondary recommendation: Agda (cubical mode).

  • Native HoTT: Cubical Agda implements cubical type theory with computational univalence. If the VVN system (Sheet 2) is formalized using HoTT, Agda is the natural choice.

  • Constructive by default: Proofs are constructive unless classical postulates are explicitly added. Matches Sheet 10.

  • Clean syntax: Proofs resemble mathematical notation.

  • Limitation: Smaller library. No equivalent of Mathlib. More foundational work needed.

Not recommended: Coq.

  • Reason: Coq is being succeeded by Rocq (renamed project). The ecosystem is in transition. For new projects starting in 2026, Lean 4 or Agda is a better investment.

Formalization roadmap for the matheology system.

Phase 1 — Foundational definitions:

  • Formalize mereological parthood (≤), S5 modal operators (□, ◇), and the basic predicates (P, S, G, W).

  • In Lean 4: define these as a structure with axioms as axiom declarations or as a class for maximum reusability.

Phase 2 — PET axioms and theorems (ax1–ax14, th1–th4):

  • Translate the existing informal proofs into tactic proofs.

  • These are classical, direct proofs — likely the easiest to formalize.

  • Expected effort: 500–1000 lines of Lean per theorem, depending on the granularity of the mereological library.

Phase 3 — JUB predicate semantics:

  • Define the predicates Stable(i), Extensible(i), LifeFriendly(i), BABL-attractor(i) formally. This is the critical bottleneck: th5–th11 are proto-formal because these predicates lack definitions.

  • This phase is mathematical, not proof-engineering. The definitions must be justified by the content of Sheets 5 (dynamical systems) and 6 (ergodic theory).

Phase 4 — JUB theorems (th5–th11):

  • Once the predicates are defined (Phase 3), formalize the proofs.

  • These proofs may require axioms from mechanism design (Sheet 3), social choice theory (Sheet 8), and ergodic theory (Sheet 6) that are not yet in Mathlib — requiring custom formalizations.

Phase 5 — Cross-model integration:

  • Formalize the categorical structure (Sheet 1): PET and JUB as categories, functors between them, natural transformations.

  • Check alignment echoes categorically.

  • If topos-theoretic reasoning is adopted (Sheet 7), this phase requires the topos library (currently limited in all proof assistants).

Connecting to Curry-Howard. Every formalized matheology proof is simultaneously:

  • A logical derivation (the theorem follows from the axioms)

  • A computer program (the proof computes witnesses for existential claims, transports theorems across equivalences)

  • A checkable artifact (the proof assistant’s kernel checks every step)

The Curry-Howard correspondence ensures these three views are the same object. The forge does not need to choose between them.

New questions proof theory enables:

  • What is the proof-theoretic strength of the matheology axiom system? (Can it prove the consistency of Peano Arithmetic? Of second-order arithmetic? This measures how “powerful” the axiom system is.)

  • Which of th1–th4’s proofs are already in normal form (no detours), and which have unnecessary complexity that formalization would expose?

  • Does the axiom system have the disjunction property (if it proves A ∨ B, it proves one of them)? If so, existential claims in the system always have witnesses — matching the constructive ideal.

  • What is the minimum cut rank of the proofs — how deep is the lemma-dependency structure? This measures the system’s “proof complexity” independent of its logical content.