前期授業第7回（6/2）

第7回は、これまで一つずつ習ってきた推論規則がすべて出揃う節目の回でした。∧（かつ）・∨（または）・→（ならば）の導入規則と除去規則を一覧で眺め、そこから証明の「質」を問う議論へと踏み込みました。今回のメインテーマは''detour（遠回り）''と''正規な証明（normal proof）''の概念、そして証明を構成する実践的な方法としての''逆算法''です。

授業内容の目次：

• 前回おさらいと ∨E の入れ子（A ∨ (B ∨ C) → (A ∨ B) ∨ C）
• 最小命題論理の全推論規則一覧（7規則）
• 証明樹の構造と proof net との対応
• detour（遠回り）の3パターン
• 正規な証明と正規化定理
• V字型構造・部分論理式原理
• 逆算法と具体例（A ∧ (A → B) → B）
• 演習問題5題

speakerdeck.com
最小命題論理の推論規則一覧が完成したことで、証明の「形式」ではなく「内容の豊かさ」を問えるようになります。detour は証明の本質に貢献しない「無駄な回り道」であり、それを排除した正規な証明には美しい構造的性質（V字型・部分論理式原理）が現れます。逆算法はその性質を直接利用した証明構成の戦略で、「結論の形から最後のステップが決まる」という単純なルールに従って証明木を組み上げていきます。

今回は証明論的意味論（第12〜14回）へ向かう理論的基盤の構築にあたります。「正規な証明が必ず存在する」という正規化定理は、次回（第8回）でその証明を扱います。

授業日時

6月2日（火）16：45〜18：15
文学部第4講義室

授業内容

• 前回おさらい：∧・∨の推論規則と proof net の対応を再確認
• ∨E の入れ子：A ∨ (B ∨ C) → (A ∨ B) ∨ C——外側と内側で2セットのキャンセルラベルが必要
• 最小命題論理の全推論規則一覧（→I、→E、∧I、∧E_L、∧E_R、∨I_L、∨I_R、∨E）
• 証明樹の3要素（葉・ノード・根）と仮定の2種類（開いた仮定・閉じた仮定）
• 証明樹と proof net の対応（Y字ノード・T字ノード・3入力収束ノード）
• detour（遠回り）の3パターン（→・∧・∨）
• 正規な証明の定義と正規化定理の主張
• V字型構造（上半分：除去フェーズ／下半分：導入フェーズ）
• 部分論理式原理（subformula property）
• 逆算法の手順と例題：A ∧ (A → B) → B
• 演習問題：問1〜4・チャレンジ

https://speakerdeck.com/player/PRESENTATION_ID

解説

前回おさらいと ∨E の入れ子**

授業は前回のおさらいから始まりました。∧・∨の推論規則を確認した後、∨E の入れ子の例——A ∨ (B ∨ C) から (A ∨ B) ∨ C を証明する——を丁寧に取り上げました。この証明は外側の ∨E の内部にもう一度 ∨E が現れる構造で、「場合分けの中でまた場合分けをする」という初学者が必ず戸惑う場面です。

外側の ∨E でキャンセルラベルを u と v に振り（仮定 [u: A] と [v: B ∨ C] を消費）、内側の ∨E でラベルを p と q に振る（仮定 [p: B] と [q: C] を消費）——2セットのラベルを区別して管理することが肝心です。proof net で書けば、外側の3入力収束ノードの内部に別の3入力収束ノードが入れ子になった構造で表現されます。

最小命題論理の全推論規則**

ここで今期学んだ全推論規則が出揃いました。

1. ''→I''（ならばの導入）：仮定 [u: A] のもとで B を導いたとき、A → B を結論できる。仮定 u が閉じる（cancelled）。
2. ''→E''（ならばの除去、モーダスポーネンス）：A と A → B から B を導く。
3. ''∧I''（かつの導入）：A と B から A ∧ B を導く。
4. ''∧E_L'' / ''∧E_R''（かつの除去）：A ∧ B から A、またはA ∧ B から B を導く。
5. ''∨I_L'' / ''∨I_R''（またはの導入）：A から A ∨ B、または B から A ∨ B を導く。
6. ''∨E''（またはの除去、場合分け）：A ∨ B があり、[u: A] からC・[v: B] からCを導いたとき、Cを結論できる。仮定 u と v が閉じる。

否定（¬A）は A → ⊥ の略記として既に導入済みです。

証明樹の構造と proof net との対応**

証明樹は''葉''（最上部に置かれた仮定や公理）・''ノード''（各推論規則の適用）・''根''（証明された結論）の3要素からなります。

仮定には2種類あります。''開いた仮定（open assumption）''はまだキャンセルされていない仮定で、証明が依存している前提を表します。''閉じた仮定（cancelled assumption）''は →I や ∨E によってキャンセルされた仮定で、証明の内部で消費されました。閉じた仮定には角括弧を付けて [u: A] のように表記します。

proof net との対応：同じラベルの仮定が複数の葉に現れる場合に''Y字ノード''（縮約ノード）が生じます。∧I は2本のワイヤが合流する''T字ノード''に、∨E は3本入力の''収束ノード''（場合分けノード）に対応します。

detour（遠回り）とは**

証明を書いていると、ある結合子を「導入した直後に同じ結合子で除去する」という無駄な手順が生じることがあります。これを''detour''（遠回り）と呼びます。3パターンあります：

1. ''→ の detour''：A と仮定 [u: A] から A を経由して A → B を →I で作り、その直後に →E で除去する。
2. ''∧ の detour''：A と B から A ∧ B を ∧I で作り、直後に ∧E_L または ∧E_R で片方を取り出す。
3. ''∨ の detour''：A から A ∨ B を ∨I_L で作り、直後に ∨E で場合分けして消費する。

いずれも証明の本質的な内容に貢献していません。proof net で見ると、導入ノードと除去ノードが直接接続されており、間にある2つのノードを取り除いてワイヤを直結するだけで detour を除去できます。

正規な証明と正規化定理**

detour を含まない証明を''正規な証明（normal proof）''といいます。

そして自然演繹の中心的な定理がここに登場します：

''定理（正規化定理）：最小命題論理の任意の証明は、正規な証明に変換できる。''

つまり、どんなに遠回りだらけの証明でも、同じ前提・同じ結論のきれいな証明が必ず存在します。変換の具体的な手順（detour elimination のアルゴリズムとその停止性）は次回（第8回）で扱います。今回は定理の主張を理解し、「なぜ重要か」を直感するところまで。

V字型構造と部分論理式原理**

正規な証明には2つの重要な構造的性質があります。

''（1）V字型構造''：正規な証明の上半分では除去規則のみが使われ、下半分では導入規則のみが使われます。仮定を解体して「原子的な部品」まで分解し（除去フェーズ）、それを組み立てて結論に到達する（導入フェーズ）——この V の字が正規な証明の骨格です。上半分と下半分の境界を「転換点（minimum point）」と呼びます。

''（2）部分論理式原理（subformula property）''：正規な証明に現れるすべての式は、結論または開いた仮定の''部分論理式''（subformula）です。部分論理式とは、ある式を構成する部分として取り出せる式のことです。たとえば A ∧ (A → B) の部分論理式は A ∧ (A → B)・A・A → B・B の4つです。

部分論理式原理は「証明の中から天下り的に複雑な式が出てくることはない」ことを意味します。正規化定理 ＋ 部分論理式原理が合わさって、「必要なことだけを使った証明が必ず存在する」ことが保証されます。これが証明論的意味論（ハーモニー・保守的拡張）の議論への入口となります。

逆算法**

V字型構造を踏まえると、証明を''逆算''で構成する戦略が機能します。

1. ''Step 1''：証明したい命題の''最外部の結合子''を見る。
2. ''Step 2''：その結合子の導入規則から、直前のサブゴールを確定する。
3. ''Step 3''：サブゴールが仮定や前提から除去規則で取り出せるなら取り出す。
4. ''Step 4''：サブゴールが残れば繰り返す。

正規な証明では「最後に使われる規則は最外部の結合子から（ほぼ）一意に決まる」ため、この逆算が機能します。遠回りがあると逆算が機能しないため、正規化定理が逆算法の裏付けになっています。

具体例として A ∧ (A → B) → B を証明しました。

1. 最外結合子は →。最後は →I。仮定 [u: A ∧ (A → B)] を追加。サブゴール：B を導く。
2. B を導くには A → B が必要。[u] から ∧E_R で A → B を取り出せる。→E を使うには A も必要。
3. A は [u] から ∧E_L で取り出せる。[u] を2箇所で使う（proof net では Y字ノード）。
4. 証明木が完成。

演習問題（2022年度資料より）**

今回は ∧・∨・→ の3つを組み合わせた問題5題でした。

1. 問1：A ∧ B → (B → C) → C ——∧E と →E の組み合わせ。逆算法で一気に解ける。
2. 問2：(A → C) ∧ (B → C) → (A ∨ B → C) ——∧E で両方の矢印を取り出してから ∨E で場合分け。
3. 問3：(A → C) ∨ (B → C) → (A ∧ B → C) ——∨E を使う。問2と似て非なる構造。
4. 問4（思考問題）：A ∨ B → A ∧ B ——''証明できません。'' 逆算法で行き詰まる箇所を確認しよう。
5. 問5（チャレンジ）：(A ∧ B) ∨ C → (A ∨ C) ∧ (B ∨ C) ——分配則。∨E と ∧I の組み合わせ。

問2と問3は鏡像関係にあります。問2は「かつ」で''両方''の矢印を持ち込んでいるので ∨E の各ケースで使う矢印が確定していますが、問3は「または」で''どちらか一方''しか保証されていない——それぞれのケースで ∧E を使って A と B 両方を取り出し、あとは一方の矢印に渡すだけ。証明木の形が見た目以上に違います。

今回のキーワード

detour（遠回り）、正規な証明（normal proof）、正規化定理（normalization theorem）、V字型構造、部分論理式原理（subformula property）、逆算法、proof net、∧I、∧E、∨I、∨E、→I、→E、開いた仮定、閉じた仮定、最小命題論理

宿題

本日の演習問題のうち、授業中に解けなかったものを提出してください。

• 問1：A ∧ B → (B → C) → C
• 問2：(A → C) ∧ (B → C) → (A ∨ B → C)
• 問3：(A → C) ∨ (B → C) → (A ∧ B → C)
• 問4（思考問題）：A ∨ B → A ∧ B ——なぜ証明できないか、逆算法で確認してみよう
• 問5（チャレンジ）：(A ∧ B) ∨ C → (A ∨ C) ∧ (B ∨ C)

全問解けた場合は「全問解けた」と記入して提出すること。宿題にかかった時間を必ず記入すること。提出方法・期限はKULMSの指示に従ってください。

• • • -

[2026前期火５] 科学哲学科学史（演習） 担当：矢田部俊介（西日本旅客鉄道株式会社）

前期授業第6回（5/26）

授業第6回目の今回は、前回まで扱ってきた「ならば」（→）に続いて、「かつ」（∧）と「または」（∨）の推論規則を導入しました。前回から本格的に入った proof net も引き続き扱い、証明木の中で見えにくい「命題の流れ」を、ワイヤとノードとして可視化していきます。

今回のポイントは、∧ と ∨ が互いに鏡像のような関係にあることです。∧ は、二つの証明を一つにまとめる結合子です。A と B が両方証明できれば A ∧ B が証明でき、A ∧ B からは A だけ、あるいは B だけを取り出せます。これに対して ∨ は、A か B のどちらか一方から A ∨ B を作ることができますが、A ∨ B を使うときには「A の場合」と「B の場合」の両方を調べる必要があります。

授業日時

5月26日（火）16：45〜18：15
文学部第4講義室

授業内容

• 前回のおさらい：→ の推論規則と proof net
• ヴァイオリンの一弦ずつの練習としての論理結合子
• ∧（かつ）の導入規則・除去規則
• ∧ の proof net：合流と取り出し
• ∧ と → を組み合わせた証明
• ∨（または）の導入規則・除去規則
• ∨E と場合分け証明
• ∧ と ∨ の双対性
• きれいな証明と detour
• proof net による ∧・∨ の比較
• 演習問題

speakerdeck.com

解説

今回の授業では、前回までに導入した「ならば」（→）の推論規則と proof net を土台にして、「かつ」（∧）と「または」（∨）の規則を学びました。
前回までの中心は → でした。→ の導入規則は、A を仮定して B が証明できたとき、その仮定 A をキャンセルして A → B を作る規則です。これに対して → の除去規則は、A と A → B から B を取り出す規則です。つまり、→ は「A から B が導ける」という推論関係を、対象言語の中で A → B という命題として明示化するための記号でした。
proof net では、命題はワイヤ、推論規則はノードとして表されます。キャンセルされた仮定は点線ワイヤ、使われなかった仮定は宙ぶらりんワイヤ、同じ仮定を複数回使う縮約は Y 字ノードとして可視化されます。前回はこの道具を使って、弱化や縮約が証明の中でどのように現れるのかを見ました。

今回は、この道具立てを ∧ と ∨ に拡張します。授業では、論理結合子を一つずつ学ぶことを、ヴァイオリンの弦を一本ずつ練習することにたとえました。最初から全部を自由に弾こうとするのではなく、まず →、次に否定、さらに ∧、そして ∨ というように、結合子ごとの導入規則と除去規則を一つずつ身体化していきます。論理学は眺めるだけの科目ではなく、実際に手を動かして証明を書いていく演習科目です。

まず導入したのは、∧、つまり「かつ」の推論規則です。
∧ の導入規則は非常に直観的です。A が証明でき、B も証明できるなら、A ∧ B が証明できます。これは、二本のワイヤが一つのノードで合流し、A ∧ B という一本のワイヤとして出てくるイメージです。A と B を両方持っているから、それらをまとめて A ∧ B と言ってよい、ということです。
これに対して、∧ の除去規則は二つあります。A ∧ B から A を取り出す左除去と、A ∧ B から B を取り出す右除去です。A ∧ B があるなら、その左成分である A を使ってよいし、右成分である B を使ってもよい。したがって、∧ の導入規則は構成子、∧ の除去規則は解体子に対応します。
→ と比較すると、∧ の特徴が見えてきます。→ の導入規則では、仮定のキャンセルが必要でした。A を仮定して B を導き、その仮定をキャンセルして A → B を作るからです。これに対して ∧ の導入規則では、仮定のキャンセルはありません。ただ A と B が両方あれば、それらを合わせて A ∧ B を作るだけです。一方、∧ の除去規則は左除去と右除去の二種類があります。A ∧ B からどちらを取り出すかによって、二つの除去規則が必要になるのです。
proof net で見ると、∧ の性格はさらにわかりやすくなります。∧I は二本のワイヤが合流して一本になるノードです。A と B のワイヤが集まり、A ∧ B というワイヤが出力されます。これに対して ∧EL と ∧ER は、一本の入力ワイヤから一本の出力ワイヤを取り出すノードです。A ∧ B から A を取り出すときには B の情報は捨てられ、A ∧ B から B を取り出すときには A の情報が捨てられます。
ここで重要なのが detour、つまり遠回りです。たとえば、A と B から A ∧ B を作り、その直後に ∧EL で A だけを取り出す証明があったとします。これは「A ∧ B を作ってすぐ A だけ取り出す」という無駄な回り道です。最初から A を使えばよかったはずです。proof net では、このような detour は、∧I ノードと ∧E ノードを消して、ワイヤを直結するだけで除去できます。
次に、∧ の証明例として A ∧ B → B ∧ A、つまり ∧ の交換則を扱いました。A ∧ B を仮定すると、∧ER によって B を取り出せます。また、同じ A ∧ B から ∧EL によって A を取り出せます。そこで、取り出した B と A を ∧I でまとめれば B ∧ A が得られます。最後に、最初の仮定 A ∧ B をキャンセルして A ∧ B → B ∧ A が証明されます。
この証明で重要なのは、同じ仮定 A ∧ B を二回使うことです。一回目は B を取り出すために使い、二回目は A を取り出すために使います。したがって、この証明には縮約則が含まれます。proof net では、A ∧ B のワイヤが Y 字に分岐し、一方が ∧ER へ、もう一方が ∧EL へ向かいます。つまり、∧ の交換則では、ワイヤが分岐して左右の成分を取り出し、それらを入れ替えて再び ∧I で合流させる構造が現れます。
演習では、A ∧ B → A、A ∧ B → B ∧ A、A → B → A ∧ B、そしてチャレンジ問題として (A ∧ B) ∧ C → A ∧ (B ∧ C) を扱いました。特に A → B → A ∧ B は、→ と ∧ の組み合わせの基本例です。まず A を仮定し、次に B を仮定します。その二つから ∧I で A ∧ B を構成し、B の仮定、A の仮定を順にキャンセルします。proof net では、A と B の二本の点線ワイヤが ∧I で合流し、A ∧ B になる様子が見えます。

