一階述語論理の項モード対応表

🛠️ 一階述語論理の項モード対応表：データ構築ガイド

論理記号	導入則 (データを作る)	除去則 (データを使う)
全称 ∀x, P(x)	fun x ↦ ... (値を引数に取る)	h t (値 t を関数 h に渡す)
存在 ∃x, P(x)	⟨t, h_proof⟩ (値と証明のペア)	h.elim (fun x hx ↦ ...)
等号 s = t	rfl (反射律)	h.subst h_px または h ▸ h_px

---

1. 全称記号 ∀：それは「関数」である

命題論理の「ならば ->」が「証明を引数に取る関数」だったのに対し、全称記号は 「値を引数に取る関数」 です。

• 導入 (fun): 「任意の x を渡されたら、どうやって P(x) の証明を作るか」というレシピ。
• 除去 (適用): 手持ちの全称命題 に、具体的な値 を適用します。

-- 導入
variable (U : Type) (P : U → Prop)
example : ∀ x, P x := fun x ↦ _ -- この穴で P x を作ればよい

-- 除去
example (h : ∀ x, P x) (a : U) : P a := h a -- 関数適用そのもの

---

2. 存在記号 ∃：それは「証拠品とのセット」である

存在記号は、「かつ ^」の親戚です。「具体的なモノ 」と「それが性質を満たしている証明」の2つを詰め込んだ 「依存ペア」 です。

• 導入 (⟨ ⟩): 証拠となる値 と、その証明 をセットにします。
• 除去 (.elim): 「証拠品を 、その証明を と名付けて、それらを使って結論を作る」という処理関数を渡します。

-- 導入
example (a : U) (ha : P a) : ∃ x, P x := ⟨a, ha⟩

-- 除去
example (h : ∃ x, P x) : Q :=
  h.elim (fun x hx ↦
    _ -- ここで x と hx を使って Q を作る
  )

---

3. 等号 ()：それは「書き換えの権利」である

• 導入 (rfl): 左右が（定義上）同じであれば、rfl と書くだけで証明データになります。
• 除去 (subst / ▸): 等式 を使って、ある証明 の中の を に置き換えます。

-- 導入
example (x : U) : x = x := rfl

-- 除去 (subst)
example (x y : U) (h : x = y) (px : P x) : P y := h.subst px

-- 除去 (▸記法 / マクロ)
-- Mathlibで非常によく使われる「等号による流し込み」のショートカットです
example (x y : U) (h : x = y) (px : P x) : P y := h ▸ px

---

4. 等号の便利な道具箱 (Eq系)

等号に関しては、関数的な定数が用意されています。

• Eq.symm h: を にひっくり返す。
• Eq.trans h1 h2: と から を作る。
• congrArg f h: から を作る。

---

5. 理髪師のパラドックスで見る「項モード」の組み立て

「自分を剃らない者だけを剃る理髪師 」がいると仮定して矛盾を導く例： h : ∀ x, shaves b x ↔ ¬ shaves x x

example (h : ∀ x, shaves b x ↔ ¬ shaves x x) : False :=
  -- 1. まず全称記号を除去して、理髪師本人についての同値式を取り出す
  let h_self : shaves b b ↔ ¬ shaves b b := h b

  -- 2. 「P ↔ ¬P」は矛盾であるという命題論理の知識を使う
  -- (これ自体も fun を使った項モードで書ける)
  not_iff_not_self (shaves b b) h_self

---

6. 項モード設計のコツ（一階述語論理版）

① 山括弧 ⟨ ⟩ の入れ子を恐れない

存在記号が重なっている場合（）、項モードでは単純な入れ子のペアになります。 ⟨x, ⟨y, hrxy⟩⟩

② 匿名引数 _ の活用

全称記号の除去 h a などで、Leanが型から値を推論できる場合は h _ と書けます。ただし、値そのもの（証拠品）を指定する場合は省略できません。

③ インラインタクティクの使いどころ

等号の変形が複雑な場合、そこだけ by rw [h] を差し込むのが Mathlib 流です。

⟨ x, by rw [h1, h2]; exact h3 ⟩

---

💡 まとめ：項モードの「手触り」

• ∀ は「パイプ」**: 値を流し込むと、その値専用の命題が出てくる。
• ∃ は「カプセル」**: 中身（値と証明）を取り出すには .elim か match が必要。
• = は「コンバーター」**: ある型の証明を、別の型の証明へ変換する。

---

1. Skeleton：外側から「枠」を決める

ゴールの形を見て、最初の「一行」を _ 付きで書く習慣は同じです。

• ゴールが∀ x, P xなら： fun x ↦ _ （まず「任意の 」という材料を確保する）
• ゴールが∃ x, P xなら： ⟨ _ , _ ⟩ （「具体的な値」と「その証明」の2つの穴を作る）

2. Inspect：_ (ホール) との対話

ここで Infoview が出す情報が、一階述語論理ではより具体的になります。

example : ∃ x, P x :=
  ⟨ _ , _ ⟩

この時、Infoview を見ると：

• 1つ目の _：Expected type: U （**具体的な「値」**を入れろと言われる）
• 2つ目の _：Expected type: P ?m.1 （その値が 性質を満たす「証明」 を入れろと言われる）

このように、「何を（値）」探して、「何（証明）」を示すべきかを Lean が常に教えてくれます。

3. ドット記法による探索

仮定（Hypothesis）が量化記号を持っている場合、ドット記法はさらに強力です。

• 存在記号の仮定 h : ∃ x, P x の場合： h. と打つと elim が出てきます。 → h.elim (fun x hx ↦ _) と展開する指針が即座に立ちます。
• 全称記号の仮定 h : ∀ x, P x の場合： 全称記号は「関数」なので、ドット記法よりも h _（引数を渡す）という操作がメインになります。

---

4. 古典論理（Classical）の「魔法の定数」

一階述語論理特有の「魔法の定数」も項モードで呼び出せます。

• Classical.choose h： 存在証明 h : ∃ x, P x から、**具体的な「その中身の値」**を強引に取り出します。
• Classical.choose_spec h： choose で取り出した値が、確かに性質 P を満たしているという証明を取り出します。

注意: これらは Exists.elim（非古典的/安全な分解）を使わずに、値を直接「ぶっこ抜く」操作です。

---

5. ハイブリッド利用：by の使いどころ

一階述語論理では、「値を見つけるのは人間、その後の書き換えは Lean」 という分担が効率的です。

example (h : ∃ x, x = a) : ∃ x, x = a :=
  let ⟨val, spec⟩ := h
  ⟨val, by rw [spec]⟩ -- 値は項モードで維持し、等号の変形だけタクティクに任せる

---

💡 一階述語論理版：デバッグ・サイクル

1. Skeleton: fun x ↦ _ や ⟨ _ , _ ⟩ で、証明の「入れ物」を作る。
2. Inspect: _ が「値（U）」を求めているのか「証明（Prop）」を求めているのかを確認する。
3. Refine:

• 値が必要なら、コンテキストにある変数や定数を入れる。
• 証明が必要なら、手持ちの全称命題 h に値を適用して h x などを作る。

4. Polish: h ▸ hx などの便利な記法を使って、見た目を整える。