Foundation Distinguishability From Specifiability Nontrivial Spec From Proper On

Specifiability and distinction

In mathematics, a specification is a rule that picks out some objects from a larger collection. The collection is often called the universe of discourse, and the rule is a predicate: a property that each object either has or lacks. A non-trivial specification is one that is neither empty nor everything: it holds for at least one object in the universe and fails for at least one other. For example, in the universe of whole numbers, the rule "is even" is non-trivial because some numbers are even and some are not. The rule "is a number" is trivial because it holds for every object in the universe.

The Recognition Science framework's machine-checked library of formal theorems proves a small but sharp point about such specifications. If a universe admits a non-trivial specification, then that universe must contain at least two distinct objects. The reason is immediate: the rule holds for one object and fails for another, so those two objects cannot be the same. The framework packages this observation as a theorem named distinguishability_from_specification. It also provides a construction, nontrivial_spec_from_proper_ontology, that turns any proper, non-empty subset of a universe into such a specification. If an ontology, meaning a chosen sub-collection of objects, has something inside it and something outside it, then that ontology itself certifies that the universe has at least two distinct elements.

The framework goes further and proves the converse on an inhabited carrier. If a universe has at least one element and admits no non-trivial specification at all, then the universe has at most one element. Taken together, the two directions form an equivalence: on a non-empty carrier, the existence of a non-trivial specification is exactly equivalent to the existence of two distinct objects. The framework records this equivalence as the theorem distinguishability_iff_nontrivial_specifiability and packages it in a certificate structure called SpecifiabilityClosureCert. The certificate is theorem-backed, meaning it is derived from the formal proofs rather than assumed.

In Recognition Science, this result provides a route to the absolute floor: the framework's program of finding the minimal assumptions that force structure. The point is that the ability to specify an ontology with something inside and something outside already delivers the distinction between objects that the framework's broader chain of results needs. The framework does not claim that any particular specification is meaningful or that the universe must be specified in any particular way. It claims only the conditional: if a non-trivial specification exists, then distinction exists. The construction also does not claim that the two objects are distinguishable by any further property; it proves only that they are not identical. The equivalence holds for any non-empty carrier, with no additional assumptions about the nature of the objects or the specification rule.

/-- Specifiability forces distinguishability. -/
theorem distinguishability_from_specification
    {K : Type*} (S : NontrivialSpecification K) :
    ∃ x y : K, x ≠ y := by
  obtain ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ := S
  refine ⟨x, y, ?_⟩
  intro hxy
  have hyx : P y := by
    simpa [hxy] using hx
  exact hy hyx

/-- If an ontology is a proper, non-empty subset of its universe of discourse,
then it defines a non-trivial specification. -/
def nontrivial_spec_from_proper_ontology
    {K : Type*} (Ω : Set K)
    (h_inhabited : ∃ x : K, x ∈ Ω)
    (h_proper : ∃ x : K, x ∉ Ω) :
    NontrivialSpecification K :=
  nontrivial_specification_of_proper_subtype Ω h_inhabited h_proper

/-- If no non-trivial specification exists on an inhabited carrier, then the
carrier has at most one element. -/
theorem at_most_one_of_no_nontrivial_specification
    {K : Type*} [Nonempty K]
    (h_no_nts : ¬ Nonempty (NontrivialSpecification K)) :
    ∀ x y : K, x = y := by
  intro x y
  by_contra hxy
  apply h_no_nts
  have hy_ne_x : y ≠ x := by
    intro hyx
    exact hxy hyx.symm
  exact ⟨
    { inOntology := fun z => z = x
      someInside := ⟨x, rfl⟩
      someOutside := ⟨y, hy_ne_x⟩ }⟩

/-- Non-trivial specifiability is equivalent to object-level
distinguishability on an inhabited carrier. -/
theorem distinguishability_iff_nontrivial_specifiability
    {K : Type*} [Nonempty K] :
    (∃ x y : K, x ≠ y) ↔ Nonempty (NontrivialSpecification K) := by
  constructor
  · rintro ⟨x, y, hxy⟩
    have hy_ne_x : y ≠ x := by
      intro hyx
      exact hxy hyx.symm
    exact ⟨
      { inOntology := fun z => z = x
        someInside := ⟨x, rfl⟩
        someOutside := ⟨y, hy_ne_x⟩ }⟩
  · rintro ⟨S⟩
    exact distinguishability_from_specification S

What this page does not claim

The theorem does not claim that any particular specification is meaningful or that the universe must be specified in any particular way. The construction does not claim that the two distinct objects are distinguishable by any further property beyond non-identity. The equivalence does not claim anything about carriers that are empty, since it requires a non-empty 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/DistinguishabilityFromSpecifiability.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: