背景
在命題邏輯中，我們討論了一些或真或假的命題之間的關係，例如我們可以記”蘋果是紅色的”為命題 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 是等價的。
這裡使用了 Iff.rfl（自反律），表示對於任何命題 a, a ↔︎ a。我們可以用 #check 指令查看 Iff.rfl 的類型：
#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 pExists.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) : bExists.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 Exists.intro w (And.intro hw.right hw.left))一些有用的工具
自動匹配構造函數
在Lean中，⟨⟩ 能自動匹配構造函數的類型和參數。
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 關鍵詞
你還可以結合 match 語句進一步簡化上面的證明：
example (h : ∃ x, p x ∧ q x) : ∃ x, q x ∧ p x :=
match h with
| ⟨w, hw⟩ => ⟨w, hw.right, hw.left⟩練習
在這個部分的練習中，你可以使用經典邏輯。（但不是所有證明都需要使用經典邏輯，你可以自行判斷。）
證明：(∀ x, p x ∧ q x) ↔︎ (∀ x, p x) ∧ (∀ x, q x)
參考答案
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)
)
)證明：(∀ x, p x → q x) → (∀ x, p x) → (∀ x, q 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證明：(∀ x, p x) ∨ (∀ x, q x) → ∀ x, p x ∨ q x
參考答案
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)
)證明 (∃ x : α, r) → r
參考答案
example : (∃ x : α, r) → r :=
fun h : (∃ x : α, r) =>
Exists.elim h
(
fun (w : α) (hr : r) =>
hr
)證明 (a : α) : r → (∃ x : α, r)
參考答案
example (a : α) : r → (∃ x : α, r) :=
fun (h : r) =>
Exists.intro a h證明：(∃ x, p x ∧ r) ↔︎ (∃ x, p x) ∧ r
參考答案
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)
)
)證明：(∃ x, p x ∨ q x) ↔︎ (∃ x, p x) ∨ (∃ x, q x)
參考答案
example : (∃ x, p x ∨ q x) ↔ (∃ x, p x) ∨ (∃ x, q x) :=
Iff.intro
(
fun h : (∃ x, p x ∨ q x) =>
Exists.elim h
(
fun w (hpwqw : p w ∨ q w) =>
Or.elim hpwqw
(
fun hpw : p w =>
Or.intro_left (∃ x, q x)
(Exists.intro w hpw)
)
(
fun hqw : q w =>
Or.intro_right (∃ x, p x)
(Exists.intro w hqw)
)
)
)
(
fun h : (∃ x, p x) ∨ (∃ x, q x) =>
Or.elim h
(
fun hpw : (∃ x, p x) =>
Exists.elim hpw
(
fun w (hpw : p w) =>
Exists.intro w (Or.intro_left (q w) hpw)
)
)
(
fun hqw : (∃ x, q x) =>
Exists.elim hqw
(
fun w (hqw : q w) =>
Exists.intro w (Or.intro_right (p w) hqw)
)
)
)
