/- 用 Lean4 将下列自然语言转换为形式化语言：将前面几行前提作为 Axioms，最后一行的命题（或其否定）作为 Theorem 并证明它。-/

-- 例子
/-
Ax1: Babies are illogical;
Ax2: Nobody is despised who can manage a crocodile;
Ax3: Illogical persons are despised.
Prop: Babies cannot manage crocodiles.
-/

variable {Person : Type}

axiom baby : Person → Prop
axiom illogical : Person → Prop
axiom despised : Person → Prop
axiom manage : Person → Prop

axiom Ax1 : ∀ p : Person, baby p → illogical p
axiom Ax2 : ∀ p : Person, manage p → ¬ despised p
axiom Ax3 : ∀ p : Person, illogical p → despised p

theorem BabiesCannotManageCrocodiles :
  ∀ p : Person, baby p → ¬ manage p := by
  intro p hbaby hmanage
  have : illogical p := Ax1 p hbaby
  have : despised p := Ax3 p this
  have : ¬ despised p := Ax2 p hmanage
  contradiction

-- 题目1
/-
Ax1: Every one who is sane can do Logic.
Ax2: No lunatics are fit to serve on a jury.
Ax3: None of your sons can do logic.
Prop: None of your sons are fit to serve on a jury.
-/

-- 题目2
/-
Ax1: None of the unnoticed things, met with at sea, are mermaids.
Ax2: Things entered in the log, as met with at sea, are sure to be worth remembering.
Ax3: I have never met with anything worth remembering, when on a voyage.
Ax4: Things met with at sea, that are noticed, are sure to be recorded in the log.
Prop: I have never met with a mermaid.
-/

-- 题目3
/-
Ax1: No interesting poems are unpopular among people of real taste.
Ax2: No modern poetry is free from affectation.
Ax3: All your poems are on the subject of soap-bubbles.
Ax4: No affected poetry is popular among people of real taste.
Ax5: No ancient poem is on the subject of soap-bubbles.
Prop: Your poetry is not interesting.
-/