色恋で述語論理の例を作る

[Seasawher]

opaque People : Type

/-- A さんは B さんのことが好き（愛している）という述語 -/
opaque love (a b : People) : Prop

@[inherit_doc] infix:70 " -♥→ " => love

/-- 「すべての人は誰かに好かれている」ことを表す命題 -/
def everyone_loved_someone : Prop :=
  ∀ p : People, ∃ q : People, q -♥→ p

/-- 「誰にでも好きな人がいる」ことを表す命題 -/
def everyone_loves_someone : Prop :=
  ∀ p : People, ∃ q : People, p -♥→ q

/-- 「すべての人を愛している博愛主義者がいる」という命題 -/
def exists_who_loves_all : Prop :=
  ∃ p : People, ∀ q : People, p -♥→ q

/-- 博愛主義者が存在するなら、すべての人は誰かに好かれている -/
example (h : exists_who_loves_all) : everyone_loved_someone := by
  intro p
  obtain ⟨phi, h⟩ := h
  exists phi
  apply h

/-- ナルシシスト（自分だけを愛している）であることを表す述語 -/
def narcis (p : People) : Prop :=
  ∀ q : People, p -♥→ q ↔ q = p

/-- 「自分のことを愛してくれる人のことが好き」という述語 -/
def returnLove (p : People) : Prop :=
  ∀ q : People, q -♥→ p ↔ p -♥→ q

[Seasawher]

色恋で例を作るとイメージしやすいのでわかりやすいだろうという考え。

ただし、あまり本質的な例とも思えないので引っ張るべきではない。