前期授業第11回（6/30）

第10回では、tonkを作って壊し、「良い定義とは調和した規則のことだ」というところまで来ました。今回（第11回）は、その「調和（ハーモニー）」を、ぼんやりした標語ではなく数学的な条件として展開します。鍵になるのは、調和は一つの現象ではなく、ミクロ・中間・大域という三つのレベルの連鎖だ、という見方です。

三層とは、ミクロ（結合子1個を見る＝反転原理）、中間（証明全体を見る＝正規化）、大域（言語全体を見る＝保存拡大）の三つです。今回はこの三層がどう繋がるか、そしてどこで切れるかを追いました。連鎖は「反転原理（ミクロ）⇒ 正規化（中間）⇒ 保存拡大（大域）」で、tonkは一番下のリンクで切れるので、上の二層もろとも自滅します。

さらに今回は一歩踏み込んで、「三つのハーモニーは、いつも揃って成り立つのか？」という問いを立てました。答えは「いいえ」です。古典論理やCookの体系のように、三層が一致しない例があります。次回（第12回）は、正規化のもう一つの顔として、カット除去と推件計算へ進む予定です。

授業日時

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

授業内容

• 前回の回収：tonkを壊した「正体」を三層モデルとして定式化する
• 大域のハーモニー＝保存拡大性（Belnap 1962）の定義
• 保存拡大性の落とし穴：正しいが「非操作的」／言語相対性
• ミクロのハーモニー＝反転原理：ローレンツェンの「透明な窓」と許容可能性
• プラヴィッツの読み替え（1965）：除去は導入を「既に含んでいる」
• ∧のカット＆ペースト：1手で「戻せる」＝「消せる」（還元前と還元後の証明図）
• 中間のハーモニー＝正規化（真正のハーモニー）が三層を架橋する橋
• 連鎖まとめ：反転原理 ⇒ 正規化 ⇒ 保存拡大、tonkは最下層で折れる
• ダメットのハーモニー（1973a）と思想史（Lorenzen→Prawitz→Dummett）
• 意味の分子論：全体論と原子論の中間
• 三層は一致するとは限らない①：古典論理（正規化は成立、反転原理・保存拡大は破れる）
• 三層は一致するとは限らない②：早見表と散布図（古典論理とCookは鏡像）
• 発展：tonkは本当に死んだか？（Cook 2005）
• ふたたびLLMへ：ハルシネーションの三層診断／まとめ／演習

speakerdeck.com

解説

「良い規則」とは何か——三層モデルへ

前回（第10回）は、tonkを作って壊し、「良い定義とは調和した規則のことだ」というところまで来ました。今回はその「調和（ハーモニー）」を、数学的な条件として展開します。大事なのは、調和は一つの現象ではなく、ミクロ・中間・大域という三つのレベルの連鎖だ、という見方です。ミクロは結合子1個を見る反転原理、中間は証明全体を見る正規化、大域は言語全体を見る保存拡大です。今日はこの三層がどう繋がり、そしてどこで切れるのかを追いました。

大域のハーモニー：保存拡大性とその落とし穴

まず一番大きなレベル、大域から始めます。ブランダムの「論理は内容を足さない」という要求を数学的に書くと、保存拡大性（conservative extension）になります。体系Sに新しい結合子∘の導入・除去規則を足して S′ にしたとき、∘を含まない古い論理式φについて「S′でφが証明できる ⟺ Sでφが証明できる」が成り立つ、というのが保存拡大の定義です。つまり∘を足しても、∘を含まない命題の証明力は増えない。これはベルナップ（Belnap, 1962）がtonkへの応答として定式化したものです。∧・∨・→は保存拡大を満たし、tonkは満たしません。

ところがこの大域の基準には落とし穴があります。正しいのですが、''非操作的''なのです。「矛盾に陥らないよう何かをすればよい」と言われても、言語全体（可算無限個の命題）について「すべてのφで同値」を直接確かめるのは現実的ではありません。大域要求は目標を与えますが、行動規範（手順）を与えてくれないのです。さらにベルナップが強調したように、何が論理結合子かは''言語相対的''で、同じ規則でも足すベースの体系が違えば結果が変わりえます。

ミクロのハーモニー：反転原理と「透明な窓」

そこで、結合子1個ごとに・一目でチェックできる操作的な基準が欲しくなります。それがミクロのレベルの反転原理です。出発点はローレンツェン（Lorenzen, 1950年代）の許容可能性で、「その規則を足しても原子命題の証明可能な集合が大きくならない」という、保存拡大を原子命題に限定した種子のような条件です。ローレンツェンは論理結合子を''透明なガラス窓''になぞらえました（この比喩は本書のものです）。除去規則は透明で、余計なことをしない。A∨B ⊢ C は「Cの導出にはAとBの二つの前提が要る」以上の意味を持たない、というわけです。

これをプラヴィッツ（Prawitz, 1965）が自然演繹の除去規則に焦点を当てて再定式化したのが反転原理です。除去規則は導入規則の「反転」であり、導入の直後に除去すると元に戻ります。プラヴィッツ自身の言葉でいえば、導入してすぐ除去した証明（還元前）は、除去規則を使わない証明（還元後）を''「既に含んでいる」''のです。実際に∧でやってみましょう。AとBからA∧Bを作り（∧導入）、そこからAを取り出す（∧除去）のは遠回りです。でも左のAの証明を切り取って上に貼り直せば、A∧Bを経由せずにAが得られます。除去で取り出したAは、導入の時点で''もとから手元にあった''のです。この切り取り＆貼り付けが効くと、結合子を含まない結論からその結合子を消せます。つまりミクロ（反転原理）が大域（保存拡大）を導きます。

中間のハーモニー：正規化という橋

