Foundation Self Bootstrap Distinguishability Distinguishability Lifted From Bool

The distinction lemma

Distinguishability is the ability to tell two things apart. In mathematics, a common way to express this is with a function that returns either "true" or "false" for each object in a collection. Such a function is called a Boolean predicate. The theorem distinguishability_lifted_from_bool states a simple fact: if a Boolean predicate takes the value "true" for at least one object and "false" for at least one object, then there exist two distinct objects in the collection. The proof is immediate: pick one object where the predicate is true and another where it is false. If these were the same object, the predicate would have to be both true and false at once, which is impossible.

This result is part of a larger argument called the self-bootstrap, which asks how any notion of difference can get started in a formal system. The theorem does not create difference out of nothing. It only shows that a difference already present in the predicate, the difference between true and false, transfers to the objects being classified. The two-element type Bool, containing just "true" and "false", already carries a definitional distinction: the theorem bool_distinguishable proves that false is not equal to true. The lifted theorem then carries that distinction up to any carrier that supports a Boolean predicate with both outcomes.

In Recognition Science, this lemma is a meta-level fact. It shows that the formal language itself already distinguishes propositions: the proposition asserting that a carrier has two distinct elements is never equal to its own denial. This is proved by prop_ne_not and dist_claim_self_distinguishes. The framework's library, a machine-checked collection of formal theorems, records these facts as a certificate. The certificate states that the meta-language distinguishes propositions and that the claim of object-level distinguishability is distinct from its negation. It does not pretend to derive an object-level non-singleton carrier from nothing.

The honest form of the argument, distinguishability_forced_given_object_witness, makes the limit explicit. Given a meta-level distinction between propositions and a witness that a carrier has at least two elements, the theorem returns that witness unchanged. The self-bootstrap route closes at the meta-language floor, not below it. This means the framework proves the meta-level facts used by the argument, but the object-level condition of having two distinct elements remains a named premise, not a derived conclusion.

/-- 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

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

/-- 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)

/-- Route A, honest form: object-level distinguishability is never weaker
than the meta-level fact that the formal language already distinguishes
`Prop` values. The object-level non-singleton condition is still named. -/
theorem distinguishability_forced_given_object_witness
    (K : Type*) (_h_meta_dist : ∃ P Q : Prop, P ≠ Q)
    (h_at_least_two_in_carrier : ∃ x y : K, x ≠ y) :
    ∃ x y : K, x ≠ y :=
  h_at_least_two_in_carrier

What this page does not claim

This theorem does not derive the existence of two distinct objects from nothing; it requires a Boolean predicate with both truth values as input. This theorem does not prove that any particular carrier, such as the real numbers or physical space, has two distinct elements. This theorem does not establish that the meta-language distinction between propositions is the same as an object-level distinction in any specific model.

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: