.. meta::
   :description: Reference sheet — Constructive mathematics and intuitionistic logic for topos-internal reasoning in matheology forge sessions.
   :keywords: constructive mathematics, intuitionistic logic, BHK interpretation, excluded middle, computational content, topos, matheology

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

1. If the forge adopts topos-theoretic reasoning (Sheet 7), every
   internal proof must be constructive.
2. HoTT (Sheet 2) is inherently constructive — the univalence axiom
   and higher inductive types have computational content that classical
   reasoning destroys.
3. 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.