ミクロと大域をつなぐのが、中間レベルの正規化です。どんな証明も遠回りを全て消してカノニカルな証明に書き換えられる、という第8・9回の主役です。ダメットはこれを''真正のハーモニー''（intrinsic harmony）と呼び、もっとも本質的な調和としました。正規化は「ただの中間の一段」ではなく、ミクロの局所的な書き換えを証明全体に行き渡らせ、それによって大域の保存拡大を保証する橋なのです。こうして、反転原理（ミクロ）⇒ 正規化（中間）⇒ 保存拡大（大域）という連鎖ができあがります。tonkはこの連鎖の最初のリンク（反転原理）で切れます。tonk除去で取り出すBは、tonk導入の時点では手元になく、復元できないからです。だから中間も大域も総崩れになり、体系ごと自滅します。

統合：三層は一致するとは限らない

ここで一歩踏み込みました。三つのハーモニーは、いつも揃うのでしょうか。まず分子論の話から。ある命題Aの意味が変わったとき、影響が及ぶのはAを部分論理式として含む命題の意味だけです。これを意味の分子論（molecularism）と呼びます。全体論（クワインの信念の網：一文の変化が言語全体に波及する）と原子論（各文が独立）の中間で、部分論理式原理（カノニカルな証明には結論の部分論理式しか現れない）が効くからこそ、意味は適切なサイズの文脈で確定します。これは正規化が効くからこそ言えることです。

そして反例です。古典論理は、正規化定理もカット除去定理も成立します（ゲンツェン）。ところが排中律 ¬A∨A は前提なしで証明でき、この∨除去は還元できません。だから反転原理も保存拡大も成り立たない（古典は直観主義の保存拡大ではない）。''正規化は成り立つのに反転原理と保存拡大は破れる''のです。逆向きの例もあります。クック（Cook, 2005）は、推論の推移性（カット）を捨てれば、tonkを足しても自滅しない体系を作れることを示しました。tonkを保存拡大として追加できる代わりに、中間の橋（正規化）を失うのです。古典論理とCookはちょうど鏡像で、片方は正規化を保ち保存拡大を失い、もう片方は正規化を捨て保存拡大を得ます。三層は独立に壊れうる——「ハーモニーの間のハーモニー」は、いつでもあるわけではないのです。

ふたたびLLMへ

最後にLLMへ戻ります。LLMは「根拠なく言わない」という大域要求は（あるべきものとして）持っていても、各推論ステップの局所的な保証機構（反転原理に当たるもの）を持ちません。「矛盾しないよう何かすればよい」という非操作的な要求だけでは、実装は守れない。ハルシネーションを、三層のどこが欠けているかという診断の枠組みで捉え直せないか——これが引き続きの問いです。次回（第12回）は、正規化のもう一つの顔として、カット除去と推件計算に進む予定です。

今回のキーワード

保存拡大性（conservative extension）、ベルナップ（Belnap 1962）、非操作的、言語相対性、反転原理（inversion principle）、ローレンツェン（Lorenzen）、許容可能性（admissibility）、透明なガラス窓、プラヴィッツ（Prawitz 1965）、既に含んでいる、カット＆ペースト、正規化、真正のハーモニー（intrinsic harmony）、ダメット（Dummett 1973a）、三層モデル、ミクロ／中間／大域、意味の分子論（molecularism）、部分論理式原理、全体論／原子論、古典論理、排中律、ゲンツェン、カット除去、クック（Cook 2005）、推移性、tonk、自滅化、ハルシネーションの三層診断

宿題

当日の演習問題です。

''問1'': ある論理結合子について、導入規則の直後に除去規則を適用した遠回り（detour）を、カット＆ペーストで還元せよ（∧ または → で）。

''問2'': tonkに似た「壊れた結合子」を自作し、それが三層（ミクロ＝反転原理／中間＝正規化／大域＝保存拡大）のどこで、なぜ壊れるかを診断せよ。

（解答にかかった時間も書いてください。）

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

• • • -

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

前期授業第10回（6/23）

第8回・第9回では証明の正規化（detour＝遠回りを有限回の書き換えで消し、正規形にすること）を学びました。今回（第10回）は、その重労働が「何のためだったのか」を哲学的に回収する回です。第1回で投げたまま保留していた問い「意味とは何か」に立ち返り、意味の理論を1.0（対応説・真理重視型）と2.0（使用説・推論規則重視型）として整理し直しました。そのうえで2.0の核心を「良い定義とは何か」として展開し、素朴な2.0の危機であるPriorのTonkを提示して終わります。

今回の背骨は次の通りです。意味には二つの道がある（1.0は世界記述の理論で推論は二次的、2.0は使用説）→ 論理結合子の意味は導入規則と除去規則で定まる → ただし良い定義とは「単なる略記」であって現実について言えることを増やしてはならない（保存拡大）→ 悪い定義は結論を密輸する（アンセルム・ボッシュ）→ その論理結合子版がTonk → 体系が崩壊する → だから「調和」が要る（ゲンツェン）→ その調和は第8・9回の正規化で測れた、という伏線回収です。本格的な定式化は次回（第11回）に回します。

次回（第11回）は、今回名前だけ出した「調和」を数学的な条件として展開します。反転原理・正規化・保存拡大という三つのレベルの関係が主題です。

授業日時

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

授業内容

