On veut démontrer ceci:

∀R.A ⊑ ¬∃R.⊤ ⊔ ∃R.A

Supposons donc qu'il existe une entité x telle que:

  (∀R.A)(x)

et

  ¬(¬∃R.⊤ ⊔ ∃R.A)(x)

Voici ce qu'on peut inférer:

  (∀R.A)(x)
  (∃R.⊤ ⊔ ¬∃R.A)(x)
  (∃R.⊤ ⊓ ∀R.¬A)(x)
  (∃R.⊤)(x)
  (∀R.¬A)(x)
  R(x,y)
  A(y)
  ¬A(y)
  Contradiction!
Last modified: Sunday, 14 November 2021, 4:51 PM