次に導入したのが、∨、つまり「または」の推論規則です。
∨ の導入規則は二つあります。A が証明できれば A ∨ B が証明できます。これが左導入です。また、B が証明できれば A ∨ B が証明できます。これが右導入です。つまり、A ∨ B を作るには、A と B の両方を持っている必要はありません。どちらか一方があれば十分です。
ここで ∧ との対比が重要になります。∧ は、導入規則が一つで、除去規則が二つでした。A と B の両方から A ∧ B を作り、A ∧ B から A または B を取り出します。これに対して ∨ は、導入規則が二つで、除去規則が一つです。A から A ∨ B を作ることもできるし、B から A ∨ B を作ることもできます。しかし A ∨ B を使うときには、単純に A か B のどちらかを取り出すことはできません。
∨ の除去規則は、場合分け証明の形式化です。A ∨ B があるとします。このとき、A の場合に C が証明でき、B の場合にも C が証明できるなら、結局どちらの場合でも C が成り立つので、C を結論できます。形式的には、A ∨ B、A を仮定して C を導く枝、B を仮定して C を導く枝、この三つが揃ったときに C を結論します。
この ∨E では、仮定のキャンセルが除去側で起こります。→I では、A を仮定して B を導き、その仮定をキャンセルして A → B を作りました。つまり、キャンセルは導入側で起こっていました。これに対して ∨E では、A の場合の仮定と B の場合の仮定を、それぞれ場合分けの枝の中で使い、最後に ∨E によってまとめてキャンセルします。∨ の解体は、二つの枝が揃って初めて完成します。
proof net で見ると、∨I は一本の入力ワイヤから一本の出力ワイヤを作るノードです。A から A ∨ B を作る、あるいは B から A ∨ B を作るだけなので、形としては ∧E と似ています。これに対して ∨E は、A ∨ B のワイヤと、A から C へ行く枝、B から C へ行く枝の三つが合流して C になるノードです。つまり、∨E は場合分けの合流点です。
この構造から、∧ と ∨ の双対性が見えてきます。∧I は二本のワイヤが合流する導入規則です。一方、∨E は三本の入力を持つ合流型の除去規則です。∧E は一本のワイヤから一本のワイヤを取り出す除去規則です。一方、∨I は一本のワイヤから一本のワイヤを作る導入規則です。つまり、∧ と ∨ は、導入と除去の形が鏡像的に入れ替わっているのです。
∨ の証明例として、A ∨ B → B ∨ A、つまり ∨ の交換則を扱いました。A ∨ B を仮定します。そこからは、A の場合と B の場合に分けます。A の場合には、A から右導入によって B ∨ A を作ることができます。B の場合には、B から左導入によって B ∨ A を作ることができます。どちらの場合にも B ∨ A が得られるので、∨E によって B ∨ A を結論できます。最後に、最初の仮定 A ∨ B をキャンセルして A ∨ B → B ∨ A が証明されます。
proof net では、この証明は二つの枝が ∨E で合流する形になります。∧ の交換則では、A ∧ B のワイヤが Y 字で分岐し、B と A を取り出して入れ替え、∧I で再合流しました。これに対して ∨ の交換則では、A の場合と B の場合の二つの枝をそれぞれ B ∨ A に変換し、最後に ∨E で合流させます。∧ では分岐して入れ替える。∨ では場合分けして合流する。この違いが、proof net によって視覚的に見えるようになります。
演習では、A → A ∨ B、A ∨ A → A、A ∨ B → B ∨ A、そしてチャレンジ問題として (A ∨ B) ∨ C → A ∨ (B ∨ C) を扱いました。A → A ∨ B は、∨I のもっとも基本的な練習です。A を仮定すれば、∨IL によって A ∨ B を作ることができます。B は実際には使いません。これは「B が証明された」という意味ではなく、「A が成り立つなら A または B は成り立つ」という意味です。
A ∨ A → A は、∨E の最もシンプルな例です。A ∨ A を仮定し、左の場合も A、右の場合も A として場合分けします。どちらの枝でも結論 A は仮定そのものなので、∨E によって A が得られます。この証明では、場合分けの両枝が同じ形になります。∨E の構造を確認するにはちょうどよい例です。

その後、「きれいな証明」と detour について整理しました。detour とは、ある結合子を導入した直後に、同じ結合子を除去するような無駄な遠回りです。たとえば、A と B から A ∧ B を作り、その直後に A だけを取り出すなら、最初から A を使えばよかったはずです。このような遠回りを消す操作が正規化です。

正規化によって得られる証明を正規形と呼びます。正規形の証明には、いくつかの重要な性質があります。第一に、部分論理式原理を満たします。つまり、証明中に現れる命題は、基本的には結論や仮定の部分命題に限られます。第二に、証明の構造が V 字型になります。前半では除去規則によって仮定を分析し、後半では導入規則によって結論を総合する。このように、きれいな証明は、分析から総合へと一方向に進む構造を持ちます。

この話は、後の授業で扱う大域的ハーモニーにつながります。局所的には、それぞれの結合子について導入規則と除去規則が釣り合っている必要があります。しかし、それだけでは足りません。体系全体として、どんな証明も detour を消して正規形へ変換できる必要があります。この正規化可能性こそが、大域的ハーモニーの核心です。

授業では、LLM との接続にも触れました。LLM の chain of thought は、もっともらしい推論の列を出力します。しかし、それが論理学でいう意味での正規形を保証しているわけではありません。証明論の観点から見ると、重要なのは、推論過程が単に長く書かれていることではなく、detour がなく、導入と除去がハーモニーを保ち、正規化可能な形になっているかどうかです。この問題は、第14回で改めて扱う予定です。

最後に、∧ と ∨ の proof net を読み比べました。A ∧ B → B ∧ A の proof net では、A ∧ B の仮定が Y 字で分岐し、∧ER で B、∧EL で A を取り出し、それらを入れ替えて ∧I で B ∧ A を作ります。ここでは、同じ仮定を二回使うため、縮約則が見えています。

一方、A ∨ B → B ∨ A の proof net では、A の場合と B の場合の二つの枝が作られます。A の枝では ∨IR によって B ∨ A を作り、B の枝では ∨IL によって B ∨ A を作ります。そして、A ∨ B の仮定と二つの枝が ∨E で合流します。ここでは、場合分けの構造が proof net の形として現れます。

今回の授業全体を通じて確認したのは、論理結合子はそれぞれ固有の「動き方」を持っているということです。→ は仮定をキャンセルして推論関係を命題化する記号です。∧ は二つの証明を合流させ、必要に応じて左右の成分を取り出す記号です。∨ は一方から全体を作り、使うときには場合分けを要求する記号です。

そして、それぞれの動きは、導入規則と除去規則として定義されます。証明論的意味論の立場では、論理結合子の意味とは、まさにこの導入規則と除去規則のペアによって与えられます。さらに proof net を使うと、その規則が実際の証明の中でどのように働いているかを、ワイヤとノードとして見ることができます。
論理学は、記号の意味を暗記する科目ではありません。実際に証明を書き、規則を適用し、ワイヤの流れを追い、どこに Y 字があり、どこに場合分けがあり、どこに detour があるのかを確認する演習科目です。今回の ∧ と ∨ の導入により、命題論理の主要な結合子の姿がかなり見えてきました。

次回は、命題論理のきれいな証明と正規化をさらに詳しく扱います。導入規則と除去規則を一つずつ練習したあと、それらが体系全体としてどのようにまとまり、どのように detour を消していけるのかを見ていきます。

今回のキーワード

自然演繹、証明木、proof net、証明ネット、ワイヤ、ノード、キャンセル仮定、点線ワイヤ、弱化、宙ぶらりんワイヤ、縮約、Y字ノード、ならば、→、かつ、∧、∧導入、∧除去、左除去、右除去、または、∨、∨導入、∨除去、場合分け、双対性、交換則、結合則、配分則、detour、遠回り、正規化、正規形、部分論理式原理、V字型構造、大域的ハーモニー

宿題

スライド内の演習問題に取り組んでください。

A, B, C は任意の命題です。証明木を書き、できれば proof net も描いてください。

• 問1　A ∧ B → A
• 問2　A → A ∨ B
• 問3　A ∧ B → B ∧ A
• 問4　A ∨ B → B ∨ A
• 問5　A → B → A ∧ B
• 問6（チャレンジ） A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C)

問3では ∧ の交換則として Y 字ノードを意識してください。問4では ∨ の交換則として、∨E による場合分けを意識してください。問6は配分則であり、A と B ∨ C を仮定したあと、B の場合と C の場合に分ける必要があります。

提出方法・期限は KULMS の指示に従ってください。

前期授業第5回（5/19）

授業第5回目の今回は、前回導入した「ならば」（→）の導入規則・除去規則を使って、実際に証明を書く練習を行いました。あわせて、証明木を proof net として読み直す方法をもう一度整理し、仮定が使われる・使われない・複数回使われるという違いを、ワイヤの形として可視化しました。

また、前回の補足として、論理式の括弧の省略規則と、否定 ¬A を A → ⊥ として定義する方法を導入しました。授業の最後には、新しい論理結合子として「かつ」（∧）の導入規則と除去規則に入りました。これにより、論理結合子を一つずつ「弦」として練習していく段階に入りました。

授業日時

5月19日（火）16：45〜18：15
文学部第4講義室

授業内容

• 論理式の略記規則と否定の定義
• 前回の宿題解答
• 「ならば」（→）の問題演習
• proof net の見方と描き方
• 縮約則・弱化則の可視化
• 証明木の構造：葉・幹・根、主枝と従属演繹
• 分析的部分と総合部分
• ∧（かつ）の導入規則と除去規則
• 宿題

speakerdeck.com

解説

今回の授業では、前回導入した「ならば」（→）の推論規則を実際に使いながら、証明を書く練習を行いました。前回確認したように、→ の導入規則は、A を仮定して B が証明できたときに、その仮定 A をキャンセルして A → B を得る規則です。これに対して、→ の除去規則は、A と A → B から B を取り出す規則です。いわゆる modus ponens、前件肯定です。

この二つの規則は、導入と除去、構成と解体の対になっています。→導入規則は「A から B が導ける」という推論の事実を A → B という命題として構成する規則であり、→除去規則は A → B という命題に A を適用して B を取り出す規則です。つまり、→ の意味は、真理値表によってではなく、この導入規則と除去規則の釣り合いによって与えられます。

授業の最初では、前回の補足として、論理式の括弧に関する表記規約を整理しました。学生からの指摘を受けて、原子命題に勝手に括弧を付けたもの、たとえば (Z = S(Z)) のような形をどう扱うかを確認しました。厳密には、帰納的定義に書かれていないものは WFF、つまり整式ではありません。これはコンパイラエラーのようなものです。定義にない形は、意味を考える以前に、そもそも形式言語の文として構成されていないということです。

ただし、実際にすべての括弧を厳密に書くと、式が非常に読みにくくなります。そこで、今後の授業では略記規則を採用します。第一に、→ は右結合とします。したがって、A → B → C は A → (B → C) の略記です。A → B → C → D なら、A → (B → (C → D)) と読みます。一方、(A → B) → C は括弧を外すと意味が変わるので、省略できません。

第二に、結合子の優先順位を決めます。強い順に、¬、∧、∨、→ とします。つまり、否定がもっとも強く、次に「かつ」、次に「または」、最後に「ならば」がもっとも弱い結合子です。たとえば A → B → A ∧ B は、A → (B → (A ∧ B)) と読みます。∧ は → よりも強く結合するため、A ∧ B が先に一つのまとまりになるからです。

次に、否定 ¬A の定義を導入しました。この授業では、否定を独立した基本記号として扱うのではなく、A → ⊥ の略記として扱います。ここで ⊥ は「ボトム」と呼ばれる特殊な命題記号です。¬A とは、「A を仮定すると矛盾する」、つまり A から ⊥ が導ける、ということを表します。したがって、

¬A := A → ⊥

と定義します。同様に、¬¬A は (A → ⊥) → ⊥ です。今回の段階では、⊥ に対する特別な推論規則はまだ導入しません。したがって、¬A が出てきたら A → ⊥ に展開して考えるだけで十分です。

その後、前回の宿題解答を確認しました。第一の問題は、(A → A → B) → (A → B) の証明でした。これは、同じ仮定 A を二回使う必要がある問題です。まず A → A → B を仮定し、さらに A を仮定します。すると、A → A → B に A を適用して A → B が得られます。さらに、その A → B に同じ A をもう一度適用して B が得られます。最後に A の仮定をキャンセルして A → B を作り、さらに最初の仮定をキャンセルして全体の命題を得ます。

ここで重要なのは、同じ仮定 A が二回使われていることです。これが縮約則です。縮約則とは、同じ仮定を複数回使ってよいという規則です。通常の最小命題論理ではこれを許しますが、アフィン論理や線形論理では制限されます。証明木だけを見ると、この「同じ仮定を二回使った」という事実はやや見えにくいのですが、proof net にすると一目でわかります。A のワイヤが途中で二股に分かれるからです。この二股の分岐が Y 字ノードです。

第二の宿題は、A → (B → C) → (A → B) → C の証明でした。これは、A、B → C、A → B という三つの仮定をそれぞれ一回ずつ使う問題です。A → B に A を適用して B を得て、B → C に B を適用して C を得る。あとは仮定を順にキャンセルしていけば、目的の命題が得られます。この証明では、縮約則も弱化則も使われません。仮定がそれぞれ一回ずつ使われるため、proof net も非常にきれいな形になります。

この二つの宿題を比較すると、proof net の意義がよくわかります。証明木では、どちらもそれほど複雑には見えないかもしれません。しかし proof net で見ると、第一の問題には Y 字ノードがあり、第二の問題には Y 字ノードがありません。つまり、第一の証明ではリソースとしての仮定が複製されており、第二の証明では仮定が線形に流れています。証明の複雑さの違いが、ワイヤの形として可視化されるのです。

続いて、「ならば」の問題演習を行いました。今回の演習では、まず A → ((A → B) → A) を扱いました。これは弱化則の典型例です。A を仮定すれば A はすでに得られています。そのあと A → B を仮定しても、その仮定は使われません。それでも、A → B を仮定したもとで A が得られるので、(A → B) → A を作ることができます。さらに最初の A をキャンセルすれば、A → ((A → B) → A) が得られます。

ここで A → B という仮定は導入されたにもかかわらず、証明の中では一度も使われません。これが弱化則です。弱化則とは、使わない仮定を追加してよいという規則です。proof net では、この使われなかった仮定は宙ぶらりんのワイヤ、dangling wire として表されます。証明木では消えてしまう「使われなかった」という情報が、proof net では可視化されます。

次に、A → (A → B → C) → B → C を証明しました。これは三つの仮定を組み合わせる練習です。A を仮定し、A → B → C を仮定し、B を仮定します。A → B → C に A を適用すると B → C が得られ、そこに B を適用すると C が得られます。あとは B、A → B → C、A の仮定を順にキャンセルします。この証明では、それぞれの仮定が一回ずつ使われるため、縮約も弱化もありません。

さらに、否定を含む問題として、A → ¬¬A を扱いました。ここでは、まず ¬ を展開することが重要です。¬A は A → ⊥ なので、¬¬A は (A → ⊥) → ⊥ です。したがって、A → ¬¬A は、A → ((A → ⊥) → ⊥) という命題になります。

証明は単純です。A を仮定し、さらに A → ⊥ を仮定します。すると、A → ⊥ に A を適用して ⊥ が得られます。これにより、A → ⊥ を仮定すると ⊥ が得られるので、(A → ⊥) → ⊥ が導けます。最後に A の仮定をキャンセルすれば、A → ¬¬A が得られます。ここでは、⊥ の特別な規則は使っていません。あくまで → の除去規則だけで ⊥ を導いています。

次に、¬¬¬A → ¬A も扱いました。これも、まず否定を展開する必要があります。¬A は A → ⊥、¬¬A は (A → ⊥) → ⊥、¬¬¬A は ((A → ⊥) → ⊥) → ⊥ です。したがって、証明すべき命題は、(((A → ⊥) → ⊥) → ⊥) → (A → ⊥) です。

考え方は、先ほどの A → ¬¬A の技を流用することです。まず ¬¬¬A、つまり ((A → ⊥) → ⊥) → ⊥ を仮定します。次に、A を仮定して ⊥ を導ければ、A → ⊥、つまり ¬A が得られます。A を仮定したもとで、さらに A → ⊥ を仮定すれば、A と A → ⊥ から ⊥ が得られます。したがって、(A → ⊥) → ⊥ が得られます。これを最初の ¬¬¬A に適用すれば、⊥ が得られます。よって A → ⊥ が証明でき、全体として ¬¬¬A → ¬A が得られます。

エクストラ問題として、(A → B → C) → (A → B) → A → C も扱いました。これはコンビネータ論理の S コンビネータに対応する命題です。証明では、A → B → C、A → B、A を仮定します。A → B → C に A を適用して B → C を得ます。一方、A → B に同じ A を適用して B を得ます。最後に B → C に B を適用して C を得ます。ここで A の仮定が二回使われます。したがって、この証明には縮約則が含まれ、proof net では Y 字ノードが現れます。

このエクストラ問題を通じて、証明木の構造も整理しました。証明木には、葉、幹、根があります。葉は仮定、幹は推論の経路、根は最終的な結論です。また、証明木の中には主枝と従属演繹があります。主枝は証明全体の中心的な流れであり、従属演繹は仮定を置いて部分的に行われる推論です。

さらに、きれいな証明には、分析的部分と総合的部分があります。上のほうでは除去規則を使って、仮定から必要な結論を取り出していきます。これが分析的部分です。下のほうでは、導入規則を使って、目的の形の命題を組み立てていきます。これが総合的部分です。きれいな証明とは、除去規則による分析が上にあり、導入規則による総合が下にある、一方向の構造を持つ証明です。

後半では、proof net の見方と描き方を改めて確認しました。proof net は、証明図とは別のものではありません。証明図の中にすでに潜んでいる構造を取り出したものです。証明図の各命題に丸を付け、どの命題からどの命題へ情報が流れているかを線で結ぶと、proof net が現れます。

対応関係は単純です。証明図における命題は、proof net ではワイヤになります。推論規則はノードになります。キャンセルされた仮定は点線ワイヤになります。使われない仮定は宙ぶらりんのワイヤになります。同じ仮定が複数回使われる場合には、ワイヤが分岐し、Y 字ノードが現れます。

→除去規則は、A → B と A という二本の入力ワイヤから B という一本の出力ワイヤを作るノードです。→導入規則は、キャンセルされる仮定 A の点線ワイヤと、証明された B の実線ワイヤから、A → B という出力ワイヤを作るノードです。A → A の証明では、仮定 A がそのままキャンセルされるだけなので、最もシンプルな proof net になります。A → (B → A) の証明では、B の仮定が使われず、dangling wire として現れます。

proof net を読むときには、いくつかのチェックポイントがあります。まず、ワイヤの本数を見る。次に、点線ワイヤを見る。さらに、dangling wire があるかを確認する。Y 字ノードがあるかも重要です。Y 字ノードがあれば縮約則が使われています。dangling wire があれば弱化則が使われています。そして最後に、出力ワイヤのラベルが証明したい命題になっているかを確認します。

授業の最後には、新しい論理結合子として ∧、つまり「かつ」の規則を導入しました。∧ の導入規則は非常に直観的です。A が証明され、B も証明されているなら、A ∧ B が証明されます。つまり、二つの命題を合わせて「A かつ B」を作る規則です。

一方、∧ の除去規則は、A ∧ B から A を取り出す左除去と、A ∧ B から B を取り出す右除去の二つです。つまり、「A かつ B」が成り立っているなら、A だけを取り出してよいし、B だけを取り出してもよい。これは、∧ が「,（コンマ）」と同じ働きをしているということです。

たとえば、A → B → A ∧ B は、A を仮定し、B を仮定し、その二つから A ∧ B を導入すれば証明できます。逆に、A ∧ B → A は、A ∧ B を仮定し、∧ の左除去によって A を取り出し、最後に仮定をキャンセルすれば証明できます。同様に、A ∧ B → B も右除去で証明できます。

このように、A ∧ B を仮定することと、A および B をそれぞれ仮定することは、推論上ほとんど同じ働きをします。∧ は、二つの前提を一つの命題としてまとめるための記号であり、同時に、そのまとまりから左右の成分を取り出すための記号でもあります。したがって、∧ の意味もまた、導入規則と除去規則の対によって与えられます。

今回の授業全体を通じて確認したのは、証明を書くとは、単に「正しい結論にたどり着く」ことではないということです。どの仮定を置き、どの仮定を使い、どの仮定をキャンセルし、どの仮定を使わなかったのか。その構造まで含めて、証明は一つの計算過程です。proof net は、その計算過程をワイヤとノードとして可視化するための道具です。

また、否定を ¬A := A → ⊥ として定義することで、否定を特別扱いせず、「ならば」の体系の中で扱えることも確認しました。A → ¬¬A や ¬¬¬A → ¬A のような一見複雑な命題も、¬ を展開すれば、結局は → の導入規則と除去規則の組み合わせとして理解できます。

次回は、∨（または）の導入規則と除去規則に進みます。∧ が左右の成分を合わせる規則であるのに対して、∨ はどちらか一方から全体を作り、さらに場合分けによって使う規則です。これにより、自然演繹における主要な論理結合子の規則がかなり出そろっていきます。

今回のキーワード

自然演繹、ならば、含意、→、導入規則、除去規則、modus ponens、前件肯定、仮定のキャンセル、discharge、括弧の省略規則、右結合、優先順位、否定、¬、ボトム、⊥、¬A := A → ⊥、二重否定、三重否定、縮約則、弱化則、Y字ノード、dangling wire、proof net、証明ネット、証明木、葉、幹、根、主枝、従属演繹、分析的部分、総合的部分、Sコンビネータ、かつ、∧、∧導入、∧除去

宿題

本日の演習問題で解けなかったものを提出してください。

A, B, C は任意の命題です。¬A は A → ⊥ の略記です。可能な限りきれいな証明で示してください。

• 問1　A → ((A → B) → A)
• 問2　A → (A → B → C) → B → C
• 問3　A → ¬¬A
• 問4　¬¬¬A → ¬A
• Extra　(A → B → C) → (A → B) → A → C

授業中に解けた問題は提出不要です。解けなかった問題だけ提出してください。全問解けた場合は、「全問解けた」と KULMS に記入して提出してください。

問4・Extra は難しいので、できなければ「証明不可能と思う」または「途中まで：……」と書いて、途中経過を提出しても構いません。

提出は次回授業開始前までに、KULMS 授業サイトの「課題」から行ってください。

前期授業第4回（5/12）

授業第4回目の今回は、前回導入した「形式言語」「構成と解体」「導入規則と除去規則」「ハーモニー」という考え方を受けて、いよいよ自然演繹の推論規則に入ります。今回の中心は「ならば」、つまり含意記号 → です。

まず、→ の導入規則と除去規則を確認し、「A を仮定して B が証明できるなら A → B が証明できる」「A → B と A があれば B が得られる」という二つの規則を学びます。そのうえで、証明を木として書くだけでなく、ワイヤとノードからなる「証明ネット」として可視化する方法を紹介します。証明ネットは、仮定がどこからどこへ流れ、どこで使われ、どこでキャンセルされるのかを見えるようにするための道具です。

授業日時

5月12日（火）16：45〜18：15
文学部第4講義室

授業内容

• 前回のおさらい：形式言語・構成と解体・ハーモニー
• 宿題の答え合わせ・文の定義の改訂
• 「ならば」（→）の導入規則と除去規則
• ゲンツェンの自然演繹
• 仮定のキャンセルと証明木の読み方
• きれいな証明の書き方：最後の結合子から逆算する
• 論理的語彙の役割：明示化
• 縮約則・弱化則と論理体系のデザイン
• 証明ネット（proof net）入門
• 演習問題
• 宿題

speakerdeck.com

解説

• 今回の授業では、形式言語の中で実際に推論を行うための規則を導入します。前回までは、形式言語をどのように作るか、つまり項や命題をどのように帰納的に定義するかを見てきました。たとえば、変数や Z は項であり、t が項なら S(t) も項であり、t1 と t2 が項なら plus(t1, t2) も項である、というように、有限個の規則から無限に多くの記号列を構成できるのでした。

• 命題についても同様です。t1 と t2 が項なら t1 = t2 は文であり、A と B が文なら A ∧ B や A → B も文になる。つまり、形式言語とは、適当に記号を並べたものではなく、明示された構成規則に従って作られた記号列の体系です。今回からは、その形式言語の中で「正しい推論」をどのように定義するかを考えます。
  • 前回の重要なキーワードは、構成と解体でした。自然数もどきの例では、Z から S(Z) を作り、S(Z) から S(S(Z)) を作る操作が構成でした。これに対して、plus(S(Z), S(S(Z))) のような複雑な項を計算し、最終的に S(S(S(Z))) のようなカノニカルな形に直す操作が解体でした。
  • 論理結合子についても同じことが言えます。ある論理記号を含む命題を作る規則が導入規則であり、その論理記号を含む命題から情報を取り出す規則が除去規則です。したがって、導入規則は構成子に、除去規則は解体子に対応します。本授業で重視する証明論的意味論では、論理結合子の意味は、真理値表によってではなく、その導入規則と除去規則の対によって与えられます。

• 今回扱ったのは、「ならば」を表す含意記号 → です。
  • まず、数学で「ならば」がどのように使われているかを確認しました。たとえば、ある三角形について「∠A = 90°」を仮定し、そこから「∠B + ∠C = 90°」を導けたとします。このとき、私たちはその推論全体をまとめて、「∠A = 90° ならば ∠B + ∠C = 90°」と言うことができます。つまり、A を仮定して B が導けるなら、A → B という命題を作ることができます。これが → の導入です。
  • 一方で、「A ならば B」と「A」がすでにあるなら、そこから B を取り出すことができます。これは古くから modus ponens、つまり前件肯定と呼ばれてきた推論です。形式的には、A と A → B から B を得る規則です。これが → の除去です。
  • 自然演繹では、この二つの規則を次のように考えます。→導入規則では、A を仮定して B を証明できたとき、その仮定 A をキャンセルして A → B を証明します。ここで重要なのが、仮定のキャンセル、すなわち discharge です。証明の途中で「いったん A を仮定する」が、その仮定は最後に → を作るときに使い終わったものとして閉じられます。
  • 最も短い例は A → A の証明です。A を仮定すれば、当然 A は得られます。したがって、その仮定 A をキャンセルすれば、A → A が得られます。これは一見あまりにも自明ですが、自然演繹では、このような「仮定を置き、その仮定を使って結論を得て、最後に仮定をキャンセルする」という構造が非常に重要です。
  • →除去規則は、A と A → B から B を得る規則です。これは「A ならば B」と「A」があるなら「B」と言ってよい、というもっとも基本的な推論です。ここでは、A → B という命題に含まれている → が除去され、結論 B が取り出されます。したがって、→導入規則が → を作る規則であるのに対して、→除去規則は → を使って中身を取り出す規則です。
  • このように、→ の意味は、導入規則と除去規則の対によって与えられます。→導入によって入れたものだけを、→除去によって取り出せる。この釣り合いが、前回扱った局所的ハーモニーです。論理記号の規則がよく設計されているとは、導入と除去がこのように釣り合っているということです。
• 授業では次に、きれいな証明の書き方を学びました。基本方針は、「最後の結合子」から逆算することです。証明したい命題の一番外側の結合子が → であれば、その命題は →導入規則によって最後に作られたはずです。したがって、A → B を証明したいなら、まず A を仮定し、そのもとで B を証明すればよい、と考えます。
  • たとえば、A → (B → A) を証明したいとします。最後の結合子は外側の → なので、まず A を仮定して B → A を証明すればよい。次に、B → A の最後の結合子も → なので、B を仮定して A を証明すればよい。しかし A はすでに最初の仮定として持っています。したがって、B の仮定は実際には使われません。この「使わない仮定を置いてもよい」という性質が弱化則です。
  • このように、証明したい命題の形から逆算していくと、自然演繹の証明はかなり機械的に組み立てられます。もちろん、すべての証明が簡単に見つかるわけではありませんが、少なくとも → だけからなる単純な体系では、「最後の結合子を見る」という発想が非常に有効です。
• ここで、論理的語彙の役割についても触れました。ブランダムの言い方を借りれば、論理的語彙には「明示化」の役割があります。対象レベルで A から B が導出されるとき、メタレベルの観察者は「A から B が導出された」と述べることができます。→導入規則は、このメタレベルの事実を、対象レベルの命題 A → B として言語の中に取り込む働きをします。
  • つまり、→ とは、単に二つの文をつなぐ記号ではありません。それは、「この前提からこの結論が導ける」という推論上の関係を、対象言語の中で明示的に表現するための記号です。論理記号は、私たちがすでに行っている推論実践を、言語の中で見える形にする装置なのです。
  • ただし、この明示化がうまく機能するためには、規則が「悪さをしない」必要があります。導入規則と除去規則の釣り合いが崩れていると、論理記号は推論を明示化するどころか、体系全体を壊してしまいます。今後扱う tonk 問題は、その典型例です。
• 今回の後半では、仮定のキャンセルをめぐる論理体系のデザイン選択も確認しました。特に重要なのが、縮約則と弱化則です。縮約則とは、同じ仮定を複数回使ってよいという規則です。たとえば、同じ A という仮定を二箇所で使い、最後にまとめてキャンセルすることを許すかどうかが問題になります。最小命題論理ではこれを許しますが、アフィン論理では許しません。
  • 弱化則とは、使わない仮定を自由に追加してよいという規則です。A → (B → A) の証明では、B という仮定を置きますが、実際にはその B を使わずに A を得ます。このような未使用の仮定を許すかどうかも、論理体系によって異なります。最小命題論理やアフィン論理では弱化を許しますが、線形論理やランベック計算では許しません。
  • このように、論理体系は一つだけではありません。どの構造規則を認めるかによって、証明できる命題の集合が変わります。特に縮約則は、証明論的には正規化を難しくする重要な要因です。同じ仮定を複数回使えるということは、証明の一部を複製できるということでもあります。この複製が、後で扱う証明の正規化を非常に複雑にします。
• 最後に、証明ネットを導入しました。証明ネットとは、証明木をワイヤとノードとして描き直す方法です。通常の証明木では、命題がどこからどこへ流れているのか、同じ仮定がどのように使われているのかが見えにくい場合があります。そこで、命題をワイヤとして、推論規則をノードとして表現します。
  • →除去規則は、A → B と A という二本の入力ワイヤから B という一本の出力ワイヤを作るノードとして描けます。→導入規則は、仮定 A をキャンセルしながら B から A → B を作るノードとして描けます。キャンセルされた仮定は点線のワイヤで表し、使われない仮定は宙ぶらりんのワイヤとして表します。
  • 証明ネットの利点は、証明の構造が視覚的にわかることです。A → A の証明では、一本の仮定ワイヤがそのまま →導入によってキャンセルされるだけです。A → (B → A) の証明では、B の仮定が使われず、弱化として宙ぶらりんになることが見えます。(A → B) → (B → C) → (A → C) の証明では、A から B、B から C へと、ワイヤが順に →除去を通って流れていく様子が見えます。
  • さらに、縮約則を証明ネットで表すと、ワイヤが二股に分かれる Y 字ノードとして現れます。この Y 字ノードが、証明の複雑さを可視化します。Y 字がない体系では、証明の書き換えは比較的きれいに進みます。しかし Y 字があると、正規化の過程で証明の一部が複製され、その複製された部分にさらに Y 字が含まれていれば、複製がさらに複製を呼ぶことになります。これが、後半で扱う「証明論的悪夢」の入り口です。
• 今回の授業全体を通じて確認したのは、論理記号とは、ただ真理値を操作する記号ではなく、推論の構造を明示化するための装置だということです。→ は、A から B が導けるという推論上の関係を、A → B という命題として対象言語の中に取り込みます。その意味は、導入規則と除去規則の釣り合いによって与えられます。そして、証明ネットは、その推論の流れを見えるようにするための道具です。どの仮定が使われ、どの仮定が使われず、どこで命題が分岐し、どこで結論に流れ込むのか。これをワイヤとノードで見ることによって、証明の構造を単なる記号列ではなく、一種の配線図として理解できるようになります。今後は、→ だけでなく、∧、∨、¬ などの論理結合子についても導入規則と除去規則を学んでいきます。そのうえで、導入と除去の釣り合いが崩れたときに何が起こるのか、なぜ tonk のような「悪い論理記号」が問題になるのか、そして証明の正規化がハーモニーの核心としてどのような意味を持つのかを考えていきます。

今回のキーワード

自然演繹、ゲンツェン、ならば、含意、→、導入規則、除去規則、modus ponens、前件肯定、仮定のキャンセル、discharge、証明木、きれいな証明、正規な証明、最後の結合子、逆算、証明論的意味論、明示化、ブランダム、縮約則、弱化則、最小命題論理、アフィン論理、線形論理、ランベック計算、証明ネット、proof net、ジラール、ワイヤ、ノード、Y字ノード、正規化

宿題

スライド内を参照してください。

提出期限は5月19日（火）授業開始直前までです。KULMS授業サイトの「課題」から提出してください。「提出箱」ではありません。ファイルを添付後、「進める」だけでは提出完了にならないので、最後に必ず「提出」を押し、提出IDが表示されることを確認してください。

Word・tex・pdf、またはレポート用紙を撮影した画像で提出可能です。冒頭に、所属・氏名・学籍番号を記入してください。手書きで直接提出する場合は、授業開始前に講師へ提出してください。

宿題を解くのにかかった時間も必ず記入してください。これは今後の分量調整のために使います。

前期授業第3回（4/28）

授業第3回目の今回は、前回扱った「システム2＝仮想計算機」という見方を出発点として、自然言語の曖昧さを排し、人間の再帰的言語能力を人工的に外部化したものとして形式言語を捉えます。そのうえで、以下の4つのキーワードの組を紹介し、論理学を学んでいく上で気をつけるべきことを概説します。

• メタレベル vs 対象レベル
• 構成子 vs 解体子
• 意味論 vs 統辞論
• 局所的 vs 全域的

授業日時

4月28日（火）16：45〜18：15

授業内容

• 前回のおさらい：仮想計算機と I 言語
• 形式的手法：シミュレーション（メタレベル・対象レベル）
• 形式言語と帰納的定義（構成・解体・構成子・解体子）
• 統辞論と意味論
• ローカルとグローバル：ハーモニー
• 宿題

speakerdeck.com

解説

今回の授業では、形式言語を「人間の再帰的言語能力を人工的に外部化したもの」として定義する作業に入ります。
まず前回のおさらいとして、システム2は脳の上で動く仮想計算機である、という見方を確認しました。Macというハードウェアの上でWindowsが動くように、システム1用に進化した脳の上で、言語を使った論理的推論がシミュレートされる。これがシステム2です。システム2の重要な特徴は、言語で書かれているためにプログラマブルであることです。推論の規則を学んで身につけるとは、自分の仮想計算機のプログラムを更新することでもあります。
ここから、推論操作そのものを「対象として見る」能力が生まれます。ある文を前提として結論を導くとき、私たちは対象レベルで推論を実行しています。それに対して、「その推論はどのような構造を持っているのか」「どの規則に従っているのか」と外から記述・評価するとき、私たちはメタレベルに立っています。論理学にとって、この対象レベルとメタレベルの区別は決定的に重要です。
この区別を、今回も猫の写真で説明しました。黄色いジャンパーの人が猫に餌をやっている場面が対象レベルです。つまり、行為そのものを実行しているレベルです。それに対して、その様子を後ろからスマホで撮影している人がメタレベルです。つまり、行為を外から観察し、記述し、分析しているレベルです。「論理をする」と「論理学をする」の違いも、これと同じです（本写真は岸政彦氏からご本人の許可を受け使用させていただいているものです）。
次に、なぜ形式言語が必要なのかを考えました。自然言語は豊かですが、曖昧です。たとえば「ならば」という語も、「雨が降れば試合は中止だ」では条件を表しますが、「頑張ればできる」では励ましに近く、「これが人間の行為と呼べるならば……」では反語的に使われます。推論の形だけを厳密に扱うには、自然言語は不向きです。そこで必要になるのが、明示的な規則で作られた人工言語、すなわち形式言語です。
形式言語は、人間の推論をそのままコピーするものではありません。形式言語はシミュレーションです。川の氾濫シミュレーションが、実際の川底の小石や水面の細かな波紋までコピーするわけではないのと同じように、形式的論理体系も、人間の推論のすべてをコピーするわけではありません。感情、直観、文脈依存性などは捨象し、推論にとって本質的な記号操作の部分だけを取り出して、計算可能な体系として再現します。
その具体例として、自然数と「自然数をシミュレートする記号」の対応を見ました。メタレベルでは、自然数は 0, S(0), S(S(0)), ... と定義されます。対象レベルの形式言語では、これに対応する記号列として Z, S(Z), S(S(Z)), ... を作ります。記号そのものは違いますが、構造は同じです。0 に Z が対応し、後者関数 S が対象言語内の S に対応する。ここに、形式言語が自然数の算術をシミュレートするという発想があります。
この発想を支えるのが、基質中立性と構成性です。基質中立性とは、同じアルゴリズムはどのハードウェア上でも同じ手順で同じ結果を出す、という考え方です。紙の上であれ、脳内であれ、計算機のメモリ上であれ、同じレシピに従って構成されるなら、同じ対象が得られます。構成性とは、数学的対象を「どこかに実在するもの」としてではなく、共通のレシピによってその都度構成されるものとして捉える立場です。S(S(0)) は「2という物体が宇宙のどこかにある」ということではなく、「レシピ通りに構成した結果」です。
この構成性を、コンピュータの動作原理として「構成」と「解体」の二つに整理しました。構成とは、記号を付け足す操作です。Z から S(Z) を作り、S(Z) から S(S(Z)) を作る。これを担うのが構成子です。解体とは、逆に記号を減らす操作です。たとえば plus(S(S(Z)), S(S(Z))) のような複雑な項を計算して、最終的に S(S(S(S(Z)))) というカノニカルな形に直す。このとき、plus のような記号を消し、S と Z だけからなる形にしていく操作が解体です。
この構成と解体の考え方は、論理にも接続します。計算の場合、構成子は S や plus のような記号を導入し、解体子は eval などを通じて非カノニカルな項をカノニカルな項へ変換します。自然演繹の場合には、導入規則が構成子に、除去規則が解体子に対応します。論理結合子を証明に導入するのが導入規則であり、証明からその結合子を除去して情報を取り出すのが除去規則です。ここに、後半で扱う「導入規則と除去規則のハーモニー」の基礎があります。
その後、項と命題の帰納的定義を導入しました。項とは、Z、変数、S(t)、plus(t1, t2) などのように、明示された規則によって作られる記号列です。上記の規則に従って構成できるものだけが項であり、それ以外は項ではありません。さらに、t1 と t2 が項ならば t1 = t2 は原子命題であり、原子命題から ∧、→、¬ などを使って複合命題を作ることができます。こうして、有限個の規則から原理的に無限の文が生成されます。これは、I言語の再帰的能力を人工的に外部化したものです。
次に、統辞論と意味論の区別を確認しました。統辞論とは、記号列が文法的に正しいかどうかの問題です。Z = S(Z) や plus(Z, S(Z)) = S(Z) は、意味的に真か偽かとは別に、文法的には正しい記号列です。これに対して、S(∗) のように未定義の記号を含むものや、plus(=) のように項でないものを関数の引数にしているものは、整式ではありません。統辞論は「意味」を問わず、記号列が帰納的定義の規則に従って構成されているかを機械的にチェックします。
意味論は、それとは別に、記号列に意味を与える仕方を扱います。Z = S(Z) は文法的には正しいですが、標準的な解釈では「0 = 1」を表すので意味的には偽です。一方、plus(Z, S(Z)) = S(Z) は標準的な解釈では真です。記号列として正しいかどうかと、その記号列が正しいことを述べているかどうかは、別の問題です。
ただし、本授業で最終的に重視するのは、外界との対応としての意味論ではなく、証明論的意味論です。つまり、意味とは、記号が推論規則の中でどのように使われるかによって決まる、という立場です。この立場では、外界を直接見に行かなくても、推論規則の設計そのものを分析することで、記号の意味を理解しようとします。
最後に、ローカルとグローバルの問題を扱いました。個々の推論ステップが規則通りであることと、体系全体として正しい結論を保証できることは同じではありません。保守作業でも、各部門が自分の装置をすぐに直したいと考えることはローカルには合理的ですが、そのたびに大きなシステムを止めてしまえば、全体の稼働率は下がります。推論体系でも同じことが起こります。ローカルに「それっぽい」規則を入れてしまうと、体系全体として何でも証明できるようになる危険があります。tonk 演算子の問題はその典型です。
この問題を説明するために、ローカル・中間・グローバルという三つのレベルを導入しました。ローカルとは、証明図の書き換えなど、実際の記号操作のレベルです。中間とは、形式的な推論規則や論理体系の設計のレベルです。グローバルとは、「誰にとっても正しい推論」という社会的・公共的な目的のレベルです。ローカルに正しい操作をしていても、それだけではグローバルな正しさは保証されません。両者をつなぐ中間レベルの制度設計が必要になります。
ここで重要になるのがハーモニーです。ハーモニーとは、階層的なシステムにおいて、局所的な処理の正しさが全域的な目的の達成に結びついている状態です。局所的には、導入規則と除去規則が釣り合っていなければなりません。除去規則は、導入規則で入れたものだけを取り出せるように設計されていなければなりません。大域的には、どんな迂回路を経た証明も、有限回の書き換えによってカノニカルな証明へ変換できる必要があります。これが証明の正規化可能性であり、ダメットのいう「真正なハーモニー」です。
今回の授業全体を通じて確認したのは、形式言語とは単なる記号遊びではない、ということです。形式言語は、人間の再帰的言語能力を人工的に外部化し、推論を有限の記号操作として追跡可能にするためのシミュレーションです。そして、そのシミュレーションが「誰にとっても正しい推論」の基盤となるためには、構成と解体、導入と除去、ローカルとグローバルのあいだにハーモニーが必要になります。

今回のキーワード

形式言語、シミュレーション、対象レベル、メタレベル、帰納的定義、自然数もどき、基質中立性、構成性、構成子、解体子、カノニカルな表現、統辞論、意味論、整式（wff）、証明論的意味論、ローカル、グローバル、ハーモニー、正規化

宿題

スライド内を参照してください。
提出期限は5月12日（火）授業開始直前までです。PandA／KULMS授業サイトの提出箱、または授業開始前の紙提出で受け付けます。宿題を解くのにかかった時間も必ず記入してください。

第1回授業（4/14）質疑応答

第1回授業　質疑応答まとめ（No. 1）

授業日時：2026年4月14日（火）16:45–18:15

教室：京都大学 文学部第6演習室

科目： [2026前期火５] 科学哲学科学史（演習）

第1回授業では5つの質問をいただきました。授業の進行上十分に答えられなかった点も含めて整理します。Q1・Q4については前期後半（第11〜14回）で改めて取り上げます。なお、本QAは、学生に口頭で公開の許可を得たものですが、何らかの差し障りがあるものについては、直接矢田部まで授業時にお伝えください。

• • -

Q1. 保守的拡張における「参照点」の問題

【質問】

保守的拡張を使って推論の良し悪しを比べるとき、メタ的な立場から比較しているわけだが、そのメタの立場に立っている「我々の言語実践」が正しい推論をしているとどうやって言えるのか。また、人間の自然言語にも「ボッシェ」のようなダメな推論がたくさん含まれているはずで、それらが排除された理想状態における推論の正しさは何によって保証されるのか。

【回答】

ご指摘は正確です。保守的拡張・調和はどちらも**相対的な概念**であり、ある言語体系を別の体系と比較するためにはメタ理論が必要になります。

推論主義者はこのメタ理論自体も「絶対的に正しい基準点」ではなく、互いの言語体系を比較し合う営みの積み重ねだと考えます。外から見た唯一の正解があるわけではない。

「理想状態の推論」の正しさを保証する概念として**調和（harmony）**が機能しますが、自然言語には帰納的・経験的な推論が多く含まれており、それらはハーモニーが崩れている部分も多いです。その意味で、完全に内包的・形式的な推論体系を自然言語全体に求めることには無理があります。

この問題は前期後半（第11〜14回）のメインテーマです。

• • -

Q2. 「ドイツ人は野蛮人である」は外界参照なしに間違いと言えるか

【質問】

ドイツ人は野蛮であるというのが「間違い」なのは、21世紀という外在的な何かを参照しているからではないか。ドイツ人が野蛮である真なモデルもあり得るのではないか。形式的でなく意味論的に間違いと言うには、外界へのコミットメントが必要になるのではないか。

【回答】

非常に鋭い指摘です。

まず、あるモデルにおいてたまたまドイツ人が全員野蛮だったとしても、ドイツ人という**概念**が野蛮人を概念的に包摂しているかどうかは別の話です（歴史的偶然と概念分析の区別）。

ご指摘は実在論者からの正当な反論であり、反実在論的立場には響きませんが、実在論的立場からは有効な論点です。

ただし、ダメットの例の本来の目的は「ドイツ人は野蛮人であることが正しいか」を証明することではありません。**「ある概念を追加することで、本来引き出せなかった結論が出てきてしまう」**という推論の**構造**を示すことが目的です。「月はチーズでできている」という前提から「雪は白い」という結論を導くような、本来無関係な概念を経由して謎の結論が生じる構造が問題の核心です。ドイツ人と野蛮人でなくてもよいわけです。

• • -

Q3. SellarsとLLMの「所与なき言語使用者」

【質問】**

Sellarsは人間においても「所与（the given）」を想定することを批判している（「所与の神話」）。授業でLLMを「所与なき言語使用者」と表現していたが、Sellarsの文脈ではどう位置づけられるのか。Sellarsの批判は人間にも向けられているのに、LLMだけを「所与なき」と言うのは正確か。

【回答】

指摘はもっともで、スライドの表現はややミスリーディングでした。

Sellarsにとって「所与」とは概念的媒介なしの直接与件であり、これを知識の基礎にすることを批判したのですが、それでも人間には外界との**因果的なつながり**は残っています。知覚、身体、指示行為といった外界との直接的な接続が人間にはあります。

LLMにはその因果的な接続すらありません。つまり正確には「所与なき言語使用者」ではなく、**「所与どころか因果的接続すらない言語使用者」**が正確です。

Sellarsが批判した「所与への依存」という極端なケースをさらに極端にした存在として位置づけられます。その意味でLLMはDummett流反実在論の思考実験が工学的なシステムとして実装されてしまった状態、という見方ができます。

• • -

Q4. 調和（harmony）と保守的拡張の関係

【質問】

調和（harmony）と保守的拡張はどう違うのか。またDummett自身この2つをよく整理できていないとおっしゃっていたが、現状どう考えればよいか。

【回答】

大まかに言えば次の違いがあります。

• **調和（ローカルな概念）**：ある論理定項の導入規則と除去規則がうまく釣り合っている状態。個々の規則ペアの問題。例： の導入規則（ と から を導く）と除去規則（ から を取り出す）が釣り合っている。

• **保守的拡張（グローバルな概念）**：言語全体を拡張したとき、新しく証明可能になる文が旧言語内に生じないこと。体系全体の問題。

両者は密接に関連しますが同一ではなく、Dummett自身も晩年までこの区別に苦労していました。現在も論争中の領域です。

この2つの概念の関係については、前期後半（第11〜14回）で正面から取り上げます。

• • -

Q5. 純粋に内包的な推論体系は自然言語に存在するか

【質問】

純粋に内包だけに依拠した推論体系は本当に存在するのか。数学を除けば科学的言語も何らかの形で外界と結びつくのではないか。外延的なものと内包的なものをそんなにきれいに切り分けられるのか疑問がある。

【回答】

おっしゃる通りで、経験科学は何らかの形で外界と結びつきます。

推論主義者（特にBrandom以降）は、形式的な論理体系の内的整合性をコアとして認めつつも、それ以外の知識についての外的コミットメントを全否定してはいません。

「完全に内包的な推論体系を自然言語全体に適用する」という主張の強さは立場によって大きく異なります。Dummettは論理結合詞の意味については検証条件に基づく推論主義で説明できると主張しましたが、自然言語全体への適用には慎重でした。

授業ではまず**命題論理の論理定項**（・・・）の意味を推論規則から説明できるかという最小のケースから出発します。自然言語全体への拡張可能性は後期の議論のテーマになります。

• • -

次回予告（第2回：2026年4月21日）**

形式言語・命題論理の構文論を導入します。本日のQ1・Q4で出た「メタレベルと対象レベル」の区別についても正式に導入します。宿題は第3回以降から出題予定です。

[2026前期] 科学哲学科学史（演習）論理学 第2回 授業内質疑応答

• 授業日時： 2026年4月21日（火）16:45〜18:15
• 教室： 京都大学 文学部第4講義室
• 担当： 矢田部俊介（西日本旅客鉄道株式会社）

• • -

Q1. 「サルは動物である」という推論は情報が増えているか

【質問】

授業では「前提にしたことよりも強い結論を出せてしまうことがおかしい」という話があった。では「XはサルであるゆえにXは動物である」という推論はどうなるのか。動物の方が外延が広いので情報が増えているように見えるが、これはOKな推論なのか。

【解答】

外延と内包の区別に注意してください。「サル」という概念を内包的に分析すると、サルとは「動物であり、哺乳類であり、霊長類である」ものです。つまり「動物である」という性質はすでにサルの概念の中に含まれています。
したがって「サルは動物である」という推論は、A∧B∧Cという前提からAを取り出す連言除去と同じ構造であり、導入したものだけを取り出しているので調和している推論です。
確かに外延的に見ると動物の集合はサルの集合より大きく「情報が増えた」ように感じられますが、これは内包と外延が逆向きの関係にあることから来る錯覚です（内包が大きいほど外延は小さくなる）。推論における情報の増減は内包のレベルで判断します。
典型例は「存在者」という概念です。「私は存在者である」は真ですが、存在者の外延はすべてのものを含む最大集合であり、内包（情報量）はほぼゼロです。外延が大きいほど内包は小さい——ここを混同しないようにしてください。

• • -

Q2. ライプニッツの有限性テーゼの射程

【質問】

ライプニッツが「推論の正しさは有限ステップの計算で確認できる」と言ったとき、その推論規則そのものの正しさは前提にされているのではないか。

【解答】

まったくその通りです。ここには二次元の問いがあります。

• 個別の推論のチェック：与えられた推論が特定の規則に従って正しく適用されているかを一ステップずつ確認する。これは有限ステップで可能です。
• 規則体系そのものの正しさ：使っている規則体系が矛盾していないかを問う。これはヒルベルト的な無矛盾性証明の問題であり、はるかに難しい問題です。

ライプニッツ自身はおそらくこの二次元の区別を明示的に問題にしていませんでした。現代的な観点から振り返れば、体系の無矛盾性が証明されて初めて個別の推論チェックが意味を持つということになります。現代論理学では規則体系を最初に明示的に定義した上で推論を行い、体系の無矛盾性・完全性は別途メタ理論として扱います。

• • -

Q3. 形式的体系の出発点と「ある」の前提

【質問】

出発点となる公理・定義はどこから来るのか。「ある（存在する）」ということすら前提にしなければならず、それを選ぶのは最終的に人間の「決め」なのか。

【解答】

現代的な立場からすれば、まったくその通りです。
形式的論理体系の構成は、まず使用する記号を定め、次に公理を宣言し、その上で推論規則に従って証明を展開します。何を公理として採用するかは選択の問題であり、目的に応じて使い分けられます（ユークリッド幾何か非ユークリッド幾何か、など）。
「三角形は3つの辺を持つ」という命題もユークリッドの公理系においては定義として与えられる出発点です。形式的にはこれを単なる記号列として扱い、記号列の操作として処理しても形式的には問題ありません。
ライプニッツ自身は必然的真理の体系が唯一正しいものとして外在的に存在すると考えていたと思われますが、それは現代的な立場とは異なります。

• • -

Q4. システム1とシステム2は不可分ではないか

【質問】

ε-δ論法を使って証明するとき、ルールをどう使うかの判断はシステム1に属する気がする。とすれば、システム1と2は不可分なのではないか。

【解答】

非常に重要な指摘で、授業のスライドでも「言語・数学＝システム2」ではないという補足をしました。
システム1・システム2の区別は「2種類の脳がある」という話ではなく、推論のモードの区別です。同じ数学的操作でも、学習前の人が一歩一歩確認しながら進めるのはシステム2的であり、習熟した数学者が「だいたいこんな感じ」と直感的に把握するのはシステム1的です。
ε-δ論法に慣れた人がほぼ自動的に証明の大枠を見通せるとすれば、システム1的に処理している部分があります。熟練した数学者が学生のレポートを見て「ここが怪しい」と瞬時に感じるのも、証明の記号列をパターン認識しているシステム1の働きです。
ただしカーネマン・スタノヴィッチ自身も認めているように、この区別はきれいに二分できるものではなく、複数の認知現象を整理するためのナラティブな枠組みです。両者が相互作用しながら機能しているというのがより正確な描像です。

• • -

Q5. タルスキーの定義不可能性定理と形式体系の自己正当化

【質問】

タルスキーの定義不可能性定理がある以上、形式的体系の中にとどまってその体系自身の是非を問うことはできないのではないか。メタ理論への連鎖は終わらないのではないか。

【解答】

まったくその通りです。これは論理学の最も根本的な問題の一つです。
タルスキーの定義不可能性定理が示しているのは、十分に豊かな体系の中ではその体系自身の真理述語を定義できないということです。体系Tについて語るにはメタ理論T'が必要になり、T'についてはメタメタ理論T''が必要になります。
タルスキー自身はこの無限の階層を問題として捉えていませんでした。階段をどんどん上っていけばよいというのがタルスキーのスタンスです。ただしゲーデルの不完全性定理以降、有限主義的な自己正当化は不可能であることが示されています。
この問題は前期後半（第11〜14回）の証明論的意味論の議論と深く関わります。

• • -

Q6. LLMはシステム1的だという議論の根拠と、ポアンカレとの対応

【質問】

LLMがシステム1に近いという議論はどこかに出典があるのか。またポアンカレの数学的直観とLLMを対応させる議論の可能性はあるか。

【解答】

「LLMはシステム1的である」というテーゼは、現時点では特定の単一の出典があるというより、複数の研究者が独立に指摘している観察です。LLMがニューラルネットワークによる統計的確率分布からトークンを生成するという仕組み自体がベイズ的・システム1的な推論に相当するという見方は比較的自然に出てきます。
ポアンカレとの対応については興味深い論点です。ポアンカレはヒルベルト・クーチュラの論理主義に対して、数学には論理では還元できない直観が不可欠だと論じました。この「数学的直観」はある意味でシステム1的であり、LLMがその種の「もっともらしさ」の認識において人間の直観に近い振る舞いをする可能性は論じる価値があります。

ただし決定的な違いがあります。人間の数学的直観は豊かな身体的・社会的経験に裏打ちされており、LLMの「もっともらしさ」は統計的パターンにすぎません。比較分析の研究テーマとしては面白い問いです。ぜひ論文でお書きになることをお勧めします。

• • -

Q7. 真理重視型・形式重視型と意味論・統語論の対比、および「証明論的意味論」の「意味論」

【質問】

真理重視型と形式重視型の違いは意味論的に定義するか統語論的に定義するかという対比に対応するのか。また「証明論的意味論」という言葉の「意味論」はどういう意味で使われているのか。

【解答】

対応関係はおおむねその通りですが注意が必要です。
真理重視型は通常タルスキー的なモデル論的意味論に基づき、形式重視型はゲンツェン的な証明論に基づきます。古典論理では完全性定理によってこの二つは同値になりますが、直観主義論理などではそうではありません。
「証明論的意味論」という言葉については、セマンティクスという語の使い方が論者によって大きく異なります。タルスキー的な真理関数的モデル意味論だけが「意味論」ではなく、圏論的意味論・ゲーム意味論など多様な立場があります。ダメットは導入規則がその語の「意味を定義する」という意味でこの立場をとりましたが、ジラールらは正規化ができるかどうかが体系の本質であり表記の違いに過ぎないという立場をとります。
関連性論理との接続も含め、第11〜14回で正面から取り上げます。

• • -

次回予告（第3回：2026年4月28日）**

メタレベルと対象レベルの区別を正式に導入した上で、形式言語の必要性と再帰的定義による命題論理の統語論を扱います。次回から宿題が出ます。資料は日曜夜までにKULMSにアップします。