在命题逻辑中，我们讨论了一些或真或假的命题之间的关系，例如我们可以记“苹果是红色的”为命题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)
          )
    )