distinguishability_from_specification

formal source

  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 ∉ Ω) :
  52    NontrivialSpecification K :=
  53  nontrivial_specification_of_proper_subtype Ω h_inhabited h_proper
  54
  55/-- If no non-trivial specification exists on an inhabited carrier, then the
  56carrier has at most one element. -/
  57theorem at_most_one_of_no_nontrivial_specification