• 導入：正規化は何のためだったのか——第1回の問い「意味とは何か」への回帰
• LLMのハルシネーションを「意味」の問題として捉え直す
• 意味の理論1.0＝対応説（真理条件）と、その限界（推論の良し悪し・照合すべき外界がない場合）
• 1.0は「世界記述の理論」であって「推論の理論」ではない（命題が一次的・推論は二次的）
• ウィトゲンシュタイン『哲学探究』第2節の言語ゲーム（棟梁と見習い）
• 意味の理論2.0＝使用説：「語の意味とは、言語におけるその使われ方である」（探究43節）
• 論理学版の使用説＝証明論的意味論／推論主義（Dummett・Prawitz・Read）
• ブランダム：論理は推論を「明示化」する（doing → saying）
• 良い定義＝単なる略記、グローバルな要求としての保存拡大
• 悪い定義①：アンセルムの神の存在証明（結論の密輸）
• 悪い定義②：ボッシュ（ダメット）——導入と除去が釣り合わない
• 論理結合子版の悪い定義＝Tonk（Prior, 1960）の導入・除去規則
• Tonkの破綻：任意のAから任意のBが導け、体系が崩壊する
• 危機の診断＝調和（harmony）：除去で取り出せるのは導入で入れたものだけ
• ゲンツェン：導入規則は定義、除去規則はその帰結
• 伏線回収：調和は第8・9回の正規化で測れる（Tonkは正規化できない）
• 調和の三つのレベル（反転原理・正規化・保存拡大）——名前と位置づけのみ
• まとめ：ふたたびLLMへ／演習・次回予告

speakerdeck.com

解説

正規化は何のためだったのか——意味の問いへ戻る

第8回・第9回では、どんな証明も遠回り（detour）を有限回の書き換えで消して正規形にできる、という正規化を苦労して証明しました。今回はまず、その重労働が何のためだったのかを問い直すところから始めました。結論を先取りすれば、正規化は「ある哲学的な問いに答えるための準備」だったのです。その問いとは、第1回で投げたまま保留していた「意味とは何か」です。第1回では、LLMが存在しない論文をもっともらしく引用し、事実と異なることを自信ありげに述べる（ハルシネーション）現象を見ました。これは「嘘」ではありません。嘘をつく意図がそもそもないからです。では、LLM（あるいは私たち）にとって、文の「意味」とは何なのでしょうか。意味を説明する道は、大きく二つあります。

意味の理論1.0＝対応説とその限界

意味の理論1.0は、文の意味をその文が真となる条件（真理条件）だと考えます。「雪は白い」の意味は、雪が白いという事実に対応していることです。この立場では、ハルシネーションは外界との対応の失敗であり、診断は文を事実のデータベースと照合することになります。しかし1.0では捉えきれないことがあります。一つは推論そのものの良し悪しです。「雪は白い、ゆえに草は緑である」は、結論はたまたま正しくても推論はおかしいのですが、外界照合だけではこのおかしさを捉えられません。もう一つは、照合すべき外界がない場合です。数学の命題や「もし〜だったら」という反実仮想は、いったい何と照合すればよいのでしょうか。

ここで大事なのは、1.0の目的はそもそも「世界を記述すること」にあるという点です。1.0にとって論理的な推論とは、世界の記述状態（どのモデル）によらず真を保つ推論のこと（タルスキの「すべてのモデルで真」）です。つまり1.0では、命題（真理の担い手）が一次的な基礎概念であり、推論はそこから派生する二次的な概念にすぎません。これは第2回で見た、アリストテレスにおいて「形式」が必然性概念から導かれる二次的概念だった構造と同じです。しかし、論理学で本当に問いたいのは推論そのものではないでしょうか。推論の生成のメカニズム（導入規則と除去規則）や、推論の同値関係や変形（正規化）こそ知りたいのです。そこで、推論を一次的に扱う理論＝2.0が必要になります。

意味の理論2.0＝使用説：meaning is use

2.0の発想は、後期ウィトゲンシュタイン『哲学探究』にさかのぼります。第2節の言語ゲームでは、棟梁Aと見習いBが登場します。Aが「ブロック」「ピラー」「プレート」「ビーム」と叫ぶと、Bは対応する石材を運びます。この原始的な言語では、語の意味は辞書の定義ではなく、このやりとりのなかでの使われ方に尽きています。これが「意味とは使用である」という発想の出発点です。43節の有名な定式化は「語の意味とは、言語におけるその使われ方である」というものでした。

論理学版の使用説では、論理結合子の「使用」とは数学の証明のなかでの使われ方であり、それは導入規則（どんな根拠でその結合子を使ってよいか）と除去規則（その結合子から何を取り出してよいか）で定まります。この立場を証明論的意味論（proof-theoretic semantics）あるいは推論主義（inferentialism）と呼びます。担い手はDummett・Prawitz・Readです。さらにブランダムは、論理的語彙の役割を「明示化（making it explicit）」として捉えました。推論のなかに暗黙に含まれている各語の役割を、主張の形で明示するのが論理の仕事だ、という見方です。たとえば条件法 A→B は、「AからBを推してよい」という推論のふるまい（doing）を、「A→B」という主張（saying）に変えます。だから論理は内容を「足さない」——すでに行っている推論を明示するだけなのです。

良い定義＝略記、悪い定義＝密輸

論理結合子を導入規則・除去規則で定めることは、結局その結合子を「定義」することです。では良い定義とは何でしょうか。良い定義とは「単なる略記」です。既知の語を使って新しい語の使い方を定めるだけのもので、導入も除去もスムーズにできます。そしてグローバルな要求として、定義したからといって現実について言えることが増えてはいけません。これが保存拡大（conservative extension）です。定義は言葉だけに関わるべきで、いつのまにか世界について何かを主張してはなりません。

