.. meta::
   :description: Reference sheet — Proof theory and the Curry-Howard correspondence for machine-checkable formalization in matheology forge sessions.
   :keywords: proof theory, Curry-Howard, natural deduction, sequent calculus, cut elimination, proof assistant, Lean, Coq, Agda, matheology

***********************************************************************
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:

.. list-table::
   :header-rows: 1
   :widths: 40 60

   * - 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.