nontrivial_specification_of_proper_subtype
plain-language theorem explainer
Any non-empty proper subset S of a type K defines a non-trivial specification by taking the ontology predicate to be membership in S. Researchers on the absolute-floor program cite this when converting a proper ontology into the structure needed for distinguishability. The definition is a direct constructor application that supplies the required existence witnesses hin and hout.
Claim. Let $K$ be a type and $Ssubseteq K$ a set such that there exists $x in K$ with $x in S$ and there exists $y in K$ with $y notin S$. Then $S$ induces a non-trivial specification of an ontology in $K$ whose predicate is membership in $S$.
background
The module DistinguishabilityFromSpecifiability implements Route B for the absolute-floor program. Its central point is that a non-trivial specification is equivalent to a non-singleton carrier: if a framework can specify an ontology with something inside and something outside, it already has the distinction needed by the Law-of-Logic chain. The structure NontrivialSpecification (K : Type*) consists of a predicate inOntology : K → Prop together with witnesses someInside : ∃ x : K, inOntology x and someOutside : ∃ x : K, ¬ inOntology x.
proof idea
This is a definition that constructs an instance of NontrivialSpecification by setting inOntology to the membership predicate for S and assigning the supplied existence hypotheses hin and hout directly to someInside and someOutside. It is a one-line wrapper around the structure constructor.
why it matters
This definition supplies the basic construction used by nontrivial_spec_from_proper_ontology to convert a proper ontology into a non-trivial specification. It fills the role in the absolute-floor program of showing that any framework capable of specifying an ontology with something inside and outside already possesses the distinction required by the Law-of-Logic chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.