悪い定義は、こっそり結論を密輸します。例の一つはアンセルムの神の存在証明です。神を「肯定的な性質を全て持つもの」と定義し、「存在する」も肯定的な性質だとすれば、定義から「神は存在する」が出てしまいます。言葉の定義のはずが、いつのまにか現実について何かを言ってしまっているのです。もう一つはダメットの挙げる「ボッシュ」です。大戦期、英国人はドイツ人を「ボッシュ」と呼び、言外に「野蛮人」というニュアンスを込めました。導入規則は「xはドイツ人 ⊢ xはボッシュ」、除去規則は「xはボッシュ ⊢ xは野蛮人」です。合成すると「ドイツ人 → ボッシュ → 野蛮人」となり、導入でこっそり入れた「野蛮人」が除去で取り出されてしまいます。元の「ドイツ人」にはなかった含意が出てくる——これは導入と除去が釣り合っていない、つまり保存拡大の破れであり、悪い定義です。

Tonkの破綻と、調和という診断

この自然言語のボッシュと同じことを論理結合子でやったらどうなるか。それがPrior（1960）「The Runabout Inference-Ticket」の出した新しい結合子 tonk です。導入規則は ∨ の導入に似せて「A から A tonk B を導いてよい」、除去規則は ∧ の除去に似せて「A tonk B から B を取り出してよい」とします。この二つを合成すると、A から A tonk B を導入し、そこから B を除去できます。つまり任意のAから任意のBが導けてしまいます。Aが一つでも証明できれば（たとえば A→A）、あとは何でも証明できてしまい、体系は崩壊します。「導入規則と除去規則を勝手に置けば意味が決まる」という素朴な使用説は、このままでは破綻するのです。

なぜtonkはダメなのか。除去で取り出すBが、導入で入れたAと無関係だからです。良い結合子なら、除去で取り出せるのは導入で入れたものだけであるべきです。この導入と除去の釣り合いを調和（harmony）と呼びます。ではなぜ釣り合っている「はず」なのか。その原理的根拠は、自然演繹を作ったゲンツェン（1934）にさかのぼります。ゲンツェンの考えでは、導入規則はその論理結合子の「定義」とみなせ、除去規則は結局その定義からの帰結にすぎません。だとすれば、除去は定義（＝導入）で入れた以上のものを取り出せない——導入と除去には釣り合い（調和）があるはずなのです。

伏線回収：調和は正規化で測れる

ゲンツェンは「釣り合うはず」と言いました。では、その「はず」をどう確かめればよいのでしょうか。それがまさに第8・9回でやった正規化です。導入の直後に除去するという遠回り（detour）が必ず書き換えで消せる——これは、除去が導入の裏返しになっていることの証拠であり、調和の一つの測り方です。∧・∨・→・¬ は正規化できました。しかしtonkは正規化できません。遠回りを消す書き換えが存在しないのです。正規化という重労働は、2.0をtonkから救うための技術的な答えだったのです。

なお調和は、実は一つの概念ではなく複数のレベルがあります。ローカル（結合子1個のレベル）の反転原理、中間（証明全体のレベル）の正規化、グローバル（言語全体のレベル）の保存拡大の三つです。今日触れたのは中間の正規化（ダメットの言う「真正な調和」）でした。三者の関係は次回（第11回）で扱います。こうして使用説（2.0）は、「調和した規則に限る」という条件を付けて、はじめて本物の立場になります。最後にふたたびLLMへ。ハルシネーションを、「外界照合の失敗（1.0）」としてだけでなく、「推論規則の不調和／証明の遠回りが解けないこと（2.0）」として診断できないか——これが第11回以降に持ち越す問いです。

今回のキーワード

意味の理論1.0（対応説・真理条件・モデル的意味論）、意味の理論2.0（使用説・証明論的意味論・推論主義／inferentialism）、世界記述の理論、ウィトゲンシュタイン『哲学探究』、言語ゲーム、meaning is use、Dummett、Prawitz、Read、Brandom（明示化／making it explicit）、doing と saying、良い定義＝略記、保存拡大（conservative extension）、密輸、アンセルムの神の存在証明、ボッシュ（Boche）、Tonk（Prior, 1960）、体系の崩壊、調和（harmony）、ゲンツェン（1934）、導入規則は定義・除去規則は帰結、反転原理、正規化、真正な調和

宿題

当日口頭で指定した演習問題を提出してください。

''問1'': tonkの導入規則と除去規則を合成し、任意のAから任意のBが導けることを証明木で確かめよ。

''問2'': ボッシュの導入規則「xはドイツ人 ⊢ xはボッシュ」と除去規則「xはボッシュ ⊢ xは野蛮人」から「ドイツ人 ⊢ 野蛮人」が出ることを図示し、どこで釣り合い（調和）が破れているか説明せよ。

''問3'': ∧ の導入直後に除去する遠回り（detour）が、なぜtonkと違って消せるのか説明せよ。

（解答にかかった時間も書いてください。）

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

• • • -

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

前期授業第9回（6/16）

前回（第8回）は正規化定理の証明戦略を立てたが、最終盤（18:13）で「止まる」ことの説明が不完全なまま時間切れとなった。今回（第9回）はその続きとして、なぜ「止まる」証明が難しいかを丁寧に振り返り、「峰の高さ（degree）の多重集合」を計測器に選ぶことの正当性をヒドラゲームという道具を通じて明らかにした。授業の前半は前回の残課題（計測器選び）、後半はヒドラゲームの定式化とスコアベクタによる停止性証明が中心だった。

目次：

• Section 0：前回のおさらい（detour除去・見敵必殺）
• 前回で足りなかった説明：「止まる」はなぜ難しいか
• 第1幕：還元すると何が起きるか（§1.1 具体例）
• 第2幕：継ぎ目2か所——還元後に新detourが生まれる場所
• 第2幕：正しい計測器——峰の高さ（degree）
• 第3幕：抽象化——ヒドラゲームへの翻訳（対応表）
• 第4幕：ヒドラゲームのルールとプレイ実演
• 第5幕：スコアベクタと辞書式順序——停止性の証明
• 縮約がある場合・正規化定理の仲間たち・ジラールの洞察
• まとめ・演習・次回予告

授業の骨子は「正しい計測器の発見」です。detour数・証明の長さ・詰まりの数という3つの候補がそれぞれ停止の証明に使えない理由を確認し、「峰の高さだけを多重集合にまとめたもの」が正しい計測器であることをヒドラゲームを通じて説明しました。この計測器はヒドラゲームのスコアベクタとして定式化され、辞書式順序で毎手厳密に減少する——だから有限手で必ず終わる、という論法です。

次回（第10回・6/23）は推論主義（inferentialism）とTonkの問題に進みます。正規化定理が「良い論理規則の条件」とどう結びつくかが主題です。

授業日時

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

授業内容

• 前回のおさらい（正規化定理の主張・見敵必殺・→と∧のdetour除去）
• 前回の宿題（問1・問2）解答配布
• 前回で足りなかった説明：「止まる」がなぜ難しいか（detour数・長さ・詰まりの3候補の検討）
• 第1幕：§1.1の具体例で還元を実行——証明が縦に長くなる現象
• 第2幕：継ぎ目2か所——→還元後に上側・下側の2か所に新detourが生まれる
• 第2幕：峰の「高さ（degree）」が正しい計測器である理由
• 第3幕：抽象化——「峰の度数の多重集合」をヒドラゲームに翻訳（対応表）
• 第4幕：ヒドラゲームのルール（頭を刈ると高さが低い頭が最大2本増える）
• 第4幕：プレイ実演——{3}スタート最悪ケース（7手で終了）
• ヒドラ実況①②③：視覚的な進行の確認
• 第5幕：スコアベクタ（高さdの頭の本数cをならべたベクタ）の定義
• 第5幕：補題——1手ごとにスコアベクタが辞書式に厳密減少する
• 第5幕：補題——辞書式順序には無限下降列がない（二重帰納法）
• 第5幕：定理——アフィン版ヒドラゲームは必ず有限手で終わる
• 証明論への持ち帰り：正規化定理の停止性証明の完成
• 縮約がある場合の困難（本家Kirby-Paris問題・超限順序数の必要性）
• 正規化定理の仲間たち（弱・強正規化、カット除去定理、部分論理式原理）——前回再掲
• ジラールの洞察（前回再掲）
• 演習問題（問A・問B・問C、当日指定）
• 次回予告：第10回（6/23）推論主義とTonk

https://speakerdeck.com/player/PRESENTATION_ID speakerdeck.com

解説

前回の残課題——「止まる」はなぜ難しいか

第8回授業の終盤で、正規化の証明の核心として「1回の還元でdetourが必ず減る」ことを示す必要があると確認したが、その説明が不完全なままになっていた。今回はまずその原因を正面から確認した。

計測器の候補として次の3つが考えられる。

(1) ''detour個数''：1回の還元でdetour個数が増えることがある。→還元を実行すると、元の峰（A→B）は消えるが、代わりに π₁[π₂/u]という証明が合成され、その中に新たな継ぎ目（上側・下側）が現れてdetourになりうる。計測器として不適切。

(2) ''証明の長さ（縦）''：→還元では π₂ を π₁ に代入するため証明が縦に伸びる。前回授業記録（17:51）でこの現象を録音で確認した。長さは増えるので計測器にならない。

(3) ''詰まり（V字）の数''：実は「詰まりは減る」という側面があるが、その一方で証明の長さは増える。この2つは''逆方向に動く''ため、どちらか一方だけでは「全体として終わりに近づいている」と言えない。

• • -

第1幕：還元すると何が起きるか——§1.1 の具体例

具体的な証明図（§1.1）を使い、→還元を実際に実行した。峰の論理式は (A∧B)→A（高さ = degree 2）。

還元前：π₁（仮定[u: A∧B]を使い A を導く）と π₂（A∧B を証明する）が横に並び、→E の横棒がまたいで B を導く。

還元後：π₂ を π₁ の仮定[u: A∧B]に代入した証明 π₁[π₂/u] が縦に続く。A→B という峰は消えるが、証明は縦に延び、新たな峰（∧-detour）が生まれる可能性がある。

この例で「証明の長さは増える」「detour数は変わりうる」ことが具体的に確認できた。

• • -

第2幕：継ぎ目2か所——どこに新detourが生まれるか

→還元 π₁[π₂/u] を詳しく見ると、新しいdetourが生まれる可能性がある箇所は''ちょうど2か所''に限定される（アフィン論理の場合）。

''上側継ぎ目''：π₂ の底（I-規則）と π₁ 内で u の直上にある E-規則が接続される場所。π₂ の結論（A）が π₁ の I-規則の下に来るため、I→E の「V字」ができる可能性がある。

''下側継ぎ目''：π₁[π₂/u] の底（→I）と外側の文脈の E-規則が接続される場所。π₁ が A→B の証明だったなら、→I が下に来て外側の →E と接触する。

どちらの継ぎ目で生まれる新detourも、元の峰（A→B、degree d）より''低い''論理式が峰になる（degree < d）。これが停止性の鍵だ。

''正しい計測器の発見''：個々のdetourの個数ではなく、「峰の高さ（degree）の多重集合」を比較すれば良い。元の峰（degree d）が消え、生まれる新峰は全て degree < d ——つまり多重集合は「高い要素が消えて低い要素が増える」方向に変化する。

• • -

第3幕：抽象化——ヒドラゲームへの翻訳

峰の高さの多重集合という概念を、より直感的なゲームとして定式化する。これが''ヒドラゲーム''である。

対応表をまとめると次のようになる：

証明論	ヒドラゲーム
--------	-------------
証明図 π	ヒドラ（怪獣）
detour 1個	頭 1本
峰の degree	頭の高さ（1, 2, 3, ...）
還元 1回	頭を 1本刈る
新しい峰（高さ < d）	高さ < d の頭が高々2本
正規形（detourゼロ）	頭が全部なくなった
正規化の停止性	ゲームは必ず終わる

ヒドラゲームを使うと、論理式の構造という複雑な情報を捨て、「高さだけ」に集中できる。このような抽象化が数学の力だ。

アフィン論理（縮約なし）では、仮定ラベル u がちょうど1か所にしか現れないため、π₂ の代入は1か所のみ。したがって新しく生まれる峰の候補は継ぎ目2か所だけで、どちらも degree < d。これが「高さ < d の頭が''高々2本''」という制約の由来だ。

• • -

第4幕：ヒドラゲームのルールとプレイ実演

アフィン版ヒドラゲームのルール（§4 の形式化）：

1. ヒドラは自然数の有限多重集合 H（各要素が「頭の高さ」）
2. 1手ごとに任意の要素 d ∈ H を選んで取り除く（「刈る」）
3. 刈った d に対し、d より低い高さの要素を最大2本まで追加できる
4. H = ∅ になったらゲーム終了（ヘラクレスの勝ち）

§4.2 の実演：{3}（高さ3の頭1本）から最悪ケースをたどる。

• 手1：高さ3を刈る → {2, 2}（辞書式ベクタ (1,0,0) → (0,2,0) に減少）
• 手2：高さ2を1本刈る → {2, 1, 1}（(0,2,0) → (0,1,2) に減少）
• 手3：高さ2を刈る → {1,1,1,1}（(0,1,2) → (0,0,4) に減少）
• 手4〜7：高さ1を1本ずつ刈る（4本→3→2→1→0）

計7手で終了。頭の本数は一度4本まで増えるが、ゲームは有限手で必ず終わる。

• • -

第5幕：スコアベクタと辞書式順序——停止性の証明

''スコアベクタ''の定義：初期状態の最大高さを D とする。ヒドラの現在状態を

(c_D, c_{D-1}, ..., c_2, c_1)

というベクタで表す。ここで c_d は高さ d の頭の本数。

''補題（辞書式減少）''：高さ d の頭を1本刈ると、c_d が1減り、c_i（i < d）がいくつか増えうる。辞書式順序では左の桁が優先されるため、c_d の位置（左）が1減れば、右の桁がどれだけ増えてもベクタ全体は辞書式に小さくなる。''→ スコアベクタは毎手厳密に減少する。''

''補題（辞書式整礎性）''：(N^D, 辞書式順序)には無限下降列は存在しない。証明は D についての帰納法：D=1 は自然数の最小原理（N に無限下降列なし）。D → D+1 のステップでは、無限下降列があると仮定すると第1成分が有限回で安定し、その後は第2〜D+1成分が N^D で辞書式無限下降することになるが、これは帰納仮定に矛盾する。□

''定理（アフィン版ヒドラゲームの停止性）''：どのような手順でヒドラを刈っても、アフィン版ヒドラゲームは有限手で必ず終わる。

''証明論への持ち帰り''：証明図の正規化はヒドラゲームの停止性に帰着した。スコアベクタが毎手（＝毎回の還元で）辞書式に減少し、辞書式順序には無限下降列がないから、正規化は有限回の還元で完了する。アフィン論理の正規化定理が''完全に証明された''。

''縮約がある場合''：最小命題論理（縮約規則あり）では、仮定ラベル u が複数箇所に現れるため π₂ を k 箇所にコピーする必要がある。コピーの中に新たなdetourが増えうるため「高々2本」という制約が破れる。本家 Kirby-Paris ヒドラ（1982）では「n 本増える」という設定になり、停止性の証明には ω^ω 以上の超限順序数が必要になる。これは''ペアノ算術では証明できない''（Kirby-Paris 定理）という衝撃的な結果につながる（付録A3参照）。

• • -

正規化定理の仲間たち——前回からの再掲

''弱正規化と強正規化''：今回証明したのは弱正規化（少なくとも1つの還元列が正規形に到達する）に相当する。強正規化（どの順番で還元しても必ず終わる）はより強い主張で、最小命題論理でも成立するがより精密な議論が必要。

''カット除去定理（Hauptsatz）''：推件計算における対応物。自然演繹の detour が推件計算ではカット規則に対応する。

''部分論理式原理''：正規な証明では証明に現れる全ての論理式が結論または仮定の部分論理式になる。正規化定理から自動的に導かれる系。

''ジラールの洞察''：正規化定理は技術的便宜ではなく論理にとって本質的。正規な証明こそが「カノニカルな証明」であり、導入規則と除去規則の「調和」が正規化可能性と等価になる。Tonk（Prior, 1960）のような「不調和な」規則が正規化できないのはその帰結である。

今回のキーワード

停止性（termination）、スコアベクタ（score vector）、辞書式順序（lexicographic order）、整礎性（well-foundedness）、ヒドラゲーム（Hydra game）、アフィン版ヒドラ、本家 Kirby-Paris ヒドラ、degree（峰の高さ）、継ぎ目（junction point）、上側継ぎ目・下側継ぎ目、超限順序数（transfinite ordinal）、ω^ω、二重帰納法、弱正規化・強正規化、カット除去定理（Hauptsatz）、部分論理式原理

宿題

当日口頭で指定した演習問題（問A・問B・問C のうち指定したもの）を提出すること。

