---
title: Theorem Proving in Lean4 を読む会#4 ― 第3章 3.3-3.7
tags: 
author: [Yuki Imamura](https://image.docswell.com/user/imamuray)
site: [Docswell](https://www.docswell.com/)
thumbnail: https://bcdn.docswell.com/page/YJ6MNWKL7V.jpg?width=480
description: 2026/11/06 [Lean] Theorem proving in Lean4 読書会 /ゆるIT勉強会 で発表した資料です。 イベントページ：https://yurufuwait-hmmt-online.connpass.com/event/411735/  Theorem Proving in Lean 4 を Lean 入門者向けに解説しています。 原文はこちら：https://leanprover.github.io/theorem_proving_in_lean4/  初回：Theorem Proving in Lean4 を読む会#1 ― 第1章 https://www.docswell.com/s/imamuray/ZJWVME-2026-10-22-201931 前回：Theorem Proving in Lean4 を読む会#3 ― 第2章 2.4-第3章 3.2 https://www.docswell.com/s/imamuray/5Q2PLN-2026-11-01-101613 次回：11/13以降
published: November 07, 26
canonical: https://image.docswell.com/s/imamuray/Z3JVVP-2026-11-07-084758
---
# Page. 1

![Page Image](https://bcdn.docswell.com/page/YJ6MNWKL7V.jpg)

Theorem Proving in Lean 4
を読む会#4
3.3. Propositional Logic ～
2026/11/06 21:30~


# Page. 2

![Page Image](https://bcdn.docswell.com/page/GJ5Z5MPME4.jpg)

今日の流れ
21:15～21:30：開場
21:30～22:30：勉強会
●
Theorem Proving in Lean 4 の 3.3. Propositional Logic から
勉強会終了後は雑談などご自由に
●
自由に退席OK


# Page. 3

![Page Image](https://bcdn.docswell.com/page/9E2RN96RJR.jpg)

Theorem Proving in Lean 4 を読む


# Page. 4

![Page Image](https://bcdn.docswell.com/page/D7YDP4957M.jpg)

資料について
この資料の作成者もLean学習中です。
資料はChatGPTを使用して原文の翻訳や概要を作ってからスライドにまとめています。
学習中のため、誤った説明や用語の使い方があるかもしれませんが、その際はご指摘
いただければと思います。


# Page. 5

![Page Image](https://bcdn.docswell.com/page/VEN65YL4E8.jpg)

Leanの実行環境について
ブラウザで動作する Lean Playground が手軽です
●
おそらく、Theorem Proving in Lean 4 を読むだけならこれで完結できるはず
ローカルにセットアップしたい場合は公式へ
●
●
●
https://lean-lang.org/install/
○ 公式ではVSCodeの拡張経由で入れる方法推奨とのこと
VSCode拡張を経由しない場合：https://lean-lang.org/install/manual/
Dev Containerを使いたい場合は Mathlib を参考にするとよさそう
○ https://github.com/leanprover-community/mathlib4/tree/master/.devcontai
ner


# Page. 6

![Page Image](https://bcdn.docswell.com/page/Y79LYP44J3.jpg)

3. Propositions and Proofs


# Page. 7

![Page Image](https://bcdn.docswell.com/page/G78X6DQVED.jpg)

前回（第3回）の補足


# Page. 8

![Page Image](https://bcdn.docswell.com/page/L7L89MXRJR.jpg)

前回（第3回）の補足
def と theorem
set_option linter.unusedVariables false
--variable {p : Prop}
variable {q : Prop}
theorem t1 : p → q → p :=
fun hp : p =>
fun hq : q =>
hp
variable (α β : Type)
def t1Like : α → β → α :=
fun x : α =>
fun y : β =>
x
theorem は def の一種。
def とは違い、theorem の型(=命題)は
Prop のみ。
variable (α β : Type)
-- これは型がPropではないと怒られる
theorem t1' : α → β → α :=
fun ha => fun hb => ha


# Page. 9

![Page Image](https://bcdn.docswell.com/page/4EM6ZYLP7W.jpg)

前回（第3回）の補足
書いた証明が正しいかどうかの確認方法
エディタ上で型エラーが出ていなければ OK。
型が正しく構築できてる＝証明が正しく書けてる。


# Page. 10

![Page Image](https://bcdn.docswell.com/page/PERP69KY79.jpg)

前回（第3回）の補足
第3章、第4章での証明の書き方tips
tacticを使うと証明すべきゴールが示されるが、第5章までtacticを使わない のでどんな
型を目指せばいいのかわかりづらい。
_ (アンダースコア)を置くと示す型がわかるのでおすすめ（3.6節に説明あり）
カーソル位置で作るべき
型が示される


# Page. 11

![Page Image](https://bcdn.docswell.com/page/P7X3MQL4EX.jpg)

前回（第3回）の補足
含意（→）の証明
set_option linter.unusedVariables false
--variable {p q : Prop}
-- 含意の導入規則：ラムダ抽象
theorem t1 : p → q → p :=
fun hp : p =>
fun hq : q =>
show p from hp
-- 含意の除去規則：関数適用
theorem t2 (h₁ : p) (h₂ : p → q) : q :=
show q from h₂ h₁


# Page. 12

![Page Image](https://bcdn.docswell.com/page/37KYG9LPED.jpg)

3.1. Propositions as Types
3.2. Working with Propositions as Types
3.3. Propositional Logic
3.3.1. Conjunction
3.3.2. Disjunction
3.3.3. Negation and Falsity
3.3.4. Logical Equivalence
3.4. Introducing Auxiliary Subgoals
3.5. Classical Logic
3.6. Examples of Propositional Validities
3.7. Exercises


# Page. 13

![Page Image](https://bcdn.docswell.com/page/LJ39NW34J5.jpg)

3.3. Propositional Logic
概要
命題論理の含意以外の論理結合子（¬,∧,∨,↔）の使い方を説明している節。
結合子の優先順位は¬,∧,∨,↔の順。
含意（→）を含め、二項論理結合子は右結合。
命題論理の結合子は、Leanのライブラリで定義されており、自動的にインポート
される。それぞれの演算子には、標準的な導入規則 と除去規則 が用意されてる。
●
●
●
●
3.3.1. Conjunction：∧
3.3.2. Disjunction：∨
3.3.3. Negation and Falsity：¬
3.3.4. Logical Equivalence：↔


# Page. 14

![Page Image](https://bcdn.docswell.com/page/8JDGWK45JG.jpg)

3.3. Propositional Logic
3.3.1. Conjunction
●
●
●
●
●
And.intro：p と q の証明から、p ∧ q の証明を作る。
And.left / And.right：p ∧ q の証明から、それぞれ p / q の証明を取り出
す。
⟨hp, hq⟩：And.intro hp hq の省略記法。
h.left / h.right：And.left h / And.right h の省略記法。
∧ と × の類似と違い ：カリー＝ハワード同型対応の一例だが、含意と関数型の場
合とは異なり、Leanでは ∧ と × は別々のものとして扱われる。


# Page. 15

![Page Image](https://bcdn.docswell.com/page/VEP39KMD78.jpg)

3.3. Propositional Logic
3.3.2. Disjunction
●
●
●
●
●
Or.intro_left / Or.intro_right：それぞれ p,q の証明から p∨q の証明を作る。
○ Or.intro_left q hp のように、もう一方の命題も引数として指定する。
Or.elim：p ∨ q の証明と、p → r、q → r の証明から r を導く。
○ p の場合と q の場合の両方で r が導ければよい、という場合分けの証明を表す。
Or.inl / Or.inr：Or.intro_left / Or.intro_right の省略形。
○ 例えば Or.inl hp は Or.intro_left _ hp に相当する。Leanが文脈から引数の
型を推論できるため、簡潔に記述できる。
型注釈の省略：Leanは式全体の型から、関数の引数の型も推論できる。次の2つは同じ型の証
明を表す。注釈を付けると読みやすさや、エラーの発見・調査に役立つ場合がある。
○ example (p q : Prop) : p → p ∨ q := fun hp : p => Or.inl hp
○ example (p q : Prop) : p → p ∨ q := fun hp => Or.inl hp
h.elim による省略記法 ：Or.elim h … は h.elim ... とも書ける。


# Page. 16

![Page Image](https://bcdn.docswell.com/page/27V4MV9GEQ.jpg)

3.3. Propositional Logic
3.3.3. Negation and Falsity
●
●
●
●
●
¬p（否定） ：p → False と定義される。p を仮定して矛盾を導くことで、¬p を証明
できる。
否定の利用 ：hp : p と hnp : ¬p から、hnp hp : False が得られる。
False.elim：False の証明から任意の命題を導ける（ex falso）。
absurd：absurd hp hnp は、hp : p と hnp : ¬p の矛盾から任意の命題を
導く。
True と False：True は True.intro で証明できる。一方、False には導入
規則がなく、矛盾から他の命題を導くために使われる。


# Page. 17

![Page Image](https://bcdn.docswell.com/page/5JG1GL4D7L.jpg)

3.3. Propositional Logic
3.3.4. Logical Equivalence
●
●
●
●
●
p ↔ q（論理的同値） ：p → q と q → p の両方が成り立つことを表す。
Iff.intro：h1 : p → q と h2 : q → p から p ↔ q の証明を作る。
Iff.mp / Iff.mpr：h : p ↔ q から、それぞれ p → q / q → p の証明を取り
出す。
匿名コンストラクタ記法 ：Iff.intro h1 h2 は ⟨h1, h2⟩ と書ける。また、And
と同様に ⟨h.left, h.right⟩ などの記法を使って証明を簡潔に書ける。
ドット記法 ：Iff.mp h と Iff.mpr h は、それぞれ h.mp と h.mpr と書ける。
例えば、(and_swap p q).mp h のように、同値の証明から必要な方向の含意
を利用できる。


# Page. 18

![Page Image](https://bcdn.docswell.com/page/47QDXYGXEP.jpg)

3.1. Propositions as Types
3.2. Working with Propositions as Types
3.3. Propositional Logic
3.4. Introducing Auxiliary Subgoals
3.5. Classical Logic
3.6. Examples of Propositional Validities
3.7. Exercises


# Page. 19

![Page Image](https://bcdn.docswell.com/page/KE4Z6W52J1.jpg)

3.4. Introducing Auxiliary Subgoals
3.4 まとめ
●
●
●
●
have：証明の途中で補助的な命題を導入し、その証明を後続の推論で利用でき
る。
中間結果の利用 ：have hp : p := ... のように中間結果に名前を付けること
で、長い証明を小さな段階に分けて書ける。
suffices：「〜を示せば十分」として、元の目標を証明するために必要な中間命
題を設定できる。
証明の順序を整理する ：have と suffices を使うことで、先に中間命題を証明
したり、目標から逆向きに考えたりして、証明を構造化できる。


# Page. 20

![Page Image](https://bcdn.docswell.com/page/L71RVYWK7G.jpg)

3.1. Propositions as Types
3.2. Working with Propositions as Types
3.3. Propositional Logic
3.4. Introducing Auxiliary Subgoals
3.5. Classical Logic
3.6. Examples of Propositional Validities
3.7. Exercises


# Page. 21

![Page Image](https://bcdn.docswell.com/page/G7W1LG6PJ2.jpg)

3.5. Classical Logic
用語整理：命題論理、直観主義論理、古典論理
用語
分類
説明
命題論理 （propositional logic）
論理学の分野
命題と論理結合子を用いて、命題間の
論理的関係や推論を扱う。
直観主義論理 （intuitionistic logic）ま
たは、
構成的論理 （constructive logic）
論理体系
排中律を一般には認めず、構成的な証
明を重視する。
古典論理 （classical logic）
論理体系
排中律や二重否定除去などの古典的な
推論原理を認める
直感主義論理と古典論理が分かれていることで、 証明に求める性質を区別できる 。
●
●
直観主義論理 ：証明の構成を重視し、結論を成立させる具体的な情報を得やすい
古典論理 ：広く使われている数学的推論を利用しやすい


# Page. 22

![Page Image](https://bcdn.docswell.com/page/4JZPMLY673.jpg)

3.5. Classical Logic
古典論理と直観主義論理
●
●
●
●
Leanの基本的な論理規則は、直観主義論理の考え方に基づいている。
古典論理では、排中律 を認める。
○ p ∨ ¬p：任意の命題 (p) は、真または偽のどちらかである。
○ Leanでは Classical.em p で利用できる。
直観主義論理の p ∨ q は、どちらが成立するかを示す証明を要求する。
○ 古典論理では、どちらの証明も持っていなくても p ∨ ¬p を認める。
排中律から 二重否定除去 が導ける。
○ ¬¬p → p
○ これにより、矛盾を導く背理法が一般に利用できる。


# Page. 23

![Page Image](https://bcdn.docswell.com/page/YE6MNWDLJV.jpg)

3.5. Classical Logic
Leanで古典論理を使う
●
●
●
●
open Classical で古典論理の原理を利用できる。
主な証明方法：
○ Classical.em p：排中律による場合分け
○ byCases：命題が成立する場合と否定が成立する場合に分ける
○ byContradiction：結論の否定を仮定して矛盾を導く
直観主義論理では証明できず、古典論理が必要とする命題の例：
¬(p ∧ q) → ¬p ∨ ¬q
¬(p ∧ q) からは、pとqが同時に成立しないことは分かるが、どちらが成立しないかまでは
分からない。排中律を使えば証明できる。
古典論理の原理が必要な場面を理解し、必要な箇所で利用することが重要。


# Page. 24

![Page Image](https://bcdn.docswell.com/page/GE5Z5M3M74.jpg)

3.1. Propositions as Types
3.2. Working with Propositions as Types
3.3. Propositional Logic
3.4. Introducing Auxiliary Subgoals
3.5. Classical Logic
3.6. Examples of Propositional Validities
3.7. Exercises


# Page. 25

![Page Image](https://bcdn.docswell.com/page/972RN9ZRER.jpg)

3.6. Examples of Propositional Validities
●
●
●
Leanの標準ライブラリには、命題論理の基本的な恒等式が用意されており、証明
で利用できる。
○ 交換律、結合律、分配律など
sorry：証明の未完成部分を一時的に埋める。Leanの型チェックを先に進められ
るが、証明の正しさは保証されない。
_：Leanにその部分の項を推論させる。推論できなければ、必要な型やコンテキス
トを含むエラーが出るため、未解決のゴールを確認できる 。


# Page. 26

![Page Image](https://bcdn.docswell.com/page/DJYDP4R5JM.jpg)

3.1. Propositions as Types
3.2. Working with Propositions as Types
3.3. Propositional Logic
3.4. Introducing Auxiliary Subgoals
3.5. Classical Logic
3.6. Examples of Propositional Validities
3.7. Exercises


# Page. 27

![Page Image](https://bcdn.docswell.com/page/V7N65YD478.jpg)

3.7. Exercises
練習問題
勉強会では、
-- commutativity of ∧ and ∨
example : p ∧ q ↔ q ∧ p := sorry -- 本文 3.3.4 のサンプルコードに解答あり
example : p ∨ q ↔ q ∨ p := sorry -- 本文 3.3.2 のサンプルコードとほぼ同じ
の2つを実際に解きながら解説しました。


# Page. 28

![Page Image](https://bcdn.docswell.com/page/YJ9LYPG4E3.jpg)

次回
11/13(金) 21:30~22:30
基本的に、毎週金曜 21:30~22:30 に実施
次回は4章から。