NontrivialSpecification

formal source

  18/-- A non-trivial specification of a sub-ontology inside a universe of
  19discourse `K`: a predicate that holds for at least one element and fails
  20for at least one element. -/
  21structure NontrivialSpecification (K : Type*) where
  22  inOntology : K → Prop
  23  someInside : ∃ x : K, inOntology x
  24  someOutside : ∃ x : K, ¬ inOntology x
  25
  26/-- Specifiability forces distinguishability. -/
  27theorem distinguishability_from_specification
  28    {K : Type*} (S : NontrivialSpecification K) :
  29    ∃ x y : K, x ≠ y := by
  30  obtain ⟨P, ⟨x, hx⟩, ⟨y, hy⟩⟩ := S
  31  refine ⟨x, y, ?_⟩
  32  intro hxy
  33  have hyx : P y := by
  34    simpa [hxy] using hx
  35  exact hy hyx
  36
  37/-- Any non-empty proper subtype is a non-trivial specification. -/
  38def nontrivial_specification_of_proper_subtype
  39    {K : Type*} (S : Set K)
  40    (hin : ∃ x : K, x ∈ S) (hout : ∃ x : K, x ∉ S) :
  41    NontrivialSpecification K where
  42  inOntology := fun x => x ∈ S
  43  someInside := hin
  44  someOutside := hout
  45
  46/-- If an ontology is a proper, non-empty subset of its universe of discourse,
  47then it defines a non-trivial specification. -/
  48def nontrivial_spec_from_proper_ontology
  49    {K : Type*} (Ω : Set K)
  50    (h_inhabited : ∃ x : K, x ∈ Ω)
  51    (h_proper : ∃ x : K, x ∉ Ω) :