Foundation Self Bootstrap Distinguishability Meta Language Distinguishes Props

The meta-language floor

A formal language is a system of symbols and rules for combining them. The distinction between a true proposition and a false one is the most basic separation any such language can make. The machine-checked theorem meta_language_distinguishes_props establishes that the language of the framework itself already makes this separation: there exist two propositions, True and False, that are not equal to each other. This is a fact about the formal system, not about the physical world.

The theorem is part of a larger argument the framework calls the self-bootstrap route. The route asks whether the framework can derive the existence of distinct objects from its own structure. The theorem proves one piece of that route: the formal language itself is not a single undifferentiated blob. It can tell True apart from False. The proof is direct and does not rely on any physical assumption.

The framework's library also proves a related fact: no proposition is equal to its own negation. If a proposition P were equal to not P, then assuming P would force not P, and assuming not P would force P. Classical logic rules this out. The theorem dist_claim_self_distinguishes applies this to the specific claim that a carrier has at least two distinct elements. That claim is itself distinguishable from its denial.

What the theorem does not do is derive the physical world. It does not prove that any actual object exists, or that space has points, or that matter has parts. The theorem operates entirely at the level of the formal language. The framework is explicit about this limit: the object-level condition, that a carrier actually has two distinct elements, remains a named assumption. The theorem shows the meta-language floor is solid, but it does not climb from that floor to the physical world.

In Recognition Science, this result is a checkpoint. The self-bootstrap route closes at the meta-language floor, not below it. The framework models the physical world as a ledger of recognition events, but this theorem does not establish that ledger. It establishes only that the formal language in which the framework is written already contains a basic distinction. That distinction is a precondition for any further claim, not a proof of one.

The practical consequence is modest but real. Anyone building on the framework knows that the formal foundation is not empty: the language itself distinguishes propositions. This is a theorem-backed fact, not a hope. But the step from that formal fact to a physical carrier with distinct elements remains open. The framework names that step honestly and does not pretend the theorem has closed it.

/-- The meta-language has at least one non-trivial propositional distinction. -/
theorem meta_language_distinguishes_props : ∃ P Q : Prop, P ≠ Q :=
  ⟨True, False, by
    intro h
    have hf : False := by
      simpa [h] using True.intro
    exact False.elim hf⟩

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

What this page does not claim

This theorem does not prove that any physical object exists. This theorem does not establish the ledger of recognition events. This theorem does not derive the existence of distinct elements in any actual carrier.

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: