Foundation Self Bootstrap Distinguishability

The bootstrap's honest floor

Distinguishability is the capacity of a system to tell two things apart. In mathematics, the simplest carrier of this capacity is the two-element type Bool, whose values are false and true. The framework's module begins by proving, in a machine-checked library of formal theorems, that false is not equal to true. This is the base case: a two-element type carries a definitional distinction.

The module then lifts this distinction to any carrier that supports a Boolean predicate taking both truth values. If a type K has a predicate P such that some x satisfies P and some y does not, then x and y are distinct. This is a theorem, not an assumption: the existence of the two truth values forces the existence of two distinct objects. The proof is constructive, producing the witnesses x and y from the two hypotheses.

Next, the module proves a meta-level fact about the formal language itself. For any proposition P, the proposition P is never equal to its negation, not P. This holds in classical logic. The proof runs by cases: if P holds, then assuming P equals not P yields a contradiction; if P fails, the same equality yields P. Either way, the equality is impossible.

The self-bootstrap claim is the assertion that some carrier admits a non-trivial distinction, written as there exist x and y with x not equal to y. The module proves that this claim is itself distinguishable from its own denial. That is, the claim is not equal to the negation of the claim. This follows directly from the previous theorem applied to the proposition that the carrier has two distinct elements.

Finally, the module packages these facts into a certificate structure. The certificate states two things: the meta-language distinguishes propositions, and the object-level claim is not its own negation. The certificate is theorem-backed, meaning it is constructed from the proved theorems, not postulated. The module does not derive an object-level non-singleton carrier from nothing; it proves the meta-level facts that the self-bootstrap argument uses, and it names the object-level condition as an explicit hypothesis in the final theorem.

What this establishes in plain language is a precise boundary. The formal language already contains distinctions among propositions, and the claim that objects are distinguishable is distinct from its denial. But the module does not pretend to conjure a two-object world from an empty one. The object-level non-singleton carrier remains an input, not an output. This is the honest form of the bootstrap: it closes at the meta-language floor, not below it.

/-- The two-element type carries a definitional distinction. -/
theorem bool_distinguishable : (false : Bool) ≠ true := by
  decide

/-- Any carrier supporting a Boolean predicate with both truth values
inherits an object-level distinction. -/
theorem distinguishability_lifted_from_bool
    {K : Type*} (P : K → Bool)
    (hpos : ∃ x : K, P x = true) (hneg : ∃ x : K, P x = false) :
    ∃ x y : K, x ≠ y := by
  obtain ⟨x, hx⟩ := hpos
  obtain ⟨y, hy⟩ := hneg
  refine ⟨x, y, ?_⟩
  intro hxy
  have hfalse : P x = false := by
    simpa [hxy] using hy
  cases hx.symm.trans hfalse

/-- A proposition is never equal to its negation in classical logic. -/
theorem prop_ne_not (P : Prop) : P ≠ ¬ P := by
  intro h
  by_cases hp : P
  · have hnp : ¬ P := by
      rw [h] at hp
      exact hp
    exact hnp hp
  · have hp' : P := by
      rw [h.symm] at hp
      exact hp
    exact hp hp'

/-- The claim that a carrier admits a non-trivial distinction is itself
distinguishable from the denial of that claim. -/
theorem dist_claim_self_distinguishes (K : Type*) :
    (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y) :=
  prop_ne_not (∃ x y : K, x ≠ y)

/-- The self-bootstrap certificate is theorem-backed. -/
theorem selfBootstrapCert : SelfBootstrapCert where
  meta_distinguishes := meta_language_distinguishes_props
  claim_not_its_negation := dist_claim_self_distinguishes

What this page does not claim

This module does not derive an object-level non-singleton carrier from nothing. The certificate does not establish that any particular physical carrier has two distinct elements. The module does not prove that the self-bootstrap argument succeeds in deriving object-level distinguishability from the meta-language alone.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/SelfBootstrapDistinguishability.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: