在命題邏輯中，我們討論了一些或真或假的命題之間的關係，例如我們可以記“蘋果是紅色的”為命題p，然後基於p進行一些運算。

命題邏輯又被稱爲0階邏輯。而一階邏輯從更細的粒度分析“句子”。例如，我們可以引入一個“謂詞”IsRed來表示“是紅色的”，用(IsRed Apple)表示蘋果是紅色的。

當變量為兩個時，一階邏輯引入“關係”的概念。例如對於“馬克思和孔子是朋友”，我們可以設IsFriend是一個關係，用(IsFriend 馬克思 孔子)表示“馬克思和孔子是朋友”。

一階邏輯還引入了全稱量詞“∀”和存在量詞“∃”。例如，我們可以說“所有的蘋果都是紅色的”，用∀ (x : Apple), IsRed x表示。我們也可以說“存在有不是紅色的蘋果”，可以表示為∃ (x : Apple), ¬(IsRed x).

-- 本章會使用如下的變量
variable (α : Type) (p q : α → Prop) (r : Prop)

接下來我們介紹全稱量詞“\(\forall\)”、存在量詞“\(\exists\)”。

∀ x : α, p x表示對於任意x : α，都有p x成立。這裡p的類型為α → Prop，如前所述，是一個“謂詞”。

在Lean語言中，對於任意的表達式prop，∀ x : α, prop都等同於(x : α) → prop. 前者是一個使用了全稱量詞的表達式，而後者是一個函數，但它們的含義是相同的。

下面這個例子清楚的展示了這點。

example : (∀ x : α, p x) ↔ ((x : α) → p x) := Iff.rfl

上面的證明表示∀ x : α, p x和(x : α) → p x是等價的。

#check Iff.rfl -- Iff.rfl {a : Prop} : a ↔ a

下面這個例子很好地展示了全稱量詞和函數之間的關係：

example (α : Type) (p q : α → Prop) : (∀ x : α, p x ∧ q x) → ∀ y : α, p y :=
  fun h : ∀ x : α, p x ∧ q x =>
  -- 我們需要證明∀ y : α, p y，即函數y : α → p y
  fun y : α =>
  -- 只需證明p y
  show p y from (h y).left
  -- 注意h的類型為∀ x : α, p x ∧ q x. h也可以作為函數使用。

∃ x : α, p x表示存在x : α使得p x成立，也可以寫作exists x : α, p x或者Exists (fun x : α => p x). 從下面的證明可以看出，這幾種寫法是等價的。

example : (∃ x : α, p x) ↔ exists x : α, p x := Iff.rfl
example : (∃ x : α, p x) ↔ Exists (fun x : α => p x) := Iff.rfl

關於存在量詞的兩條重要規則是Exists.intro（引入）和Exists.elim（消去）。

#check Exists.intro
-- Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p

Exists.intro表明如果存在w : α且h : p a成立，那麼⟨a, h⟩就構成∃ x : α, p x的證明.

下面這個例子是關於“存在大於零的自然數”的證明：

example : ∃ x : Nat, x > 0 :=
  -- 首先，我們先舉例說明，1就是一個大於零的自然數。將這個證明命名為`h`.
  have h : 1 > 0 := Nat.zero_lt_succ 0
  -- 那麼，⟨1, h⟩就是一個對於該命題的證明
  Exists.intro 1 h

接下來介紹Exists.elim：

#check Exists.elim
-- Exists.elim.{u} {α : Sort u} {p : α → Prop} {b : Prop} (h₁ : ∃ x, p x) (h₂ : ∀ (a : α), p a → b) : b

Exists.elim表明如果∃ x, p x成立，且∀ (a : α), p a → b，那麼命題b成立。

之前說過，∀ (a : α), p a → b等價於(a : α) → (p a → b)，因此在實際使用中，我們需要構造一個類型為(a : α) → (p a → b)的函數

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  Exists.elim h
    -- 接下來我們需要證明∀ (w : α), p w ∧ q w → ∃ x, q x ∧ p x
    (fun w =>
     fun hw : p w ∧ q w =>
     -- 已知 p w ∧ q w ，只需證明∃ x, q x ∧ p x
     show ∃ x, q x ∧ p x from ⟨w, hw.right, hw.left⟩)

上面的例子使用了⟨w, hw.right, hw.left⟩來構造∃ x, q x ∧ p x，這是因為⟨⟩能自動匹配改造函數的類型和參數。⟨⟩的輸入方式是在編輯器中依次輸入\<>。

你還可以結合match語句進一步簡化上面的證明：

example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
  match h with
  | ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩

在這個部分的練習中，你可以使用經典邏輯。(但不是所有證明都需要使用經典邏輯，你可以自行判斷。)

example : (∀ x, p x ∧ q x) ↔ (∀ x, p x) ∧ (∀ x, q x) :=
  Iff.intro
    (
      fun h : (∀ x, p x ∧ q x) =>
        And.intro
          (fun x => (h x).left)
          (fun x => (h x).right)
    )
    (
      fun h : (∀ x, p x) ∧ (∀ x, q x) =>
        (
          fun x =>
            And.intro (h.left x) (h.right x)
        )
    )

example : (∀ x, p x → q x) → (∀ x, p x) → (∀ x, q x) :=
  fun (h1 : ∀ x, p x → q x) (h2 : ∀ x, p x) =>
    fun x =>
      have px : (p x) := (h2 x)
      show q x from h1 x px

example : (∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x :=
  fun h :( ∀ x, p x) ∨ (∀ x, q x) =>
    fun x =>
      Or.elim h
        (
          fun hxpx : (∀ x, p x) =>
            Or.intro_left (q x) (hxpx x)
        )
        (
          fun hxqx : (∀ x, q x) =>
            Or.intro_right (p x) (hxqx x)
        )

example : (∃ x : α, r) → r :=
  fun h : (∃ x : α, r) =>
    Exists.elim h
      (
        fun (w : α) (hr : r)=>
          hr
      )

example (a : α) : r → (∃ x : α, r) :=
  fun (h : r) =>
    Exists.intro a h

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
  Iff.intro
    (
      fun h : (∃ x, p x ∧ r) =>
        Exists.elim h
          (
            fun w (hpwr : p w ∧ r) =>
              And.intro
                (Exists.intro w hpwr.left)
                hpwr.right
          )
    )
    (
      fun h : (∃ x, p x) ∧ r =>
        Exists.elim h.left
          (
            fun w (hpw : p w) =>
              Exists.intro w (And.intro hpw h.right)
          )
    )