Reference Sheet 10: Constructive Mathematics & Intuitionistic Logic#

Target audience: Forge auditor who knows S5 modal logic, CEM, FOL, basic game theory, topos theory (Sheet 7), and HoTT (Sheet 2) but needs constructive mathematics to reason within non-Boolean topoi and to understand the computational content of proofs.

1. Orientation#

Classical mathematics accepts proofs by contradiction: to prove something exists, it suffices to show that its nonexistence leads to absurdity. Constructive mathematics rejects this — to prove something exists, you must construct it. This is not a philosophical preference but a mathematical necessity once you work inside a topos (Sheet 7): the internal logic of most topoi is intuitionistic (constructive), and proofs by contradiction are not available there.

This matters for the matheology system because:

If the forge adopts topos-theoretic reasoning (Sheet 7), every internal proof must be constructive.
HoTT (Sheet 2) is inherently constructive — the univalence axiom and higher inductive types have computational content that classical reasoning destroys.
Constructive proofs are programs: every constructive existence proof contains an algorithm that computes the witness. This is the Curry-Howard correspondence (expanded in Sheet 12) and is the foundation for machine-checking proofs.

The existing toolkit (S5, CEM, FOL) is classical. This sheet catalogs exactly what fails constructively, what survives, and how to adapt classical reasoning habits for constructive contexts.

2. Key Concepts#

BHK interpretation (Brouwer-Heyting-Kolmogorov). The constructive meaning of logical connectives:

A proof of A ∧ B is a pair: a proof of A and a proof of B.
A proof of A ∨ B is a tagged proof: either a proof of A or a proof of B, with a tag indicating which.
A proof of A → B is a function: a method that transforms any proof of A into a proof of B.
A proof of ∃x. P(x) is a pair: a specific witness w and a proof of P(w).
A proof of ∀x. P(x) is a function: a method that, given any x, produces a proof of P(x).
A proof of ¬A is a proof of A → ⊥: a method that transforms any proof of A into absurdity.

Matheology use: Under BHK, proving “there exists a maximally causally responsible agent h*” (ax19) requires constructing h* — identifying a specific agent, not merely showing the nonexistence of a world without one. If the proof is purely by contradiction (“assume no such h* exists, derive absurdity”), it fails constructively.

Law of Excluded Middle (LEM). The principle A ∨ ¬A for all propositions A. Classically valid; constructively not provable in general. To assert A ∨ ¬A constructively, you must have either a proof of A or a proof of ¬A. For undecided propositions (neither proved nor refuted), LEM is simply unavailable.

Matheology use: Many classical proofs proceed by cases: “either P or ¬P; in case P we get X, in case ¬P we get Y, and in both cases Z follows.” This pattern is not constructively valid unless P is decidable — unless you can algorithmically determine which case holds.

Double negation elimination (DNE). The principle ¬¬A → A. Classically valid; constructively fails. Knowing that A is not impossible does not constructively give you a proof of A. However, A → ¬¬A is constructively valid (if A holds, it is not impossible), and ¬¬¬A → ¬A is valid (triple negation collapses).

Matheology use: A HELL pro-finding that argues “it is impossible for th8 to be false, therefore th8 is true” uses DNE — valid classically but not constructively. The constructive version must exhibit the two attractors directly.

Decidability. A proposition P is decidable if P ∨ ¬P holds constructively — i.e., there is an algorithm that determines which. A type A has decidable equality if (a = b) ∨ ¬(a = b) for all a, b : A. Natural numbers, finite sets, and Boolean values have decidable equality. Real numbers and function types typically do not.

Matheology use: The axiom system’s propositional content divides into decidable propositions (can be algorithmically checked — e.g., “is this well-formed?”) and undecidable ones (require judgment — e.g., “is this axiom true?”). Constructive reasoning works smoothly for decidable propositions and requires more care for undecidable ones.

Constructive existence vs. classical existence. Classical: ∃x. P(x) means “it is not the case that no x satisfies P.” Constructive: ∃x. P(x) means “here is a specific x, and here is a proof that P(x) holds.” The gap is enormous. Classical existence can be proved by contradiction; constructive existence requires a witness.

Matheology use: th7 (God Seeks a Volunteer) asserts existence of a sought volunteer. Classically, this can be proved by showing the alternative is absurd. Constructively, the proof must identify (or give a method to identify) the volunteer — or else re-formulate the claim as ¬¬∃ (double-negated existence: “it is not the case that no volunteer exists”), which is strictly weaker.

