Leanにおける述語論理

今回は述語論理（predicate logic）を取り上げ、全称記号・存在記号を使った命題を Lean 4 で証明する方法を見ていきます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

述語論理とは

述語論理とは、述語を取り扱う論理学のことです。述語とは変数を含んだ命題のことで、変数に具体的な値を代入することで真偽が定まります。

述語を用いて論理式を組み立てる際には、次の二つの記号が導入されます。

• 全称記号（∀）：「任意の値が与えられたとき」という仮定を示します。「すべての x について P(x) が成り立つ」という命題を ∀ x, P x と書きます。
• 存在記号（∃）：命題を満たす値が少なくとも一つ存在することを示します。「P(x) を満たす x が存在する」という命題を ∃ x, P x と書きます。

全称記号 ∀ を使った証明

以下の例では、述語 P に対して全称記号を用いた命題を証明しています。

def P (n : Nat) : Prop := n = n

example : ∀ a : Nat, P a := by
  intro x
  dsimp [P]

intro タクティクは全称記号を仮定するために使います。「a が任意に与えられたとする」と宣言するようなイメージです。このステップの後、証明のゴールは ⊢ P x に変わります。

次に dsimp [P] を適用します。dsimp は Definitional Simplification（定義による単純化）というタクティクで、指定した定義を展開してゴールを簡略化します。P の定義 n = n を展開すると、ゴールは x = x という自明な等式になり、Lean が自動的に証明を閉じます。

存在記号 ∃ を使った証明

次に、存在記号を用いた命題の例です。

def even (n : Nat) : Prop := ∃ m : Nat, n = m + m

example : even 4 := by
  exists 2

even は偶数であることを示す述語です。n に対して n = m + m となる自然数 m が少なくとも一つ存在するという命題を表しています。

存在記号を含む命題の証明には exists タクティクを使います。存在が主張されている値を具体的に与えれば証明が完了します。ここでは exists 2 と書くことで、m = 2 のとき 4 = 2 + 2 が成り立つことを示しています。

仮定に存在記号が含まれる場合

仮定に存在記号が使われている場合は、obtain タクティクを使って、存在が仮定されている値を取り出すことができます。

example (α : Type) (P Q : α → Prop) (h : ∃ x : α, P x ∧ Q x)
  : ∃ x : α, Q x := by
  obtain ⟨y, hy⟩ := h
  exists y
  exact hy.right

仮定 h には「P x ∧ Q x を満たす x が存在する」という情報が含まれています。obtain ⟨y, hy⟩ := h と書くことで、その値を y : α として、y が満たす命題の証明を hy として取り出せます。

続いて exists y でゴールを ⊢ Q y に変更します。これは「y こそが Q x を満たす値である」と主張する段階に移ることを意味します。hy は P y ∧ Q y の証明を持っているので、hy.right で論理積の右側、すなわち Q y を取り出せば証明が完成します。