Foundation Self Bootstrap Distinguishability Prop Ne Not

The distinction claim

In classical logic, a proposition P and its negation ¬P are always distinct: they cannot be the same statement. This is not a deep physical law but a basic fact about how logical statements work. The Recognition Science framework's declaration prop_ne_not states this formally: for any proposition P, P is not equal to ¬P. The proof is short and proceeds by contradiction: if P equaled its negation, then assuming P would force ¬P, and assuming ¬P would force P, so either way the logic collapses. The theorem is machine-checked in the framework's library of formal theorems.

The declaration is part of a larger program the framework calls the self-bootstrap argument, which asks how a physical theory can get started from minimal assumptions. One route, called Route A, tries to show that the world must contain at least two distinguishable things. The framework is careful about what this route can and cannot prove. prop_ne_not does not prove that any physical carrier has two distinct elements. What it proves is a meta-level fact: the formal language itself already distinguishes propositions, and the claim that a carrier has two distinct elements is itself distinct from the denial of that claim. In other words, the statement "there exist two different things" is not the same as the statement "there do not exist two different things."

The framework packages this into a certificate structure called SelfBootstrapCert, which records two facts: the meta-language distinguishes propositions, and the object-level distinguishability claim is not its own negation. The certificate is theorem-backed, meaning the framework's library proves it holds. But the certificate explicitly stops at the meta-language floor. It does not derive an object-level non-singleton carrier from nothing. The framework names this limitation plainly in its own documentation: the route "does not pretend to derive an object-level non-singleton carrier from nothing."

What prop_ne_not changes is the boundary of what the self-bootstrap argument can claim. It establishes that the logical language has at least one non-trivial distinction, and that the proposition asserting object-level distinguishability is distinct from its denial. That is a precise, checkable result. What remains open is whether any physical carrier actually has two distinct elements; that requires a separate witness, which the framework does not supply here.

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

prop_ne_not does not prove that any physical carrier has two distinct elements. The self-bootstrap argument does not derive an object-level non-singleton carrier from nothing.

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: