distinguishability_from_specification
plain-language theorem explainer
Specifiability of a non-trivial sub-ontology on a type K forces the existence of at least two distinct elements in K. Researchers tracing Route B of the absolute-floor program cite this result to ground the Law-of-Logic chain in basic distinguishability. The proof extracts the predicate and its inside/outside witnesses from the NontrivialSpecification structure then derives a contradiction from the assumption that those witnesses coincide.
Claim. Let $K$ be a type. Suppose there exists a predicate $P : K → Prop$ together with witnesses $x, y : K$ such that $P(x)$ and $¬P(y)$. Then there exist distinct elements $a, b ∈ K$.
background
The module DistinguishabilityFromSpecifiability implements Route B for the absolute-floor program. Its central structure NontrivialSpecification K packages a predicate inOntology : K → Prop with two existential witnesses: someInside asserting that the predicate holds for at least one element and someOutside asserting that it fails for at least one element. The module documentation states that such a specification already supplies the distinction needed by the Law-of-Logic chain.
proof idea
The tactic proof obtains the components ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ directly from the NontrivialSpecification hypothesis S. It refines the goal to the pair x, y together with a proof of inequality. Assuming x = y, the simpa tactic substitutes to produce P y from hx, which contradicts the witness hy : ¬P y.
why it matters
This theorem supplies the forward direction of the equivalence proved in the downstream result distinguishability_iff_nontrivial_specifiability. It fills the key step in Route B of the absolute-floor program, showing that specifiability forces distinguishability as required by the Law-of-Logic chain. The parent equivalence then equates non-singleton carriers with the existence of NontrivialSpecification instances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.