''問A'': §1.1 とは別の「→還元で新 ∧-detour が生まれる」例を自分で構成し、(a) 還元前のdetourと峰を全て挙げ、(b) →還元を1回実行し、(c) 生まれた新しい峰の論理式と degree を確認せよ。

''問B'': ヒドラ {高さ2の頭2本} = {2, 2} からゲームを始め、各状態のスコアベクタを書き、辞書式に減っていることを確認せよ（最悪ケースと最善ケースの両方を試みよ）。

''問C'': 高さ d の頭1本のアフィン版ヒドラゲームの最悪手数が 2^d − 1 であることを d = 1, 2, 3 で確かめよ（最悪手順を明示すること）。

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

前期授業第8回（6/9）

今回は正規化定理の証明を行いました。前回は「正規な証明とは何か」「detourとは何か」という定義と、正規化定理の主張（任意の証明は正規な証明に変換できる）を紹介したが、証明の手順は次回に持ち越しとなっていました。今回はその続きとして、実際に「どうやってdetourを除去するか」「なぜそれが有限回で終わるか」を追います。後半では、この定理がジラールの言葉を借りれば単なる技術的便宜ではなく論理の本質に関わるという話に触れ、次回の論理学の哲学（推論主義・Prior のTonk問題）への橋渡しとします。

目次：

• Section 0：前回おさらい（証明樹のかたち・V字型・detour）
• Section 1：アフィン論理で証明する + メタ定理と帰納法 + 見敵必殺戦略
• Section 2：各結合子のdetour除去（→・∧・∨）
• Section 3：停止性の証明（アフィン論理版）
• Section 4：縮約ありの指数的爆発と「隠れた回り道」
• Section 5：正規化定理の仲間たち（弱・強正規化、カット除去定理、部分論理式原理）
• ジラールの洞察と次回への橋渡し
• 演習問題

授業日時

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

授業内容

• 前回のおさらい：証明樹のV字型（上が除去規則・下が導入規則）、detourの定義、正規化定理の主張
• アフィン論理（縮約なし）での正規化定理の証明
• 正規化定理はメタ定理であることの確認（detour数への帰納法）
• 基本戦略：見敵必殺（Search and Destroy）
• →・∧・∨それぞれのdetour除去操作
• 停止性の証明（アフィン論理では還元でdetour数が単調に減る）
• 縮約規則ありの場合の困難（証明の複製・指数的爆発）
• 「隠れた回り道」問題（∨E 規則固有の問題）
• 弱正規化と強正規化の違い（前回Q&A Q3の回答）
• カット除去定理（Hauptsatz）との対応
• 部分論理式原理との関係
• ジラールの洞察：正規化定理と論理結合子の「意味」
• 演習問題：問1〜4（必修）＋チャレンジ（∨のdetour除去）

speakerdeck.com

解説

前回からの流れ：正規化定理とは何か**

前回（第7回）は自然演繹の証明がある特定の「きれいな形」を持つことができるという話をしました。証明図には''detour''（回り道）と呼ばれる冗長な部分があり、これは「導入規則で命題を組み立てた直後に、同じ結合子の除去規則でそれを壊す」パターンです。たとえば A と B から ∧I で A∧B を作り、すぐに ∧E_L で A だけ取り出すのはdetourの典型で、最初から A を使えばよいのです。

detourを含まない証明を''正規な証明''と呼びます。正規な証明は「V字型の構造」を持ちます：証明の上半分では除去規則を使って仮定から情報を取り出し、下半分では導入規則を使って結論を組み立てます。前回の第7回で「今日はこの定理の主張のみ」として紹介した正規化定理は次の主張です：

''「最小命題論理の任意の証明は、正規な証明に変換できる。」''

今回はこの定理を実際に証明しました。

アフィン論理での証明：なぜ縮約規則を外すか

証明の出発点として、最小命題論理そのものではなく''アフィン論理''（縮約規則のない体系）を対象に選ぶことを宣言しました。

縮約規則（contraction）とは「同じ前提を複数回使える」というルールです。proof netのY字ノードがこれに対応します。アフィン論理ではこの規則を外し、各前提はちょうど1回しか使えない。

なぜアフィン論理を選ぶか——縮約があると正規化の証明が極めて難しくなるためだ。具体的には、→のdetour除去では「仮定 [u:A] をAの証明で置き換える」という操作を行うが、縮約ありの場合は u が複数箇所に出てくるため、Aの証明を複製しなければならない。この複製の中に新しいdetourが生まれ、「1個消して2個増える」という事態が起きうる。最悪ケースでは証明サイズが指数関数的に膨らむ。アフィン論理なら u は1箇所だけなので複製が不要であり、停止性の議論がシンプルになる。

正規化定理はメタ定理：detour数への帰納法

正規化定理は対象言語（命題A, B, A→B, ...）の定理ではなく、''証明図の構造について語るメタ定理''である。「任意の証明図 π は正規形に変換できる」は、命題論理の命題ではなく、証明図そのものに関する主張だ。

証明の骨格は''detour数に対する帰納法''である。detour数とは証明図に含まれるdetourの個数——たとえば ∧I直後の ∧E が2か所あればdetour数は2。

• detour数 = 0：すでに正規形（帰納法の基底）
• detour数 = n+1：1回の還元操作でdetour数を n 以下にする → 帰納法の仮定を適用

アフィン論理では「1回の還元でdetour数が厳密に減る」ことが保証されるため（後述）、この帰納法が完全に機能する。

基本戦略：見敵必殺（Search and Destroy）

detour除去の基本戦略は三段階だ：
1. ''サーチ''：証明図の中をくまなく探し、detour（IノードとEノードの隣接）を見つける
2. ''デストロイ''：見つけたdetourを還元操作で消去する
3. ''繰り返し''：detourが残っていればステップ1に戻る

各結合子について「還元操作」の中身を確認した。

各結合子のdetour除去**

''→の場合''：
→I で A→B を作り、直後に →E で B を取り出す（A→B が「峰」）。
還元後は π_1 中の仮定 [u:A] を π_2（A の証明）で置き換えた証明 π_1[π_2/u] になる。A→B と →I・→E の両ノードが消える。アフィン論理では u が1か所だけなので π_2 の複製は不要。

''∧の場合''：
∧I で A∧B を作り、直後に ∧E_L で A を取り出す（A∧B が「峰」）。
還元後は A の証明 π_1 だけが残る。B の証明 π_2 は「実際には不要だった」ことになり消える（proof net ではBのワイヤがdangling wireになる）。∧E_R の場合は π_2 が残り π_1 が消える。

''∨の場合''：
∨I_L で A∨B を作り、直後に ∨E で場合分けする（A∨B が「峰」）。
∨I_L で「左から来た」という情報が保持されているため、左枝 π_2（[u:A] を使う証明）が生き残る。π_2 中の [u:A] を A の証明 π_1 で置き換えた証明になる。右枝 π_3 は消える。∨I_R の場合は右枝が生き残る。

停止性の証明（アフィン論理版）**

アフィン論理版正規化定理の証明の概略：

1. 証明 π に含まれるdetourの総数を n とおく（n は有限：証明図は有限サイズ）
2. アフィン論理では縮約規則がないため、各仮定ラベル u はちょうど1回しか出てこない
3. →の還元で π_1[π_2/u] を作るとき、u が1箇所だけなので π_2 を複製しない
4. したがって1回の還元でdetourの総数が厳密に n-1 以下になる
5. n は有限だから、高々 n 回の還元でdetourがゼロの証明（正規形）に到達する □

縮約ありの場合：指数的爆発と隠れた回り道**

最小命題論理（縮約あり）の場合は上述のように証明の複製が起き、停止性の証明に超限帰納法が必要になる。また証明サイズが 2^n オーダーに膨らみうる。

「隠れた回り道」問題は縮約とは''別の''問題である。∨E 規則は3入力の「大がかりな規則」であり、他の除去規則が ∨E の内外にまたがると、detour が見た目には存在しないにもかかわらず部分論理式原理が破れているケースが生じる。解決策は「順番変更（commuting conversion）」——∨E と他の除去規則の順番を入れ替えて隠れた回り道を顕在化させ、基本戦略で除去する。この問題は自然演繹に固有であり、推件計算では生じない。

正規化定理の仲間たち**

''弱正規化と強正規化''：
今日証明したのは「少なくとも1つの還元列が正規形に到達する（弱正規化）」。強正規化は「どの順番で還元しても必ず正規形に到達する」という強い主張であり、最小命題論理（アフィン論理も含む）でも成立するが証明には精密な議論が必要。これは前回Q&A Q3「スライドの正規化定理がネットで見るものと違う」という疑問への回答でもある。

''カット除去定理（Hauptsatz）''：
推件計算（sequent calculus）での対応物。自然演繹のdetourが推件計算ではカット規則に対応し、「カット規則を使わなくても証明できるものはカットを使っても証明できる」というゲンツェンのカット除去定理（Hauptsatz）が対応する。

''部分論理式原理''：
正規な証明では証明に現れる全ての論理式が結論または仮定の部分論理式になる。今回の証明から自動的に導かれる系である。

ジラールの洞察：正規化定理は論理の本質

Jean-Yves Girard（線形論理の創始者）の観点では、正規化定理は技術的便宜ではなく論理にとって本質的に重要な定理だ。正規な証明こそが論理的推論の「真の姿」——カノニカルな証明——であり、部分論理式原理はその証明が「結論の意味の範囲内で動く」ことを保証する。

ここで重要な観察が生まれる。导入規則は結合子に''意味を与え''、除去規則はその意味を''使う''。detour が除去できること = 導入と除去が「調和している」ということ。逆に言えば、正規化できない規則の組み合わせは「調和していない」——論理結合子として不適格である。

この観察は論理の哲学の核心問題につながる。「論理語の意味は推論規則で決まる」という立場（推論主義・inferentialism）を取るとき、任意の規則が「論理」になれるのか？ Arthur Prior（1960）は''Tonk''という接続子を提案し、その導入規則と除去規則を使うと任意の A から任意の B が証明できることを示した——明らかに論理として破綻している。Tonk はまさに正規化できない：Tonk-I の直後の Tonk-E は還元できないdetourである。

今回のキーワード

正規化定理（normalization theorem）、弱正規化（weak normalization）、強正規化（strong normalization）、アフィン論理（affine logic）、縮約規則（contraction rule）、メタ定理（metatheorem）、見敵必殺（Search and Destroy）、還元操作（reduction）、停止性（termination）、カット除去定理（Hauptsatz）、部分論理式原理（subformula property）、カノニカルな証明（canonical proof）、推論主義（inferentialism）、Tonk

宿題

スライドの演習問題（問1〜4・チャレンジ）のうち、授業中に解けなかったものを提出すること。

問1：スライドの問1の証明（∧I直後に∧E_L、∧I直後に∧E_R を含む冗長な証明）を正規化せよ。含まれるdetourを全て挙げること。
問2：スライドの問2の証明（(A→B)→(A→B) の非正規な証明）を正規化せよ。
問3：A∧(A→B)→B の正規な証明を逆算法で作れ。
問4：A→A∧A を最小命題論理（縮約規則あり）で証明せよ。
チャレンジ（加点・任意）：スライドのチャレンジ問題の証明（∨I_L 直後に ∨E が来ている A→A の証明）を正規化せよ。

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

前期授業第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 授業サイトの「課題」から行ってください。