Axiom of Choice (AC). Classically: if for every x there exists a y with P(x,y), then there exists a choice function f with P(x, f(x)) for all x. Constructively: this is equivalent to LEM in many settings (Diaconescu’s theorem, Sheet 7). In HoTT: AC for sets (h-level 0) holds but AC for general types does not.

Matheology use: Diaconescu’s theorem (Sheet 7) means: if you want non-classical internal logic in a topos, you must give up full AC. Any matheology proof that uses AC (e.g., selecting a maximal element from an infinite set) must be checked for constructive validity.

Proof relevance. In classical logic, proofs are interchangeable — the fact that A is true matters, not how it was proved. Constructively, proofs carry computational content: different proofs of the same proposition may compute different witnesses. Two proofs of ∃x. P(x) may provide different witnesses w₁ and w₂.

Matheology use: In the VVN system (Sheet 2), two different proofs that version V1 is equivalent to version V2 may carry different computational content — one may provide a syntactic rewriting, another a semantic isomorphism. These are different paths in HoTT, and constructive mathematics says this difference is meaningful, not accidental.

Markov’s principle. The statement: if a computation does not fail to halt, then it halts. Formally: ¬¬∃n. f(n) = 0 → ∃n. f(n) = 0 for decidable f. This is a weak form of DNE restricted to computationally checkable predicates. It is independent of intuitionistic logic — accepted by some constructivists (Russian school), rejected by others (Bishop school).

Matheology use: Some matheology existence claims may satisfy Markov’s principle (the predicate is decidable) even when they fail full DNE. This gives an intermediate option: you can “search” for the witness if you know the search terminates, without having found it yet.

3. Critical Theorems#

Gödel-Gentzen negative translation. Every classically provable sentence φ has a constructively provable “negative translation” φ^N (obtained by inserting double negations at strategic points). If φ is classically provable, then φ^N is intuitionistically provable. Consequence: intuitionistic logic is consistent relative to classical logic — anything classically inconsistent is also intuitionistically inconsistent. Why it matters: The existing classical proofs (th1–th4) remain consistent in the constructive setting — they just may not be directly valid. Their negative translations are valid. This means you lose constructive content but not truth. The question is whether the matheology system needs the constructive content (for computation and machine-checking) or merely classical truth.

Diaconescu’s theorem (full statement). In any topos, the (internal) axiom of choice implies the (internal) law of excluded middle. Contrapositive: in a non-Boolean topos, the axiom of choice fails internally. Why it matters: This is the theorem that forces the choice between classical reasoning (with AC but in a Boolean topos) and constructive reasoning (in a general topos but without AC). The matheology system must decide: does it need AC (e.g., for selecting maximal elements), or does it need non-classical internal logic (e.g., for handling underdetermined propositions)? It cannot have both.

Brouwer’s continuity principle. In certain constructive settings (not all), all functions from ℕ^ℕ to ℕ are continuous. This is false classically (discontinuous functions exist) but consistent with intuitionistic logic. It means constructive real analysis can differ from classical real analysis. Why it matters: If the matheology system uses real-valued observables (wealth, innovation rate) and reasons constructively, some classical theorems about these quantities may fail. Specifically, classical arguments that rely on discontinuous functions (like characteristic functions of non-decidable sets) are constructively invalid.

Constructive completeness of intuitionistic propositional logic. Intuitionistic propositional logic is complete with respect to Kripke semantics: a formula is intuitionistically provable if and only if it holds in all Kripke models. Kripke models are partially ordered sets of “information states” where truth is monotonic (once true, always true as information grows). Why it matters: The matheology system can reason about constructive truth using Kripke models — a concrete, computable semantics. A proposition that is “underdetermined” corresponds to a Kripke state where it is neither forced nor refuted. Proto-formal theorems (th5–th11) naturally live in such states: they may become true as semantic definitions are completed, but are not yet forced.

Friedman’s trick. For any proposition P, if a statement of the form ∃x. Q(x) is classically provable and the proof can be analyzed, there is often a constructive proof of ∃x. Q(x) ∨ P — a disjunctive weakening that is constructively valid even when the original is not. Why it matters: When a classical existence proof (e.g., for h* in ax19) fails constructively, Friedman’s trick may salvage a weaker constructive version: “either the witness exists or some fallback holds.” This gives the forge a systematic method for converting classical matheology proofs to constructive ones with explicit fallbacks.

4. Common Pitfalls#

Using proof by contradiction to establish existence. The most common classical habit that fails constructively. “Assume ¬∃x. P(x), derive contradiction, conclude ∃x. P(x)” is DNE, which fails. Instead: construct the witness directly, or weaken the claim to ¬¬∃x. P(x) (not-not existence).

Assuming case analysis is always available. “Either A or ¬A” is LEM. In constructive contexts, you can only do case analysis on decidable propositions. Before splitting into cases, check whether the proposition is decidable. For finite, computable properties (like “is this axiom index ≤ 14?”), decidability is automatic. For existential or universal claims over infinite domains, it generally is not.

Forgetting that ¬¬A is weaker than A. In classical logic, ¬¬A = A. Constructively, ¬¬A (“A is not impossible”) is strictly weaker than A (“A is proved”). If you prove ¬¬A and then use A, you have silently applied DNE. Track double negations carefully.

Treating all types as decidable. In HoTT (Sheet 2), equality types a =_A b may be non-decidable. You cannot always test whether two elements are equal — you can only construct a path if one exists, or show that one cannot exist. This means conditional branching on equality (“if a = b then … else …”) is not always available.

Assuming constructive proofs are impractical. Many classical proofs are already constructive — especially direct proofs, computations, and proofs by structural induction. The non-constructive proofs that need conversion are typically those using LEM, DNE, or unrestricted AC. The PET theorems th1–th4, being proved by direct derivation from axioms using mereology and S5, are likely already constructive or nearly so.

5. Bridge to Matheology#

Classifying the axiom system’s constructive status. Each axiom and theorem falls into one of:

Already constructive: Direct definitions, explicit constructions. Likely: ax1–ax4 (mereological definitions), ax5–ax7 (modal axioms in S5, which has decidable satisfiability), th1–th4 (direct derivations).
Constructivizable with work: Existence claims that currently use classical reasoning but where witnesses can be constructed. Likely: ax19 (Causal Concentration — the h* can be identified by explicit criteria), ax3 (Divine Surplus — the surplus can be exhibited).
Requires DNE or AC: Claims that essentially need classical principles. Likely: ax20-ax21 (existence of willing volunteers/ mediator — the existence claim may not have a constructive witness). For these, either accept classical reasoning (Boolean topos, Sheet 7) or reformulate as ¬¬∃ claims.

Proto-formal theorems and constructive witnesses. th5–th11 are proto-formal: their predicates (Stable(i), LifeFriendly(i)) lack full semantics. Constructive mathematics adds urgency to this: constructive proofs of th5–th11 would compute what makes an innovation stable, extensible, and life-friendly — the proofs would literally be algorithms. This is the deepest payoff of the constructive approach: not just checking that theorems are true, but extracting computational procedures from their proofs.

Connecting to HoTT (Sheet 2). HoTT’s univalence axiom is constructive in cubical type theory (Coquand et al., 2018). This means the VVN version equivalences (Sheet 2) can be computed: given two versions and a proof of their equivalence, you can algorithmically transform any structure built on one version into the corresponding structure on the other. This is not possible in classical HoTT where univalence is merely axiomatic.

Connecting to topos theory (Sheet 7). Sheet 7 introduces topoi with non-classical internal logic. This sheet explains what that means concretely:

In a Heyting-valued topos, proofs by contradiction fail.
Diaconescu’s theorem means AC fails.
The subobject classifier Ω has more than two elements — there are truth values between “true” and “false” (not “both,” as in paraconsistent logic, but “underdetermined”).
Every internal proof is a morphism in the topos, with computational content determined by the topos structure.

Kripke semantics for proto-formal theorems. The proto-formal theorems th5–th11 live in an information state where their semantic definitions are incomplete. Kripke semantics models this: the current state does not force th8 (Binary Attractors) because the state variables are undefined. As the semantic definitions are completed (information grows), the Kripke model advances to a state that either forces th8 or forces ¬th8. The proto-formal status is not a deficiency but a genuine information state in the constructive semantics.

New questions constructive mathematics enables:

Which of the 25 axioms are constructively valid as stated, and which require reformulation? (A constructive audit of the axiom system.)
Can th5–th11 be proved constructively once their semantics are completed? If so, the proofs contain extraction algorithms. If not, which classical principles do they irreducibly require?
Should the matheology system adopt a pluralist approach — classical reasoning for PET (Boolean topos), constructive for JUB (non-Boolean topos), with geometric morphisms (Sheet 7) translating between them?
What is the computational content of the PET → JUB extension? If the extension is constructive, it is an algorithm for extending any PET model to a JUB model.