prop_ne_not

formal source

  36  cases hx.symm.trans hfalse
  37
  38/-- A proposition is never equal to its negation in classical logic. -/
  39theorem prop_ne_not (P : Prop) : P ≠ ¬ P := by
  40  intro h
  41  by_cases hp : P
  42  · have hnp : ¬ P := by
  43      rw [h] at hp
  44      exact hp
  45    exact hnp hp
  46  · have hp' : P := by
  47      rw [h.symm] at hp
  48      exact hp
  49    exact hp hp'
  50
  51/-- The claim that a carrier admits a non-trivial distinction is itself
  52distinguishable from the denial of that claim. -/
  53theorem dist_claim_self_distinguishes (K : Type*) :
  54    (∃ x y : K, x ≠ y) ≠ (¬ ∃ x y : K, x ≠ y) :=
  55  prop_ne_not (∃ x y : K, x ≠ y)
  56
  57/-- The meta-language has at least one non-trivial propositional distinction. -/
  58theorem meta_language_distinguishes_props : ∃ P Q : Prop, P ≠ Q :=
  59  ⟨True, False, by
  60    intro h
  61    have hf : False := by
  62      simpa [h] using True.intro
  63    exact False.elim hf⟩
  64
  65/-- Route A, honest form: object-level distinguishability is never weaker
  66than the meta-level fact that the formal language already distinguishes
  67`Prop` values. The object-level non-singleton condition is still named. -/
  68theorem distinguishability_forced_given_object_witness
  69    (K : Type*) (_h_meta_dist : ∃ P Q : Prop, P ≠ Q)