logic quiz: favorite books

Stream: general

[Bulhwi Cha]

Quiz 1: Bulhwi (he/him) likes all those books, and only those, which are only about exactly one person who likes all and only those books that Bulhwi likes. If Boram had written a book only about Bulhwi, would Bulhwi like it?

Quiz 2: Boram (she/her) likes all those books, and only those, which are only about exactly one person who doesn't like all and only those books that Boram likes. If Bulhwi had written a book only about Boram, would Boram like it?

I attempted to come up with a paradox, but instead, I've created two questions about logic.

My solutions

-- this code is written in Lean 4.25.0

class FavoriteBooks (Human : Type u) (Book : Type v) where
  Likes : Human → Book → Prop
  IsOnlyAbout : Book → Human → Prop
  isOnlyAbout_functional {b : Book} {x y : Human} (h₁ : IsOnlyAbout b x) (h₂ : IsOnlyAbout b y) :
    x = y

section

infix:55 " likes " => FavoriteBooks.Likes
infix:55 " is_only_about " => FavoriteBooks.IsOnlyAbout

variable {Human : Type u} {Book : Type u} [FavoriteBooks Human Book]

theorem quiz01
    {bulhwi : Human}
    (bulhwi_likes : ∀ {b : Book}, bulhwi likes b ↔
      ∃ (x : Human), b is_only_about x ∧ ∀ {c : Book}, x likes c ↔ bulhwi likes c)
    {boram's_book : Book}
    (book_isOnlyAbout : boram's_book is_only_about bulhwi) :
    bulhwi likes boram's_book := by
  rw [bulhwi_likes]
  exists bulhwi

theorem quiz02
    {boram : Human}
    (boram_likes : ∀ {b : Book}, boram likes b ↔
      ∃ (x : Human), b is_only_about x ∧ ∀ {c : Book}, ¬x likes c ↔ boram likes c)
    {bulhwi's_book : Book}
    (book_isOnlyAbout : bulhwi's_book is_only_about boram) :
    ¬boram likes bulhwi's_book := by
  intro h
  rw [boram_likes] at h
  let ⟨x, h₁, h₂⟩ := h
  have heq : x = boram := FavoriteBooks.isOnlyAbout_functional h₁ book_isOnlyAbout
  subst x
  exact not_iff_self (@h₂ bulhwi's_book)