JAIST Repository: 線形論理における古典的証明と 直観主義的証明の関係についての研究
70
0
0
全文
(2) 修 士 論 文. 線形論理におけ る 古典的証明と 直観主義的証明の関係について の研究. 北陸先端科学技術大学院大学 情報科学研究科情報科学専攻. 伊藤 成孝 2015 年 3 月.
(3) 修 士 論 文. 線形論理におけ る 古典的証明と 直観主義的証明の関係について の研究 指導教員 審査委員主査 審査委員 審査委員. 石原 哉教授 石原 哉教授 緒方 和博教授 寺内 多智弘教授. 北陸先端科学技術大学院大学 情報科学研究科情報科学専攻. 1210009 伊藤 成孝 提出年月: 2015 年 2 月. Copyright © 2015 by Yoshiyuki Ito. 2.
(4) 概要 本稿では、 線形論理に お け る 古典的証明と 直観主義的証明に ど れく ら いの差があ る のかを 調査する 。 特に 、 結合子がな ら ばに 関する ⊸ だけ から な る 論理と 直観主 義と 、 そ の論理に 定数 0 を 加え た 論理に 対する 、 古典的証明と 直観主義的証明の 関係を 調査する 。 形式体系に は帰納的証明構造を 用いて 、 グラ フ 的な つな がり を 論理式間に 与え 、 そ のつな がり に 関し て 特徴付け を 行う 。.
(5) 目次 第1章 1.1 1.2 1.3. はじ めに 古典論理と 直観主義論理 . . . . . . . . . . . . . . . . . . . . . . . . 先行研究 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 研究目的 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 第2章 2.1 2.2. 線形論理 線形論理と は . . . . . . . . . . . . . . . 線形論理に おけ る シーク エン ト 計算 . . 2.2.1 論理式 . . . . . . . . . . . . . . 2.2.2 古典線形論理 . . . . . . . . . . 2.2.3 直観主義線形論理 . . . . . . . . 2.2.4 様々 な 線形論理 . . . . . . . . . 構文論に 関する 結果 . . . . . . . . . . . 2.3.1 証明可能な シーク エン ト . . . . 2.3.2 可逆性 . . . . . . . . . . . . . . 2.3.3 カ ッ ト 除去 . . . . . . . . . . . . 様々 な 形式体系 . . . . . . . . . . . . . 2.4.1 片側シーク エン ト 計算 . . . . . 2.4.2 線形論理に おけ る 自然演繹 . . . 2.4.3 線形論理に おけ る ヒ ルベルト 流. 2.3. 2.4. 第3章 3.1. 3.2 3.3. 証明構造 乗法線形論理に 関する 証明構造 . . . . 3.1.1 証明構造 . . . . . . . . . . . . . 3.1.2 帰納的証明構造 . . . . . . . . . プルーフ ネ ッ ト と 帰納的証明構造 . . . ⊸ 結合子に 関する 帰納的証明構造 . . . 3.3.1 シーク エン ト 計算と の対応関係 3.3.2 帰納的証明構造に 関する 概念 .. i. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. . . . . . . . . . . . . . .. . . . . . . .. 1 1 1 2. . . . . . . . . . . . . . .. 3 3 4 4 6 8 8 9 9 10 12 18 18 19 19. . . . . . . .. 22 22 22 24 25 37 39 39.
(6) 可逆性 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. 41. 第4章 4.1 4.2. 線形論理におけ る 古典論理と 直観主義論理の関係 ⊸ 結合子だけ から な る 線形論理での関係 . . . . . . . . . . . . . . . MIZLL に 関する 関係 . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2.1 帰納的証明構造を 用いた ア プロ ーチ . . . . . . . . . . . . . .. 44 44 46 46. 第5章. 結論. 61. 3.3.3. ii.
(7) 第1章. はじ めに. 1.1 古典論理と 直観主義論理 古典論理と は、 最も よ く 使われる 論理である 。 こ れは研究に 関し て だけ でな く 、 日常生活に 関し て に も 言う こ と ができ る 。 例え ば、 高校生で習う 論理、 ディ ジタ ル回路やブール値な ど に 用いら れる のも 古典論理である 。 古典論理の特徴と し て 、 排中律 (A ∨ ¬A) や二重否定の除去律 (¬¬A → A) が成り 立つこ と 、 ド ・ モルガン の 法則 (A ∧ B ↔ ¬(¬A ∨ ¬B) な ど ) が成り 立つこ と が挙げら れる 。 ま た、 真理値表の よ う に 二値で表現でき る のも 特徴であ る 。 こ のよ う に 、 我々 の最も 身近な 論理が 古典論理であ る 。 し かし 、 論理は古典論理だ け ではな い。 直観主義論理と いう 古典論理よ り 弱い 論理がある 。 論理が弱いと は、 成り 立つ論理式が少な いこ と を 意味する 。 例え ば、 先ほど の排中律や二重否定の除去律は直観主義論理では成り 立た な い。 直観主義論理と は、 ブラ ウ ワ ーに よ る 直観主義的な 考え 方を 弟子のハイ テ ィ ン グが形式化し た こ と で生ま れた 論理であ る 。 ブラ ウ ワ ーは、 数学的対象は数学者 の精神の産物であ り 、 あ る 性質を も つ数学的対象が存在する と いう こ と を 示すに も 、 構成的な 手続き に 従っ て そ のよ う な 対象が存在する こ と を 示さ な け ればな ら な いと 考え た 。 こ れがブラ ウ ワ ーの直観主義的な 考え 方であ り 、 こ の考え 方を 形 式化し た も のが直観主義論理であ る 。 直観主義に 基づく 数学な ど は構成的数学と 呼ばれ、 様々 な 研究がな さ れて いる 。 ま た 、 直観主義論理に 関する 有名な 定理と し て 、 カ リ ー・ ハワ ード 同型対応が知ら れて いる 。 こ れは、 直観主義論理の証明 と プロ グラ ム の間に は対応関係があ る と いう 定理であ る 。 こ の定理から も 分かる よ う に 、 直観主義論理の研究は情報科学の観点から も 見て も 重要であ る 。. 1.2 先行研究 直観主義論理は古典論理よ り 弱い論理であ る と 述べた 。 つま り 、 そ れら の論理 の間には差がある 。 では、 ど れく ら いの差がある のだろ う か、 直観主義論理にど の よ う な 仮定を 加え る こ と で古典論理と 証明能力が同じ に な る のだろ う か。 よ く 知. 1.
(8) ら れた 結果と し て 、 論理式に 存在する 全て の変数に 対する 排中律ま た は、 二重否 定の除去律を 追加すれば古典論理と 証明能力が同じ に な る と いう 結果 [3] があ る 。 し かし 、 公理のよ う に 何も 加え な く て も 直観主義論理で成り 立つ論理式も 存在す る 。 よ っ て 、 次に 浮かび上がる 疑問は、 ど のよ う な 変数に 対する 排中律や二重否 定の除去律を 追加すれば十分な のかと いう こ と であ る 。 こ れに 対し て 、 論理式だ け を 見て 必要な 集合を 定める 結果が石原 [5, 6] に よ っ て 与え ら れた 。. 1.3 研究目的 本研究では線形論理に 対し て 、 こ の問題に 取り 組む 。 線形論理と は、 構造規則 を 制限し た 部分構造論理の１ つであ る 。 全て の資源 (仮定) は証明の中で必ず１ 度 だ け 使われる と いう 考え 方を 持つ論理であ る 。 線形論理に も 先ほど の論理と 同様 に 、 古典線形論理と 直観主義線形論理があ る 。 本研究の目的と し て は、 古典線形 論理と 直観主義論理の差はど れく ら いあ る のかを 解析する こ と であ る 。 ま た 、 先 行研究のよ う に 論理式だ け で定める のではな く 、 証明図を 解析し て 必要な 集合を 定めて いる 。. 2.
(9) 第2章. 線形論理. 2.1 線形論理と は 線形論理は 1987 年に ジャ ン ＝イ ヴ・ ジラ ールに よ っ て 提唱さ れた部分構造論理 であ る [4]。 部分構造論理と は、 構造規則を 制限し た 論理のこ と である 。 線形論理 では、 弱化 (weakening) 規則と 縮約 (contraction) 規則を 認めて いな い。 そ れに よ っ て 、 線形論理では仮定が資源のよ う に 扱われ、 証明の中で必ず一度だ け 使用さ れ な け ればな ら な い。 そ のた め、 仮定に ついて 何を いく つ使う のかと いう こ と を 明 確に 表現する こ と に 適し た 論理であ る 。 先ほど の論理と 線形論理の違いを 直観的 に 理解する た めに 、 買い物を 題材に し た 有名な 例があ る 。 論理式 A, B, C を それぞれ「 １ ０ ０ 円を 支払う 」、「 コ ーヒ ーが１ 本買え る 」、「 お茶 が１ 本買え る 」 こ と を 意味する も のと する 。 さ ら に 、「 １ ０ ０ 円でコ ーヒ ーが１ 本 買え る 」 こ と と 「 １ ０ ０ 円でお茶を １ 本買え る 」 こ と を 仮定する 。 つま り 、 A ⇒ B と A ⇒ C を 仮定する 。 線形論理のかつを ⋆ を 用いて 表現する と すれば、 以下のよ う な 証明図が得ら れる 。 A⇒B A⇒C A, A ⇒ B ⋆ C R⋆. A, A ⇒ B ⋆ C は、 ２ つの１ ０ ０ 円を 支払う こ と でコ ーヒ ーと お茶が買え る こ と を 意味し て いる 。 同様に 、 通常の論理で考え る と 、 A, A ⇒ B ∧ C の証明図だけ でな く 、 次のよ う な 証明図も 得る こ と ができ る 。 A⇒B A⇒C R∧ A ⇒ B∧C こ れは１ ０ ０ 円でコ ーヒ ーと お茶が買え る こ と を 意味し て いる 。 こ の例のよ う に 、 仮定を 自由に 用いる こ と を 許す論理に ついて 考え る と 、 日常生活の考え 方と 違い が生ま れて し ま う 。 逆に 、 数学のよ う に 仮定を 自由に 用いた 方が都合がよ い場合 は、 線形論理の考え 方は不便に 感じ ら れる 。. 3.
(10) 2.2 線形論理における シ ーク エン ト 計算 こ こ では、 線形論理に 対する 形式体系を 与え る 。 有名な 形式体系と し て 、 自然 演繹やヒ ルベルト 流、 シ ーク エン ト 計算があ る 。 最初の２ つは公理と 規則の紹介 に 留め、 本稿では主に シーク エン ト 計算を 用いて 議論する 。 シーク エン ト 計算は、 式 (sequent) Γ ⇒ ∆ を 用いて 計算する 形式体系である 。 こ こ で、 Γ, ∆ は論理式の列を 表す。 こ の式の直感的な 意味は、 Γ の中の全て の論理式 を 仮定すれば、 ∆ の中に 証明可能な 論理式が存在する と いう も のである 。 つま り 、 V W Γ → ∆ と 表すこ と も でき る 。. 2.2.1 論理式 初めに 、 線形論理で使用する 言語から 定義する 。 先ほど から 使用し て いる 論理 式な ど の言葉も こ こ で正確に 定義する 。 さ ら に 、 シ ーク エン ト 計算の定義に 必要 な 基本的な 概念も 定義する 。 線形論理の言語は以下のも のから な る 。. 1. 論理結合子 ∧, ∨, ⋆, +, ⊸, !, ? 2. 量化記号. ∀, ∃. 3. 対象変数. x, y, z, · · ·. 4. 対象定数. c, d, · · ·. 5. 関数記号. f, g, · · ·. 6. 述語記号. P, Q, · · ·. 7. 補助記号. (, ), , ( コ ン マ ). 項と 論理式は以下のよ う に 定義さ れる 。 定義 (項). t, s, · · · を 項と する 。. 1. 対象変数と 対象定数は項であ る 。 2. f が m 変数の関数記号で、 t1 , · · · , tm が項な ら ば、 f (t1, · · · , tm ) も 項であ る 。 定義 (論理式). A, B, C, · · · を 論理式と する 。. 4.
(11) 1. P が n 変数の述語記号で、 t1 , · · · , tm が項な ら ば、 P(t1 , · · · , tm ) は論理式であ る 。 こ の形の論理式を 原子論理式 (atomic formula) と 呼ぶ。 2. A, B が論理式な ら ば、 (A ◦ B) も 論理式であ る 。 た だし 、 ◦ ∈ {∧, ∨, ⋆, +, ⊸} 3. A が論理式で、 x が対象変数な ら ば、 (∀x.A) と (∃x.A) も 論理式であ る 。 4. A が論理式な ら ば、 (!A) と (?A) も 論理式であ る 。 以下の条件の元で混乱が生じ な いな ら ば括弧を 省略し て も よ い。. • ∀, ∃, !, ? は ∧, ∨, ⋆, +, ⊸ よ り 結合が強い。 • ∧, ∨, ⋆, + は ⊸ よ り 結合が強い。 • ∧, ∨, ⋆, + は左結合で、 ⊸ は右結合であ る 。 例. ((A ⋆ B) ⊸ C)) ((A + B) ∧ C) (A ∨ (B ⋆ C)) (A ⊸ (B ⊸ C)). = = = =. A⋆B⊸C A+B∧C A ∨ (B ⋆ C) A⊸B⊸C. 定義 (自由変数). A に 出現する 変数の集合を V(A) と する 。 こ のと き 、 論理式 A の 自由変数 FV(A) は以下のよ う に 定義さ れる 。. 1. A が原子論理式な ら ば、 FV(A) = V(A) であ る 。 2. ◦ ∈ {∧, ∨, ⋆, +, ⊸} と する と 、 FV(A ◦ B) = FV(A) ∪ FV(B) であ る 。 3. FV(∀x.A) = FV(∃x.A) = FV(A) \ {x} であ る 。 4. FV(!A) = FV(?A) = FV(A) であ る 。 定義 (束縛変数). ま た 、 論理式 A の束縛変数 BV(A) は以下のよ う に 定義さ れる 。. 1. A が原子論理式な ら ば、 BV(A) = ∅ であ る 。 2. ◦ ∈ {∧, ∨, ⋆, +, ⊸} と する と 、 BV(A ◦ B) = BV(A) ∪ BV(B) であ る 。 3. BV(∀x.A) = BV(∃x.A) = BV(A) ∪ {x} であ る 。 4. BV(!A) = BV(?A) = BV(A) であ る 。 5.
(12) こ れら を 用いて 項の代入を 定義を する 。 定義 (項の代入). x を 変数、 t を 項と する 。. 1. s を 項と する と き 、 s に 出現する x を t で置き 換え る こ と を s[x/t] と 表す。 2. A が原子論理式 P(s1 , · · · , sm ) な ら ば、 A[x/t] = P(s1 [x/t], · · · , sm [x/t]) である 。 3. ◦ ∈ {∧, ∨, ⋆, +, ⊸} と する と 、 (A ◦ B)[x/t] = A[x/t] ◦ B[x/t] であ る 。 4. ◦ ∈ {∀, ∃} と する と 、 ◦y.A に 関する 代入は以下であ る 。 ◦y.A (◦y.A)[x/t] = ◦y.A[x/t] ◦z.(A[y/z])[x/t]. x < FV(◦y.A) のと き x ∈ FV(◦y.A) かつ y < t のと き x ∈ FV(◦y.A) かつ y ∈ t のと き (z < V(A) ∪ V(t)). 5. ◦ ∈ {!, ?} と する と 、 (◦A)[x/t] = ◦(A[x/t]) であ る 。. 2.2.2 古典線形論理 初めに 、 古典線形論理に お け る シ ーク エン ト 計算を 定義する 。 シ ーク エン ト 計 算は、 １ つの公理と そ れぞれの結合子に 関する 推論規則から な る 。 さ ら に 、 推論 規則は L 規則と R 規則から な る 。 名前の通り 、 L 規則は ⇒ の左側に 関する 規則で、 R 規則は右側に 関する 規則であ る 。 ま た 、 式 Γ ⇒ ∆ から 規則に よ っ て 式 Γ′ ⇒ ∆′ が導出さ れる こ と を 、 以下のよ う に 表す。. Γ⇒∆ 規則 Γ′ ⇒ ∆′ ま た、 規則が適用さ れたと き に新たに出現し た論理式を 主論理式 (principal formula) と 呼ぶ。 古典線形論理のシーク エン ト 計算は表 2.1 で定義さ れる 。 こ こ で、 ⊥, ⊤, 0, 1 は定数である 。 こ こ から は Γ, ∆, · · · を 論理式の多重集合と する 。 例え ば、 古典線形 論理のシーク エン ト 計算を 用いて 以下のも のが得ら れる 。. p ⇒ p Ax R0 p ⇒ 0, p L0 R⊸ ⇒ p ⊸ 0, p 0⇒ L⊸ (p ⊸ 0) ⊸ 0 ⇒ p. p ⇒ p Ax p ⇒ p Ax R⋆ p, p ⇒ p ⋆ p. 6.
(13) 表 2.1: 古典線形論理に 対する シーク エン ト 計算 公理と カ ッ ト 規則 Γ ⇒ A, ∆ Γ′ , A ⇒ ∆′ Cut Ax p⇒p Γ, Γ′ ⇒ ∆, ∆′ 乗法と 加法結合子に 関する 規則 Γ, B ⇒ ∆ Γ ⇒ A, ∆ Γ ⇒ B, ∆ Γ, A ⇒ ∆ L∧ L∧ R∧ Γ, A ∧ B ⇒ ∆ Γ, A ∧ B ⇒ ∆ Γ ⇒ A ∧ B, ∆ Γ ⇒ A, ∆ Γ′ ⇒ B, ∆′ Γ, A, B ⇒ ∆ L⋆ R⋆ Γ, A ⋆ B ⇒ ∆ Γ, Γ′ ⇒ A ⋆ B, ∆, ∆′ Γ, A ⇒ ∆ Γ, B ⇒ ∆ Γ ⇒ A, ∆ Γ ⇒ B, ∆ L∨ R∨ R∨ Γ, A ∨ B ⇒ ∆ Γ ⇒ A ∨ B, ∆ Γ ⇒ A ∨ B, ∆ ′ ′ Γ ⇒ A, B, ∆ Γ, A ⇒ ∆ Γ , B ⇒ ∆ R+ ′ ′ L+ Γ, Γ , A + B ⇒ ∆, ∆ Γ ⇒ A + B, ∆ Γ, A ⇒ B, ∆ Γ, A ⇒ ∆ Γ′ , B ⇒ ∆′ R⊸ ′ ′ L ⊸ Γ, Γ , A ⊸ B ⇒ ∆, ∆ Γ ⇒ A ⊸ B, ∆ R⊤ L⊤ 規則は無し Γ ⇒ ⊤, ∆ Γ⇒∆ L1 R1 Γ, 1 ⇒ ∆ ⇒1 L⊥ Γ, ⊥ ⇒ ∆ R⊥ 規則は無し Γ⇒∆ R0 L0 0⇒ Γ ⇒ ∆, 0 量化結合子に 関する 規則 (y < FV(Γ) ∪ FV(∆)) Γ ⇒ A[x/y], ∆ Γ, A[x/t] ⇒ ∆ L∀ R∀ Γ, ∀x.A ⇒ ∆ Γ ⇒ ∀x.A, ∆ Γ, A[x/y] ⇒ ∆ Γ ⇒ A[x/t], ∆ L∃ R∃ Γ, ∃x.A ⇒ ∆ Γ ⇒ ∃x.A, ∆ 指数結合子に 関する 規則 Γ, A ⇒ ∆ !Γ ⇒ A, ?∆ Γ, !A, !A ⇒ ∆ Γ⇒∆ W! L! R! C! Γ, !A ⇒ ∆ Γ, !A ⇒ ∆ !Γ ⇒ !A, ?∆ Γ, !A ⇒ ∆ !Γ, A ⇒ ?∆ Γ ⇒ A, ∆ Γ ⇒ ?A, ?A, ∆ Γ⇒∆ W? L? R? C? Γ ⇒ ?A, ∆ !Γ, ?A ⇒ ?∆ Γ ⇒ ?A, ∆ Γ ⇒ ?A, ∆ ∼A≔A⊸0. 7.
(14) こ れら のよ う な 公理と 規則に よ っ て 式を 導出する 図を 証明図と 呼ぶ。 ま た 、 一番 下に 出現し た 式を 終式と 呼ぶ。 正式な 定義は以下で与え れる 。 定義 (証明図と 終式).. 1. 公理は証明図であ る 。 そ の証明図の終式は公理自身であ る 。 2. P1 は S 1 を 終式と する 証明図と する 。 S1 P1 こ のと き 、 S が規則の１ つであ れば、 S も 証明図であ る 。 そ の終式は S であ る 。 3. P1 , P2 はそ れぞれ S 1 , S 2 を 終式と する 証明図と する 。 S1 S2 P1 P2 こ のと き 、 S が規則の１ つであ れば、 S も 証明図であ る 。 そ の 終式は S であ る 。 式 S を 終式と する 証明図が存在する と き S はで証明可能であ る と いう 。 ま た 、 古典線形論理に お いて 式 S が証明可能であ る と き 、 CLL ⊢ S と 書く 。 先ほど の例 よ り 、 CLL ⊢ (p ⊸ 0) ⊸ 0 ⇒ p であ る 。. 2.2.3 直観主義線形論理 次に 、 直観主義線形論理に お け る シ ーク エン ト 計算を 定義する 。 線形論理に 限 ら ず、 直観主義論理のシ ーク エン ト 計算は古典論理のシ ーク エン ト 計算から 得る こ と ができ る 。 直観主義論理に おいて は、 式が ⇒ の右側が高々 １ つの論理式に 制 限さ れる 。 し た がっ て 、 シーク エン ト 計算の公理と 規則も ⇒ の右側が高々 １ つの 論理式に 制限さ れた 形に な る 。 つま り 、 表 2.1 の ⇒ の右側を 高々 １ つの論理式に 制限し た も のが、 直観主義線形論理のシーク エン ト 計算であ る 。 例え ば、 ⊸ 結合 子に 関する 規則は以下のよ う に な る 。 ∆ は高々 １ つの論理式であ る 。. Γ ⇒ A Γ′ , B ⇒ ∆ L⊸ Γ, Γ′ , A ⊸ B ⇒ ∆. Γ, A ⇒ B L⊸ Γ⇒A⊸B. 式の制限に よ り 、 直観主義線形論理では結合子 + と ? に 関する 規則を 除外する 。 そ し て 、 S が直観主義線形論理で証明可能であ る と き 、 ILL ⊢ S と 書く 。. 2.2.4 様々 な線形論理 線形論理に は多く の論理結合子があ っ た 。 そ れら は以下のよ う に ４ つのグルー プに 分け ら れる 。. 8.
(15) 乗法結合子 (multiplicative operators) 加法結合子 (additvie operators) 量化結合子 (quantifiers) 指数結合子 (exponentials). ⋆, +, ⊸, 0, 1 ∧, ∨, ⊤, ⊥ ∀, ∃ !, ?. こ れら のグループ分け を 元に 、 線形論理に は以下のよ う な 部分論理があ る 。. MLL MELL LL0 LLq LLe. 乗法結合子に ついて の規則から な る 論理 乗法結合子と 指数結合子に ついて の規則から な る 論理 乗法結合子と 加法結合子に ついて の規則から な る 論理 指数結合子を 除いた 規則から な る 論理 量化結合子を 除いた 規則から な る 論理. 例え ば、 古典線形論理を 乗法結合子だけ に 制限し た 論理を MCLL と 表記する 。 し た がっ て 、 MCLL ⊢ Γ ⇒ ∆ と 表記し た 場合、 古典線形論理を 乗法結合子だけ に 制 限し た 論理で Γ ⇒ ∆ が証明可能であ る こ と を 意味する 。. 2.3 構文論に関する 結果 こ こ では 2.2 で定義し たシーク エン ト 計算を 用いて 、 線形論理の構文論に 関する よ く 知ら れた 結果を 紹介する 。. 2.3.1 証明可能なシ ーク エン ト 定理. CLL ⊢ A ⇒ A かつ ILL ⊢ A ⇒ A。 証明. A の複雑さ に 関する 帰納法で示すこ と ができ る 。 定理. CLL ⊢ A ⇔∼∼ A。 (CLL ⊢ A ⇒∼∼ A かつ CLL ⊢∼∼ A ⇒ A の略記であ る 。 ) 証明. 以下のよ う な ２ つの証明図が得ら れる た め、 CLL ⊢ A ⇔∼∼ A が成り 立つ。. A⇒A R0 A ⇒ A, 0 L0 ⇒∼ A, A R ⊸ 0 ⇒ L ⊸ ∼∼ A ⇒ A. A⇒A 0⇒0 L⊸ A, ∼ A ⇒ 0 R ⊸ A ⇒∼∼ A. 9.
(16) 定理 (ド ・ モルガン の法則). 線形論理に おけ る ド ・ モルガン の法則は以下の同値関 係であ る 。. 1. CLL ⊢ A ⋆ B ⇔∼ (∼ A+ ∼ B) 2. CLL ⊢ 1 ⇔∼ 0 3. CLL ⊢ A ∧ B ⇔∼ (∼ A∨ ∼ B) 4. CLL ⊢ ⊤ ⇔∼ ⊥ 5. CLL ⊢ ∀x.A ⇔∼ (∃x. ∼ A) 6. CLL ⊢ !A ⇔∼ ? ∼ A 証明. 以下のよ う な ２ つの証明図が得ら れる ため、 CLL ⊢ A ⋆ B ⇔∼ (∼ A+ ∼ B) が 成り 立つ。. L0 L0 A⇒A 0⇒ B⇒B 0⇒ A, ∼ A ⇒ L ⊸ B, ∼ B ⇒ L ⊸ L+ A, B, ∼ A+ ∼ B ⇒ L⋆ A ⋆ B, ∼ A+ ∼ B ⇒ R0 A ⋆ B, ∼ A+ ∼ B ⇒ 0 R⊸ A ⋆ B ⇒∼ (∼ A+ ∼ B) A⇒A B⇒B R0 R0 A ⇒ A, 0 B ⇒ B, 0 ⇒∼ A, A R ⊸ ⇒∼ B, B R ⊸ R⋆ ⇒∼ A, ∼ B, A ⋆ B L0 ⇒∼ A+ ∼ B, A ⋆ B R+ 0⇒ L⊸ ∼ (∼ A+ ∼ B) ⇒ A ⋆ B 他の同値関係に 関し て も 同様に 証明図を 得る こ と ができ る 。. 2.3.2 可逆性 定義 (サイ ズ (measure)). 証明図 D に 対し て 、 証明図のサイ ズ d(D) を 以下のよ う に 定義する 。. • D が R1, L0 規則ま た は公理のみな ら ば、 d(D) = 0 であ る 。. 10.
(17) • D が D′ から L∧, R∨, L∀, R∃ ま た は指数結合子に 関する 規則のど れかに よ っ て 導出さ れた と き 、 d(D) = d(D′ ) + 1 であ る 。 • D が D′ と D′′ から R⋆, L+, L ⊸, Cut のど れかに よ っ て 導出さ れた と き 、 d(D) = max(d(D′ ), d(D′′ )) + 1 であ る 。 • D が D′ から R+, R ⊸, R0, R∀, L⋆, L1, L∃ のど れかに よ っ て 導出さ れた と き 、 d(D) = d(D′ ) であ る 。 • D が D′ と D′′ から R∧ ま たは L∨ によって導出さ れたと き 、 d(D) = max(d(D′ ), d(D′′ )) であ る 。 Γ ⇒ ∆ が d(D) ≤ n であ る D に よ っ て 導出可能な ら ば、 ⊢n Γ ⇒ ∆ と 書く 。 定理 (可逆性 (inversion lemma)). 古典線形論理で以下の同値関係が成り 立つ。 1. ⊢n Γ ⇒ A ⊸ B, ∆ iff ⊢n Γ, A ⇒ B, ∆ 2. ⊢n Γ, A ⋆ B ⇒ ∆ iff ⊢n Γ, A, B ⇒ ∆ 3. ⊢n Γ ⇒ A + B, ∆ iff ⊢n Γ ⇒ A, B, ∆ 4. ⊢n Γ ⇒ 0, ∆ iff ⊢n Γ ⇒ ∆ 5. ⊢n Γ, 1 ⇒ ∆ iff ⊢n Γ ⇒ ∆ 6. ⊢n Γ ⇒ A ∧ B, ∆ iff ⊢n Γ ⇒ A, ∆ かつ ⊢n Γ ⇒ B, ∆ 7. ⊢n Γ, A ∨ B ⇒ ∆ iff ⊢n Γ, A ⇒ ∆ かつ ⊢n Γ, B ⇒ ∆ 8. ⊢n Γ ⇒ ∀x.A, ∆ iff ⊢n Γ ⇒ A[x/y], ∆ (y < FV(Γ ∪ ∆ ∪ {∀x.A})) 9. ⊢n Γ, ∃x.A ⇒ ∆ iff ⊢n Γ ⇒ A[x/y], ∆ (y < FV(Γ ∪ ∆ ∪ {∃x.A})) ⇒ の右側を 高々 １ つの論理式に 制限すれば、 直観主義線形論理に おいて も 同様の こ と が成り 立つ。 証明 (CLL ⊢n Γ, A ⋆ B ⇒ ∆ iff CLL ⊢n Γ, A, B ⇒ ∆). こ こ で用いる シーク エン ト 計算は、 分かり やすく する た めに サイ ズを 明記し た 形で書く 。 (←) シーク エン ト 計算の規則と サイ ズの定義から 自明であ る 。 (→) 証明図の高さ に 関する 帰納法で示す。 基底段階 (base case). • 公理ま た は R1 ま た は L0 のと き Γ, A ⋆ B ⇒ ∆ の形に な ら な いので、 何も 証明すべき こ と はな い。 帰納段階 (induction step). 11.
(18) • 最後に L∧ が適用さ れた と き ⊢n−1 Γ, Ci , A ⋆ B ⇒ ∆ L∧ ⊢n Γ, C0 ∧ C1 , A ⋆ B ⇒ ∆. (i ∈ {0, 1}). こ のよ う に 導出さ れた と する と 、 以下よ う に 得る こ と ができ る 。. ⊢n−1 Γ, Ci , A ⋆ B ⇒ ∆ I.H. ⊢n−1 Γ, Ci , A, B ⇒ ∆ L∧ ⊢n Γ, C0 ∧ C1 , A, B ⇒ ∆. (i ∈ {0, 1}). • 最後に R∧ が適用さ れた と き ⊢n Γ, A ⋆ B ⇒ C0 , ∆ ⊢n Γ′ ⇒ C1 , ∆′ R∧ ⊢max(n,m) Γ, Γ′ , A ⋆ B∆ ⇒ C0 ∨ C1 , ∆′ こ のよ う に 導出さ れた と する と 、 以下よ う に 得る こ と ができ る 。. ⊢n Γ, A ⋆ B ⇒ C0 , ∆ I.H. ⊢n Γ, A, B ⇒ C0 , ∆ ⊢n Γ′ ⇒ C1 , ∆′ R∧ ⊢max(n,m) Γ, Γ′ , A, B ⇒ C0 ∨ C1 , ∆, ∆′ 同様の方法で他の論理式に ついて も 示すこ と ができ る 。. 他の同値関係に 対し て も 同様に 証明でき る 。. 2.3.3 カ ッ ト 除去 カ ッ ト 規則に 関する 重要な 定理を 示す。. Γ ⇒ A, ∆ Γ′ , A ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ 上記の A と ∼ A を カ ッ ト 論理式 (cut formula) と 呼ぶ。 カ ッ ト の階数 (cut of rank) と は、 カッ ト 論理式の複雑さ である 。 証明図のカッ ト 階級 (cutrank of deduction) と は、 証明図の中に 現れる 最大のカッ ト の階数である 。 カッ ト の階層 (level of cut) と は、 そ のカ ッ ト 規則ま での証明図の高さ であ る 。 定理 (カッ ト 除去 (cut elimination)). CLL ⊢ Γ ⇒ ∆ ま たは ILL ⊢ Γ ⇒ ∆ な ら ば、 カッ ト 規則を 使わな い証明図が得ら れる 。. 12.
(19) 証明 (古典線形論理に 関する カッ ト 除去). 証明図のカッ ト 階級ま たはカッ ト の階層 を 下げる こ と で帰納的に 示す。 基底段階. • ２ つのカ ッ ト 論理式が主論理式のと き – カ ッ ト 論理式が原子論式のと き p ⇒ p Ax p ⇒ p Ax Cut p⇒p こ のと き 、 以下のよ う な カ ッ ト 規則がな い証明図に 置き 換え ら れる 。. p ⇒ p Ax – カ ッ ト 論理式が 1 のと き ⇒1. Γ⇒∆ L1 1, Γ ⇒ ∆ Cut Γ⇒∆. R1. こ のと き 、 以下のよ う な カ ッ ト 規則がな い証明図に 置き 換え ら れる 。. Γ⇒∆ – カ ッ ト 論理式が 0 のと き Γ⇒∆ R0 L0 Γ ⇒ ∆, 0 0⇒ Cut Γ⇒∆ こ のと き 、 以下のよ う な カ ッ ト 規則がな い証明図に 置き 換え ら れる 。. Γ⇒∆ 帰納段階. • 少な く と も ど ち ら かのカ ッ ト 論理式が主論理式ではな いと き. 13.
(20) – ２ つの式から 導出さ れた と き Γ1 ⇒ ∆1 , A Γ2 ⇒ ∆2 規則 Γ, Γ′ ⇒ ∆, ∆′ , A A, Γ′′ ⇒ ∆′′ Cut Γ, Γ′ , Γ′′ ⇒ ∆, ∆′ , ∆′′ こ のと き 、 以下のよ う に カ ッ ト の階層を 下げる こ と ができ る 。. Γ1 ⇒ ∆1 , A A, Γ′′ ⇒ ∆′′ Cut Γ1 , Γ′′ ⇒ ∆1 , ∆′′ Γ2 ⇒ ∆2 規則 Γ, Γ′ , Γ′′ ⇒ ∆, ∆′ , ∆′′ – １ つの式から 導出さ れた と き Γ ⇒ ∆, A 規則 Γ′ ⇒ ∆′ , A A, Γ′′ ⇒ ∆′′ Cut ′ ′′ ′ Γ , Γ ⇒ ∆ , ∆′′ こ のと き 、 以下のよ う に カ ッ ト の階層を 下げる こ と ができ る 。. Γ ⇒ ∆, A A, Γ′′ ⇒ ∆′′ Cut Γ, Γ′′ ⇒ ∆, ∆′′ 規則 Γ′ , Γ′′ ⇒ ∆′ , ∆′′ • ２ つのカ ッ ト 論理式が主論理式のと き – カ ッ ト 論理式が A ∧ B のと き A, Γ ⇒ ∆ Γ′ ⇒ ∆′ , A Γ′ ⇒ ∆′ , B R∧ L∧ ′ ′ Γ ⇒ ∆ ,A∧ B A ∧ B, Γ ⇒ ∆ Cut Γ, Γ′ ⇒ ∆, ∆′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ′ ⇒ ∆′ , A A, Γ ⇒ ∆ Cut Γ, Γ′ ⇒ ∆, ∆′ – カ ッ ト 論理式が A ⋆ B のと き Γ ⇒ ∆, A Γ′ ⇒ ∆′ , B A, B, Γ′′ ⇒ ∆′′ R⋆ L⋆ Γ, Γ′ ⇒ ∆, ∆′ , A ⋆ B A ⋆ B, Γ′′ ⇒ ∆′′ Cut Γ, Γ′ , Γ′′ ⇒ ∆, ∆′ , ∆′′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ ⇒ ∆, A A, B, Γ′′ ⇒ ∆′′ Cut B, Γ, Γ′′ ⇒ ∆, ∆′′ Γ ⇒ ∆ ,B Cut Γ, Γ′ , Γ′′ ⇒ ∆, ∆′ , ∆′′ ′. ′. 14.
(21) – カ ッ ト 論理式が A ∨ B のと き Γ ⇒ ∆, A A, Γ′ ⇒ ∆′ B, Γ′ ⇒ ∆′ R∨ L∨ Γ ⇒ ∆, A ∨ B A ∨ B, Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ ⇒ ∆, A A, Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ – カ ッ ト 論理式が A + B のと き Γ′′ ⇒ ∆′′ , A, B A, Γ ⇒ ∆ B, Γ′ ⇒ ∆′ R+ L+ ′′ ′′ Γ ⇒ ∆ ,A+ B A + B, Γ, Γ′ ⇒ ∆, ∆′ Cut Γ, Γ′ , Γ′′ ⇒ ∆, ∆′ , ∆′′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ′′ ⇒ ∆′′ , A, B A, Γ ⇒ ∆ Cut Γ, Γ′′ ⇒ ∆, ∆′′, B B, Γ′ ⇒ ∆′ Cut ′ ′′ ′ ′′ Γ, Γ , Γ ⇒ ∆, ∆ , ∆ – カ ッ ト 論理式が A ⊸ B のと き Γ ⇒ ∆, A B, Γ′ ⇒ ∆′ A, Γ′′ ⇒ ∆′′ , B R ⊸ L⊸ Γ′′ ⇒ ∆′′ , A ⊸ B A ⊸ B, Γ, Γ′ ⇒ ∆, ∆′ Cut Γ, Γ′ , Γ′′ ⇒ ∆, ∆′, ∆′′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ ⇒ ∆, A A, Γ′′ ⇒ ∆′′ , B Cut Γ, Γ′′ ⇒ ∆, ∆′′ , B B, Γ′ ⇒ ∆′ Cut ′ ′′ ′ Γ, Γ , Γ ⇒ ∆, ∆ , ∆′′ – カ ッ ト 論理式が ∀x.A のと き A[x/y], Γ′ ⇒ ∆′ Γ ⇒ ∆, A[x/y] R∀ L∀ Γ ⇒ ∆, ∀x.A ∀x.A, Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ ⇒ ∆, A[x/y] A[x/y], Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ 15.
(22) – カ ッ ト 論理式が ∃x.A のと き Γ ⇒ ∆, A[x/y] A[x/y], Γ′ ⇒ ∆′ R∃ L∃ Γ ⇒ ∆, ∃x.A ∃x.A, Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ こ のと き 、 以下のよ う に 証明図のカ ッ ト 階級を 下げる こ と ができ る 。. Γ ⇒ ∆, A[x/y] A[x/y], Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ – カ ッ ト 論理式が !A のと き ⇒ の左側の !A の導出に よ っ て 以下のよ う に 分け ら れる 。 * W! 規則に よ っ て 導出さ れた と き !Γ ⇒ ?∆, A Γ′ ⇒ ∆′ R! W! !Γ ⇒ ?∆, !A !A, Γ′ ⇒ ∆′ Cut !Γ, Γ′ ⇒ ?∆, ∆′ こ のと き 、 L! と R? の規則を 複数回適用し て 、 以下のよ う に 証明図 を 得る こ と ができ る 。. Γ′ ⇒ ∆′ .. . ′ !Γ, Γ ⇒ ?∆, ∆′ * L! 規則に よ っ て 導出さ れた と き A, Γ′ ⇒ ∆′ !Γ ⇒ ?∆, A R! L! !Γ ⇒ ?∆, !A !A, Γ′ ⇒ ∆′ Cut !Γ, Γ′ ⇒ ?∆, ∆′ こ のと き 、 以下のよ う に証明図のカッ ト 階級を 下げる こ と ができ る 。. !Γ ⇒ ?∆, A A, Γ′ ⇒ ∆′ Cut Γ, Γ′ ⇒ ∆, ∆′ * C! 規則に よ っ て 導出さ れた と き !A, !A, Γ′ ⇒ ∆′ !Γ ⇒ ?∆, A C! R! !Γ ⇒ ?∆, !A !A, Γ′ ⇒ ∆′ Cut !Γ, Γ′ ⇒ ?∆, ∆′. 16.
(23) こ のと き 、 以下のよ う に カ ッ ト の階層を 下げる こ と ができ る 。. !Γ ⇒ ?∆, !A !A, !A, Γ′ ⇒ ∆′ Cut !Γ ⇒ ?∆, !A !A, !Γ, Γ′ ⇒ ?∆, ∆′ Cut !Γ, !Γ, Γ′ ⇒ ?∆, ?∆, ∆′ .. . !Γ, Γ′ ⇒ ?∆, ∆′ – カ ッ ト 論理式が ?A のと き ⇒ の右側の ?A の導出に よ っ て 以下のよ う に 分け ら れる 。 * W? 規則に よ っ て 導出さ れた と き A, !Γ′ ⇒ ?∆′ Γ⇒∆ W? L? Γ ⇒ ∆, ?A ?A, !Γ′ ⇒ ?∆′ Cut Γ, !Γ′ ⇒ ∆, ?∆′ こ のと き 、 L! と R? の規則を 複数回適用し て 、 以下のよ う に 証明図 を 得る こ と ができ る 。. Γ⇒∆ .. . ′ Γ, !Γ ⇒ ∆, ?∆′ * R? 規則に よ っ て 導出さ れた と き A, !Γ′ ⇒ ?∆′ Γ ⇒ ∆, A R? L? Γ ⇒ ∆, ?A ?A, !Γ′ ⇒ ?∆′ Cut Γ, !Γ′ ⇒ ∆, ?∆′ こ のと き 、 以下のよ う に証明図のカッ ト 階級を 下げる こ と ができ る 。. Γ ⇒ ∆, A A, !Γ′ ⇒ ?∆′ Cut Γ, !Γ′ ⇒ ∆, ?∆′ * C? 規則に よ っ て 導出さ れた と き Γ ⇒ ∆, ?A, ?A A, !Γ′ ⇒ ?∆′ C? L? Γ ⇒ ∆, ?A ?A, !Γ′ ⇒ ?∆′ Cut Γ, !Γ′ ⇒ ∆, ?∆′ こ のと き 、 以下のよ う に カ ッ ト の階層を 下げる こ と ができ る 。. Γ ⇒ ∆, ?A, ?A ?A, !Γ′ ⇒ ?∆′ Cut Γ, !Γ′ ⇒ ∆, ?∆′ , ?A ?A, !Γ′ ⇒ ?∆′ Cut ′ ′ ′ Γ, !Γ , !Γ ⇒ ∆, ?∆ , ?∆′ .. . Γ, !Γ′ ⇒ ∆, ?∆′ 17.
(24) こ のカッ ト 除去定理よ り 、 カッ ト 規則の無い線形論理に おいて も 、 カッ ト 規則を よ う な 考え 方を 用いて よ い。 つま り 、 Γ ⇒ ∆, A と A, Γ′ ⇒ ∆′ がカ ッ ト 規則のな い 線形論理で得ら れた と する 。 こ のと き 、 そ の論理では、 Γ, Γ′ ⇒ ∆, ∆′ も 得ら れる 。. 2.4 様々 な形式体系 こ れま でに 、 シーク エン ト 計算を 定義し て 様々 な 結果を 示し て き た。 こ こ では、 シーク エン ト 計算以外のよ く 知ら れた 形式体系を 紹介する 。. 2.4.1 片側シ ーク エン ト 計算 片側シ ーク エン ト 計算と は、 そ の名の通り シ ーク エン ト 計算を 片側だけ に し た 形式体系であ る 。 公理を ⇒ p, ∼ p と する こ と で片側だけ の形式体系を 実現し て い る 。 そ のた め、 古典線形論理に 関する 形式体系だ け を 考え る 。 ま た 、 片側し か使 用し な いので、 ⇒ も 落と し て いる 。 定義は表 2.2 であ る 。 表 2.2: 古典線形論理に 対する シーク エン ト 計算 公理と カ ッ ト 規則 Γ, A ∆, ∼ A Cut Ax p, ∼ p Γ, ∆ 結合子の規則 Γ, A ∆, B Γ, A Γ, B Γ, A Γ, B ⋆ ∧ ∨ ∨ Γ, A ∧ B Γ, ∆, A ⋆ B Γ, A ∨ B Γ, A ∨ B Γ, A, B Γ + ⊤ 0 1 Γ, A + B Γ, ⊤ 1 Γ, 0 量化結合子に 関する 規則 Γ, A[x/y] Γ, A[x/t] ∀ ∃ Γ, ∀x.A Γ, ∃x.A 指数結合子に 関する 規則 ?Γ, A Γ, A Γ, ?A, ?A Γ C ! W ? ?Γ, !A Γ, ?A Γ, ?A Γ, ?A. 18.
(25) 2.4.2 線形論理における 自然演繹 次に 、 自然演繹を 紹介する 。 自然演繹は、 数学で行う 推論に よ り 近い形式体系 である と も 言われる 。 こ の体系の規則は、 大き く 分け て 導入規則 I と 除去規則 E に 分け ら れる 。 ま た 、 シ ーク エン ト 計算のよ う に 式を 制限する のではな く 、 古典論 理のみ認める 規則に よ っ て 違いが生ま れる 。 先に 定義に 必要な 概念を 定義する 。 定義. 論理式 A に 出現する 変数 x に 対し て 、 t が自由であ る と は以下のよ う に 定義 さ れる 。. • A が原子論理式であ る と き 論理式 A に 出現する 変数 x に 対し て 、 t は自由であ る 。 • A ≡ B ◦ C (◦ ∈ {∧, ∨, ⋆, +, ⊸}) であ る と き B に 出現する x に 対し て t が自由で、 C に 出現する x に 対し て t が自由でな ら ば、 A に 出現する x に 対し て t は自由であ る 。 • A ≡ ∀y.B であ る と き x = y ま た は、 y < FV(t) かつ B に 出現する x に 対し て t が自由な ら ば、 A に 出現する x に 対し て t は自由であ る 。 た だし 、 x , y であ る 。 • A ≡ ◦B (◦ ∈ {!, ?}) であ る と き B に 出現する x に 対し て t が自由な ら ば、 A に 出現する x に 対し て t は自由で ある 。 自然演繹の定義は表 2.3 であ る 。. 2.4.3 線形論理における ヒ ルベルト 流 最後に 、 ヒ ルベルト 流と 呼ばれる 形式体系を 紹介する 。 先ほど ま での形式体系 は、 １ つの公理と 多く の規則から 構成さ れて いた 。 そ れに 対し て 、 ヒ ルベルト 流 は多く の公理と 少し の規則から 構成さ れる 。 ヒ ルベルト 流の定義は表 2.4 である 。. 19.
(26) 表 2.3: 線形論理に おけ る 自然演繹. ⊤I p ⊢ p Ax Γ⊢⊤ Γ⊢A Γ⊢B ∧I Γ, ∆ ⊢ A ∧ B Γ⊢A ∆⊢B ⋆I Γ, ∆ ⊢ A ⋆ B Γ ⊢ Ai ∨I (i ∈ {0, 1}) Γ ⊢ A0 ∨ A1 i Γ, A ⊢ B ⊸I Γ⊢A⊸B ⊢1. ⊥E Γ, ⊥ ⊢ A Γ ⊢ A0 ∧ A1 ∧Ei (i ∈ {0, 1}) Γ ⊢ Ai Γ ⊢ A ⋆ B ∆, A, B ⊢ C ⋆E Γ, ∆ ⊢ C ∆ ⊢ A ∨ B A, Γ ⊢ C B, Γ ⊢ C ∨E Γ, ∆ ⊢ C Γ, A ⇒ ∆ ∆ ⊢ A ⊸E Γ, ∆ ⊢ A ⊸ B Γ⊢1 ∆⊢A 1E Γ, ∆ ⊢ A. 1I. Γ, A ⊸ 0 ⊢ 0 0E ( 古典線形論理のみ ) Γ⊢A Γ ⊢ A[x/y] Γ ⊢ ∀x.A ∀E ∀I Γ ⊢ ∀x.A Γ ⊢ A[x/t] Γ ⊢ ∃x.A ∆, A[x/y] ⊢ C Γ ⊢ A[x/t] ∃E ∃I Γ ⊢ ∃x.A Γ, ∆ ⊢ C Γ ⊢ !A ∆ ⊢ C W !Γ ⊢ A !I !E !Γ ⊢ !A Γ, ∆ ⊢ C Γ ⊢ !A ∆, A ⊢ C Γ ⊢ !A ∆, !A, !A ⊢ C C !E !E Γ, ∆ ⊢ C Γ, ∆ ⊢ C t, y は x に 対し て 自由で、 y < FV(A) であ る 。 古典線形論理での + と ? は、 ド ・ モルガン の法則に よ っ て 定義さ れる 。 (∼ A ≔ A ⊸ 0). 20.
(27) 表 2.4: 古典線形論理に 対する ヒ ルベルト 流 公理と カ ッ ト 規則 (1) A⊸A (2) (A ⊸ B) ⊸ ((B ⊸ C) ⊸ (A ⊸ C)) (3) (A ⊸ (B ⊸ C)) ⊸ (B ⊸ (A ⊸ C)) (4) ((A ⊸ 0) ⊸ 0) ⊸ A ( 古典線形論理のみ ) (5) A ⊸ (B ⊸ A ⋆ B) (6) (A ⊸ (B ⊸ C)) ⊸ (A ⋆ B ⊸ C) (7) 1 (8) 1 ⊸ (A ⊸ A) (9) A ∧ B ⊸ A, A ∧ B ⊸ B (10) (A ⊸ B) ∧ (A ⊸ C) ⊸ (A ⊸ B ∧ C) (11) A ⊸ A ∨ B, B ⊸ A ∨ B (12) (A ⊸ C) ∨ (B ⊸ C) ⊸ (A ∨ B ⊸ C) (13) A⊸⊤ (14) ⊥⊸A (15) ∀x.A ⊸ A[x/t] (16) A[x/y] ⊸ ∃x.A 規則 ⊸ -Rule A, A ⊸ B ⇒ B ∧-Rule A, B ⇒ A ∧ B ∀-Rule B ⊸ A ⇒ B ⊸ ∀x.A (x < FV(B)) ∃-Rule A ⊸ B ⇒ ∃x.A ⊸ B (x < FV(B)) 指数結合子に 関する 公理 (17) B ⊸ (!A ⊸ B) (18) (!A ⊸ (!A ⊸ B)) ⊸ (!A ⊸ !B) (19) !(A ⊸ B) ⊸ (!A ⊸ !B) (20) !A ⊸ A (21) !A ⊸ !!A 指数結合子に 関する 規則 !-Rule A ⇒ !A. 21.
(28) 第3章. 証明構造. 第 2 章では、 3 つの証明体系を 定義し た。 こ こ では、 帰納的証明構造やプルーフ ネ ッ ト と 呼ばれる 、 グラ フ の形を し た 形式体系を 定義する 。 こ れは線形論理で使 われる 形式体系であ る 。 特に 断り がな い限り 、 こ の章では古典線形論理に ついて 言及する 。. 3.1 乗法線形論理に関する 証明構造 こ こ では乗法結合子に限定し た片側シーク エン ト 計算について 考え る 。 し たがっ て 、 ルールは以下のも のだけ から な る 。. p, ∼ p Ax Γ, A ∆, B ⋆ Γ, ∆, A ⋆ B. 1. 1 Γ, A, B + Γ, A + B. こ こ で以下の２ つの証明図を 見る 。 p, ∼ p Ax q, ∼ q Ax p ⋆ q, ∼ p, ∼ q ⋆ r, ∼ r Ax ⋆ (p ⋆ q) ⋆ r, ∼ p, ∼ q, ∼ r + (p ⋆ q) ⋆ r, ∼ p+ ∼ q, ∼ r. Γ 0 Γ, 0 Γ, A ∆, ∼ A Cut Γ, ∆. p, ∼ p Ax q, ∼ q Ax p ⋆ q, ∼ p, ∼ q ⋆ p ⋆ q, ∼ p+ ∼ q + r, ∼ r Ax ⋆ (p ⋆ q) ⋆ r, ∼ p+ ∼ q, ∼ r. こ れら の違いは規則の適用順序に し か無い。 こ のよ う な 違いし か無い証明図に 関 し て 、 プルーフ ネ ッ ト では同じ グラ フ を 得る こ と ができ る 。 ま た 、 証明図を 見て わかる よ う に シ ーク エン ト 計算では何度も 同じ 論理式を 記述し て いる が、 プルー フ ネ ッ ト ではこ のよ う な 冗長な 記述を 避け る こ と も でき る 。. 3.1.1 証明構造 初めに 、 証明構造を 定義する 。 証明構造は論理式に よ っ て ラ ベル付け さ れた ラ ベル付き 無向グラ フ であ る 。 証明構造は以下の６ つの構成要素から な る 。. 22.
(29) ax. p. ∼p. A. B cut. 1 A. 0 B. A. B. ⋆. +. A⋆B. A+B. 正確な 定義は以下で与え ら れる 。 定義 (証明構造 (proof structure)). f ormula を 論理式の集合と する 。 証明構造 α は、 ３ つ組 (Vα , E α , Lα ) から な る 無向 グラ フ である 。 Vα は節点の集合、 E α は辺の集合、 Lα : Vα −→ f ormula はラ ベルに 対する 関数の集合である 。 ま た、 証明構造の定義と 同時に 、 終節点 (terminal node) T N の定義も 行う 。 こ こ で、 α, β, · · · は証明構造を 表し 、 xA は節点 x が A でラ ベル 付け さ れて いる こ と を 表す。 公理 α = ({x1 , x2 }, {{x1, x2 }}, {(x1, p), (x2 , ∼ p)}) は証明構造である 。 こ のと き 、 T N(α) = {x1 , x2 } であ る 。. 1 規則 α = ({x}, ∅, {(x, 1)}) は証明構造であ る 。 こ のと き 、 T N(α) = {x} であ る 。 0 規則 α = ({x}, ∅, {(x, 0)}) は証明構造であ る 。 こ のと き 、 T N(α) = {x} であ る 。 結合規則 α, β が証明構造で、 Vα ∩ Vβ = ∅ な ら ば、 (Vα ∪ Vβ , E α ∪ E β , Lα ∪ Lβ ) も 証 明構造であ る 。 こ のと き の終節点は、 T N(α) ∪ T N(β) であ る 。 カ ッ ト 規則 α が証明構造で、 x1 A , x2 ∼A ∈ T N(α) な ら ば、 (Vα , E α ∪ {{x1 , x2 }}, Lα }) も 証明構造であ る 。 こ のと き の終節点は、 T N(α) \ {x1 , x2 } であ る 。. ⋆ 規則 α が証明構造で、 xA , yB ∈ T N(α) かつ z < Vα なら ば、 (Vα ∪{z}, E α∪{{x, z}, {y, z}}, Lα∪ {(z, A ⋆ B)}) も 証明構造である 。 こ のと き の終節点は、 (T N(α) ∪ {z}) \ {x, y} で ある 。 + 規則 α が証明構造で、 xA , yB ∈ T N(α) かつ z < Vα なら ば、 (Vα ∪{z}, E α ∪{{x, z}, {y, z}}, Lα∪ {(z, A + B)}) も 証明構造である 。 こ のと き の終節点は、 (T N(α) ∪ {z}) \ {x, y} で ある 。 以下のグラ フ が証明構造の例でであ る 。. 23.
(30) ax. p ∼p. ax. ax. q ∼q. r ∼r. ⋆. ⋆. ∼ p⋆q. ∼q⋆r +. (∼ p ⋆ q)+ ∼ r. 3.1.2 帰納的証明構造 先ほど 定義し た 証明構造の一部であ る 帰納的証明構造を 定義する 。 帰納的証明 構造はシ ーク エン ト 計算に 対応し て いる 。 帰納的証明構造は以下の要素から 構成 さ れる 。 こ こ から は α, β, · · · は証明構造ま たは帰納的証明構造を 表し 、 文脈に よ っ て 使い分け る 。. ax. p α. ∼p. 1. β A. α B. α β. A. α B. 0 β. A. B. ⋆. +. A⋆B. A⋆B. cut. 正確な 定義は以下で与え ら れる 。 定義 (帰納的証明構造 (inductive proof structure)). 帰納的証明構造 α は、 ３ つ組 (Vα , E α , Lα ) から な る 無向グラ フ であ る 。 こ こ でも 同 時に 終節点 T N を 定義する 。 公理 α = ({x1 , x2 }, {{x1, x2 }}, {(x1, p), (x2 , ∼ p)}) は帰納的証明構造である 。 こ のと き 、 T N(α) = {x1 , x2 } であ る 。. 1 規則 α = ({x}, ∅, {(x, 1)}) は帰納的証明構造であ る 。 こ のと き 、 T N(α) = {x} で ある 。 24.
(31) 0 規則 z < Vα であ る α が帰納的証明構造でな ら ば、 α′ = (Vα ∪ {z}, E α, Lα ∪ {(z, 0)}) も 帰納的証明構造であ る 。 こ のと き 、 T N(α′ ) = T N(α) ∪ {z} であ る 。 カ ッ ト 規則 α, β が帰納的証明構造で、 xA ∈ Vα かつ y∼A ∈ Vβ 、 Vα ∩ Vβ = ∅ な ら ば、 (Vα ∪ Vβ , (E α ∪ E β ) ∪ {{x, y}}, Lα ∪ Lβ }) も 帰納的証明構造であ る 。 こ のと き の 終節点は、 (T N(α) ∪ T N(β)) \ {x, y} であ る 。. ⋆ 規則 α, β が帰納的証明構造で 、 xA ∈ Vα かつ yB ∈ Vβ 、 Vα ∩ Vβ = ∅ な ら ば、 (Vα ∪Vβ ∪{z}, E α∪E β ∪{{x, z}, {y, z}}, Lα∪Lβ ∪{(z, A⋆B)}) も 帰納的証明構造である 。 ただし 、 z < Vα ∪Vβ である 。 こ のと き の終節点は、 (T N(α)∪T N(β)∪{z})\{x, y} であ る 。 + 規則 α が帰納的証明構造で、 xA , yB ∈ Vα かつ z < Vα な ら ば、 (Vα ∪ {z}, E α ∪ {{x, z}, {y, z}}, Lα ∪ {(z, A + B)}) も 帰納的証明構造である 。 こ のと き の終節点は、 (T N(α) ∪ {z}) \ {x, y} であ る 。 こ の帰納的証明構造はシーク エン ト 計算と 対応が取れる 。 定理. 以下は同値であ る 。. 1. MCLL ⊢ Γ ⇒ ∆ 2. T N(α) = {xA ∈ Vα | A ∈ Γ ∪ ∆} であ る 帰納的証明構造 α が存在する 。 証明.. 1 → 2 シーク エン ト 計算の構成に 関する 帰納法で簡単に 示すこ と ができ る 。 2 → 1 帰納的証明構造の構成に 関する 帰納法で簡単に 示すこ と ができ る 。 . 3.2 プルーフ ネッ ト と 帰納的証明構造 今度はグラ フ 的な 特徴に 着目し て 、 ど のよ う な 証明構造が帰納的証明構造であ る かを 見る 。 こ こ ら かは 0 と 1、 カ ッ ト 規則を 落と し て 、 ⋆ と + の結合子だけ に 制 限し た 論理に ついて 考え る 。. 25.
(32) 定義 (道標 (travel instructions for trip)). 証明構造 α に 対し て 、 道標 αt = (Vαt , Aαt ) を 定義する 。 Vαt は節点の集合、 Aαt は弧 の集合であ る 。 証明構造の節点 x は x ↑ と x ↓ に 分け ら れ、 辺も 2 本の有向辺に 分 け ら れる 。 公理 α = ({x1 , x2 }, {{x1 x2 }}, {(x1, p), (x2 , ∼ p)}) のと き 、 αt = ({x1 ↑, x1 ↓, x2 ↑, x2 ↓}, {(x1 ↑, x2 ↓), (x2 ↓, x2 ↑), (x2 ↑, x1 ↓), (x1 ↓, x1 ↑)}) で あ る 。 グラ フ は以下のよ う に な る 。. ↑. p. ↓. ↑ ∼p ↓. 1 規則 α = ({x}, ∅, {(x, 1)}) のと き 、 αt = ({x ↑, x ↓}, {(x ↑, x ↓), (x ↓, x ↑)}) であ る 。 グラ フ は以下のよ う に な る 。 ↑. 1. ↓. 0 規則 α = ({x}, ∅, {(x, 0)}) のと き 、 αt = ({x ↑, x ↓}, {(x ↑, x ↓), (x ↓, x ↑)}) であ る 。 グラ フ は以下のよ う に な る 。 ↑. 0. ↓. 結合規則 β, γ から 結合規則に よ っ て 、 α が導出さ れた と する 。 こ のと き 、 α の道標 αt は (Vβt ∪ Vγt , Aβt ∪ Aγt ) であ る 。. ⋆ 規則 T N(α′ ) = ΓL ∪ ∆R ∪ {xA , yB } であ る α′ に ⋆ 規則を 適用し て 、 T N(α′ ) = ΓL ∪ ∆R ∪ {zA⋆B} である α が導出さ れたと する 。 こ のと き 、 α の道標 αt は以下のど ち ら かであ る 。 • 左 αt = (Vα′ t ∪{z ↑, z ↓}, (Aα′ t ∪{(x ↓, z ↓), (z ↑, y ↑), (y ↓, x ↑), (z ↓, z ↑)})\{(x ↓, x ↑), (y ↓, y ↑)}) グラ フ は以下のよ う に な る 。. 26.
(33) α′ t ↑. A. ↓. ↑. B. ↓. ↑ A⋆B ↓ • 右 αt = (Vα′ t ∪{z ↑, z ↓}, (Aα′ t ∪{(x ↓, y ↑), (y ↓, z ↓), (z ↑, x ↑), (z ↓, z ↑)})\{(x ↓, x ↑), (y ↓, y ↑)}) グラ フ は以下のよ う に な る 。. α′ t ↑. A. ↓. ↑. B. ↓. ↑ A⋆B ↓ + 規則 T N(α′ ) = ΓL ∪ ∆R ∪ {xA , yB } であ る α′ に + 規則を 適用し て 、 T N(α) = ΓL ∪ ∆R ∪ {zA+B} である α が導出さ れたと する 。 こ のと き 、 α の道標 αt は以下のど ち ら かであ る 。 • 左 αt = (Vα′ t ∪ {z ↑, z ↓}, (Aα′ t ∪ {(z ↑, x ↑), (x ↓, z ↓), (z ↓, z ↑)}) \ {(x ↓, x ↑)}) グラ フ は以下のよ う に な る 。. α′ t ↑. A. ↓. ↑. ↑ A+B ↓. 27. B. ↓.
(34) • 右 αt = (Vα′ t ∪ {z ↑, z ↓}, (Aα′ t ∪ {(z ↑, y ↑), (y ↓, z ↓), (z ↓, z ↑)}) \ {(y ↓, y ↑)}) グラ フ は以下のよ う に な る 。. α′ t ↑. ↓. A. ↑. B. ↓. ↑ A+B ↓ 以下のグラ フ は、 先ほど の証明構造の例に 対する 道標の１ つであ る 。. ↓. p. ↑. ↓ ∼p ↑. ↓. q. ↑. ↓ ∼q ↑. ↓∼ p ⋆ q↑. ↓. r. ↑. ↓ ∼r ↑. ↓∼ q ⋆ r↑. ↓ (∼ p ⋆ q)+ ∼ r ↑. 定義. Ii , I j ∈ {↑, ↓} と する 。 こ のと き 、 AIi から BI j への旅路 (trip) と は、 AIi から BI j への道であ る 。 ま た 、 AIi から BI j への旅路の長さ と は、 旅路の途中で通っ た 辺の 数であ る 。 n 個の節点を 持つ証明構造に 対し て 、 あ る 道標の旅路の長さ が 2n であ る と き 、 こ の旅路は長旅 (longtrip) であ る と いう 。 そ し て 、 プルーフ ネ ッ ト と は、 証明構造の任意の道標に おけ る 旅路が長旅であ る 証明構造のこ と であ る 。 定理. 以下の２ つの条件は等し い。. 1. 証明構造が帰納的証明構造であ る 。 2. 証明構造の全て の旅路が長旅であ る 。 証明. 1 → 2 は帰納的証明構造に 関する 帰納法で簡単に 示すこ と ができ る 。. 28. .
(35) こ れから 2 → 1 を 示す。 初めに 、 長旅の条件を 変え る 。 + に 関する 辺のス イ ッ チ ン グと は、 以下のど ち ら かのよ う に 置き 換え た も ので ある 。. A. A. B. B. +. +. A+B. A+B. 正確な 定義は次の通り であ る 。 定義 (ス イ ッ チン グ ). 証明構造 α に 対し て 、 ス イ ッ チ ン グ σ = (Vσ , E σ , Lσ ) を 定義する 。 Vσ は節点の集 合、 E σ は辺の集合、 Lσ : Vσ −→ f ormula はラ ベルに 対する 関数の集合であ る 。 公理 α = ({x1 , x2 }, {{x1 x2 }}, {(x1, p), (x2 , ∼ p)}) のと き 、 σ = α であ る 。. 1 規則 α = ({x}, ∅, {(x, 1)}) のと き 、 σ = α であ る 。 0 規則 α = ({x}, ∅, {(x, 0)}) のと き 、 σ = α であ る 。 結合規則 β, γ から 結合規則に よ っ て 、 α が導出さ れた と する 。 こ のと き 、 β, γ そ れぞれのス イ ッ チン グを σβ , σγ と する と 、 σ は以下である 。. σ = (Vα , E σβ ∪ E σγ , Lα ) ⋆ 規則 T N(α′ ) = ΓL ∪ ∆R ∪ {xA , yB } であ る α′ に ⋆ 規則を 適用し て 、 T N(α′ ) = ΓL ∪ ∆R ∪ {zA⋆B} である α が導出さ れたと する 。 こ のと き 、 α′ のス イ ッ チン グを σ′ と する と 、 σ は以下であ る 。 σ = (Vα , E σ′ ∪ {(x, z), (y, z)}, Lα ) + 規則 T N(α′ ) = ΓL ∪ ∆R ∪ {xA , yB } であ る α′ に ⋆ 規則を 適用し て 、 T N(α) = ΓL ∪ ∆R ∪ {zA+B } である α が導出さ れたと する 。 こ のと き 、 α′ のス イ ッ チン グを σ′ と する と 、 σ は以下のど ち ら かであ る 。 • 左 σ = (Vα , E σ′ ∪ {(x, z)}, Lα ). 29.
(36) • 右 σ = (Vα , E σ′ ∪ {(y, z)}, Lα ) α を 証明構造と する 。 こ のと き 、 ２ 節点 x, y ∈ Vα に 対し て 道があ る ス イ ッ チ ン グが存在する と き 、 x ⌣ y と 書く 。 逆に 全て のス イ ッ チン グで２ 点間に 道が存在し な いと き 、 x 6⌣ y と 書く 。 以下が証明構造のス イ ッ チン グの例であ る 。. ax. p ∼p. ax. ax. q ∼q. r ∼r. ⋆. ⋆. ∼ p⋆q. ∼q⋆r +. (∼ p ⋆ q)+ ∼ r 次に 、 ス イ ッ チン グに 対する 道標を 定義する 。 証明構造に 対する 定義と は + 規 則に 関し て 違いがあ る 。 定義 (道標). ス イ ッ チン グ σ に 対し て 、 道標 σt = (Vσt , Aσt ) を 定義する 。 Vσt は節点の集合、 Aσt は弧の集合であ る 。 公理 σ = ({x1 , x2 }, {{x1 x2 }}, {(x1, p), (x2 , ∼ p)}) のと き 、 σt = ({x1 ↑, x1 ↓, x2 ↑, x2 ↓}, {(x1 ↑, x2 ↓), (x2 ↓, x2 ↑), (x2 ↑, x1 ↓), (x1 ↓, x1 ↑)}) で ある 。. 1 規則 σ = ({x}, ∅, {(x, 1)}) のと き 、 σt = ({x ↑, x ↓}, {(x ↑, x ↓), (x ↓, x ↑)}) であ る 。 0 規則 σ = ({x}, ∅, {(x, 0)}) のと き 、 σt = ({x ↑, x ↓}, {(x ↑, x ↓), (x ↓, x ↑)}) であ る 。 結合規則 ̺, ρ から 結合規則に よ っ て 、 σ が導出さ れた と する 。 こ のと き 、 σ の道標 σt は以下であ る 。. (V̺t ∪ Vρt , A̺t ∪ Aρt ). 30.
(37) ⋆ 規則 T N(σ′ ) = ΓL ∪ ∆R ∪ {xA , yB } で あ る σ′ に ⋆ 規則を 適用し て 、 T N(σ′ ) = ΓL ∪ ∆R ∪ {zA⋆B} であ る σ が導出さ れた と する 。 こ のと き 、 σ の道標 σt は以 下のど ち ら かであ る 。 • 左 σt = (Vσ′ t ∪{z ↑, z ↓}, (Aσ′ t ∪{(x ↓, z ↓), (z ↑, y ↑), (y ↓, x ↑), (z ↓, z ↑)})\{(x ↓, x ↑), (y ↓, y ↑)}) • 右 σt = (Vσ′ t ∪{z ↑, z ↓}, (Aσ′ t ∪{(x ↓, y ↑), (y ↓, z ↓), (z ↑, x ↑), (z ↓, z ↑)})\{(x ↓, x ↑), (y ↓, y ↑)}) 左+ 規則 T N(σ′ ) = ΓL ∪ ∆R ∪ {xA , yB } であ る σ′ に 左 + 規則を 適用し て 、 T N(σ) = ΓL ∪ ∆R ∪ {zA+B} であ る σ が導出さ れた と する 。 こ のと き 、 σ の道標 σt は以 下であ る 。. σt = (Vσ′ t ∪ {z ↑, z ↓}, (Aσ′ t ∪ {(z ↑, x ↑), (x ↓, z ↓), (z ↓, z ↑)}) \ {(x ↓, x ↑)}) 右 + 規則 T N(σ′ ) = ΓL ∪ ∆R ∪ {xA , yB } であ る σ′ に 右 + 規則を 適用し て 、 T N(σ) = ΓL ∪ ∆R ∪ {zA+B} であ る σ が導出さ れた と する 。 こ のと き 、 σ の道標 σt は以 下であ る 。. σt = (Vσ′ t ∪ {z ↑, z ↓}, (Aσ′ t ∪ {(z ↑, y ↑), (y ↓, z ↓), (z ↓, z ↑)}) \ {(y ↓, y ↑)}). ス イ ッ チン グを 用いて 証明構造の全て の旅路が長旅であ る と いう 条件と 同値な 条 件を 示す。 定義. 道が v, · · · , vi , · · · , v j (v1 = v j , vi ) である と き 、 閉路と いう 。 グラ フ が循環的 (cyclic) であ る と は、 閉路が存在する と き であ る 。 逆に 閉路が存在し な いと き 、 グ ラ フ は非循環的 (acyclic) であ る と いう 。 さ ら に 、 任意の２ つの節点の間に 道があ る グラ フ を 連結グラ フ と 呼ぶ。 補題. 以下の２ つの条件は等し い。. 1. 証明構造の全て の旅路が長旅であ る 。 2. 証明構造の任意のス イ ッ チン グに 対し て 、 非循環的かつ連結グラ フ であ る 。 証明.. 31.
(38) • 1→2 ある 証明構造が長旅である 旅路を 持つと き 、 連結グラ フ である 。 次に グラ フ が非循環的である こ と を 示す。 証明構造のス イ ッ チン グが循環的である と す る と 、 以下のよ う な 証明構造を 考え る こ と ができ る 。. ···. p ···. q ··· ∼ p ··· ∼ q ···. A⋆B. こ れら の道標に ついて 考え る と 、 以下のよ う な 道標が得ら れる 。. ···. ↑. p. ↓. ···. ↑. q. ↓ ···. ↑ ∼p ↓. ↑. A. ↓. ↑. B. ···. ↑ ∼ q ↓ ···. ↓. ↑ A⋆B ↓. 実線に 着目する と 、 明ら かに 長旅でな い旅路がある こ と が分かる 。 こ れは証 明構造の全て の旅が長旅である と いう 仮定と 矛盾する ので、 証明構造が長旅 な ら ば非循環的であ る 。. • 2→1 証明構造の構成に 関する 帰納法で示すこ と ができ る 。. . 32.
(39) 補題 (+ 除去). zA+B ∈ T N(α) かつ {xA , z}, {yB, z} ∈ E α を 満たす α がプルーフ ネ ッ ト な ら ば、 (Vα \ {z}, E α \ {{x, z}, {y, z}}, Lα \ {(z, A + B)}) も プルーフ ネ ッ ト であ る 。 証明. + 結合子に 関する ス イ ッ チン グの定義から 、 プルーフ ネ ッ ト から そ の + 結合 子の終節点に 関する 部分を 取り 除いて も 、 そ の証明構造のス イ ッ チ ン グは非循環 的かつ連結グラ フ であ る 。 し た がっ て 、 そ れも ま た プルーフ ネ ッ ト であ る 。 次に 、 A ⋆ B でラ ベル付け さ れた 終節点の除去に 関する 補題を 示す。 そ のた め に は様々 な 補題が必要であ る ので、 そ れら から 示す。 定義. x, y, z ∈ Vα を 満たす、 σ の道標 σt おいて 、 xIi から yI j ま での旅路の途中で zIk を 通る と き 、 zIk ∈ [xIi , yI j ]σ と 書く 。 た だし 、 Ii , I j , Ik ∈ {↑, ↓} と する 。 定義 (帝国 (empire)). x ∈ Vα であ る α を 証明構造、 α のス イ ッ チン グの集合を S (α) と する 。 任意のス イ ッ チン グ σ ∈ S (α) に 対し て 、 x ↓∈ [x ↑, x ↑]σ であ る x の帝国 e(x) は以下の条件を 満た す３ つ組 (Ve(x) , E e(x) , Le(x) ) から な る グラ フ であ る 。. • Ve(x) = {y ∈ Vα | ∀σ ∈ S (α).( y ↑, y ↓∈ [x ↑, x ↓]σ )} • E e(x) = {{y1 , y2 } ∈ E α | y1 , y2 ∈ Ve(x) } • Le(x) = {(y, A) ∈ Lα | y ∈ Ve(x) } 定理 (旅路定理 (trip theorem)). α を 証明構造、 S (α) を α のス イ ッ チン グの集合と す る 。 こ のと き 、 任意の x ∈ Ve(x) に 対し て 、 x ∈ {y ∈ Vα | y ↑, y ↓∈ [x ↑, x ↓]σ } を 満た すス イ ッ チン グ σ ∈ S (α) が存在する 。 証明. 証明構造の帰納法で示す。 基底段階. • 公理のと き x1 p , x2 ∼p と する 。 – x ≡ x1 のと き Ve(x1 ) = {x1 , x2 } で、 σt に おいて 旅路 x1 ↑, x2 ↓, x2 ↑, x1 ↓ であ る σ が存在 する 。 – x ≡ x2 のと き Ve(x2 ) = {x1 , x2 } で、 σt に おいて 旅路 x2 ↑, x1 ↓, x1 ↑, x2 ↓ であ る σ が存在 する 。 帰納段階. 33.
(40) • 最後に 結合規則で導出さ れた と き 証明構造 β, γ に結合規則を 適用し て 、 証明構造 α が構成さ れたと する 。 x ∈ Vβ と する と 、 任意の y ∈ Vγ に 対し て x < Ve(y) であ る 。 よ っ て 、 帰納法の仮定よ り 、 求める ス イ ッ チン グが存在する こ と が分かる 。 y ∈ Vγ に 対し て も 同様の 議論ができ る 。 • 最後に ⋆ 規則で導出さ れた と き 証明構造 β に ⋆ 規則が適用し て 、 証明構造 α が構成さ れたと する 。 新たに 追 加さ れた節点を x3 A⋆B と し 、 {x1 A , x3 }, {x2 B , x3 } ∈ E α と する 。 仮定よ り 、 α の任 意のス イ ッ チン グの道標に おいて 、 x ↑, · · · , x ↓, · · · , x ↑ な ので、 β に おいて Ve(x1 ) ∩ Ve(x2 ) = ∅ であ る 。 S (e(x1 )), S (e(x2 )) を そ れぞれ e(x1 ), e(x2 ) のス イ ッ チ ン グの集合、 x ∈ Vα と する 。 – x1 ∈ Ve(x) のと き x１ ∈ Ve(x) よ り 、 x3 ∈ Ve(x) であ る 。 さ ら に x2 ∈ Ve(x) な ので、 任意の y ∈ Ve(x2 ) に 対し て 、 y ∈ Ve(x) であ る 。 し た がっ て 、 τt に お いて 旅路 x ↑ , · · · , x1 ↓, x3 ↓, x3 ↑, x2 ↑, · · · , x2 ↓, x1 ↑, · · · , x ↓ を 持つ τ ∈ S (α) が存在す ればよ い。 帰納法の仮定よ り 、 任意の x′ ∈ Ve(x) に対し て、 x′ ∈ {y ∈ Vβ | y ↑ , y ↓∈ [x ↑, x ↓]σ } を 満たすスイ ッ チン グ σ ∈ S (e(x1 )) が存在する 。 すな わ ち 、 σt において Ve (x) の全て の要素を 含む旅路 x ↑, · · · , x1 ↓, x1 ↑, · · · , x ↓ が存在する 。 同様に 、 帰納法の仮定よ り 、 任意の y′ ∈ Ve(x2 ) に 対し て 、 y′ ∈ {y ∈ Vβ | y ↑, y ↓∈ [x2 ↑, x2 ↓]σ′ } を 満た すス イ ッ チン グ σ′ ∈ S (e(x2 )) が存在する 。 すな わち 、 σ′ t に お いて Ve (x2 ) の全て の要素を 含む 旅路 x2 ↑, · · · , x2 ↓ が存在する 。 故に 、 σ, σ′ を 保ち 、 x3 の ⋆ に 関する 辺に 対 し て 、 左 ⋆ 規則を 選択する よ う に τ を 取ればよ い。 – x2 ∈ e(x) のと き 上と 同様の議論から 示すこ と ができ る 。 – x1 , x2 < e(x) のと き 新たに 追加さ れた辺と は関係がな く 、 帰納法の仮定から 求める 旅路が得 ら れる 。 • 最後に + 規則で導出さ れた と き 証明構造 β に + 規則が適用さ れて 、 証明構造 α が構成さ れたと する 。 新たに 追加さ れた 節点を x3 A+B と し 、 {x1 A , x3 }, {x2 B , x3 } ∈ E α と する 。 S (β) は β のス イ ッ チン グの集合、 x ∈ Vα と する 。 – x1 ∈ Ve(x) かつ x2 < Ve(x) のと き 34.
(41) x2 < Ve(x) よ り 、 x3 < Ve(x) で あ る 。 し た がっ て 、 τt に お いて 旅路 x ↑ , · · · , x1 ↓, x1 ↑, · · · , x ↓ を 持つ τ ∈ S (α) が存在する ればよ い。 帰納法の 仮定よ り 、 任意の x′ ∈ Ve(x) に 対し て 、 x′ ∈ {y ∈ Vα | y ↑, y ↓∈ [x ↑, x ↓]σ } を 満たすスイッ チン グ σ ∈ S (β) が存在する 。 すなわち 、 σt において Ve (x) の全て の要素を 含む 旅路 x ↑, · · · , x1 ↓, x1 ↑, · · · , x ↓ が存在する 。 故に 、 σ を 保ち 、 x3 の + に 関する 辺に 対し て 、 右 + 規則を 選択する よ う に τ を 取ればよ い。 – x1 < Ve(x) かつ x2 ∈ Ve(x) のと き 上と 同様の議論から 示すこ と ができ る 。 – x1 , x2 ∈ Ve(x) のと き x1 , x2 ∈ Ve(x) よ り 、 x3 ∈ Ve(x) であ る 。 し た がっ て 、 τt に お いて 旅路 x ↑ , · · · , x1 ↓, x3 ↓, x3 ↑, x1 ↑, · · · , x2 ↓, x2 ↑, · · · , x ↓ を 持つ τ ∈ S (α) が存在 する ればよ い。 帰納法の仮定よ り 、 任意の x′ ∈ Ve(x) に 対し て 、 x′ ∈ {y ∈ Vβ | y ↑, y ↓∈ [x ↑, x ↓]σ } を 満た すス イ ッ チ ン グ σ ∈ S (β) が存在する 。 すな わち 、 σt に おいて Ve (x) の全て の要素を 含む旅路 x ↑, · · · , x1 ↓, x1 ↑ , · · · , x2 ↓, x2 ↑, · · · , x ↓ が存在する 。 故に 、 σ を 保ち 、 x3 の + に 関する 辺に 対し て 、 左 + 規則を 選択する よ う に τ を 取ればよ い。 帰納法の仮定 よ り 、 σt に お いて x ↑, · · · , x2 ↓, x2 ↑, · · · , x1 ↓, x1 ↑, · · · , x ↓ が得ら れた 場合も 同様の議論で求める 旅路が得ら れる 。 – x1 , x2 < Ve(x) のと き 新たに 追加さ れた辺と は関係がな く 、 帰納法の仮定から 求める 旅路が得 ら れる 。 補題. x3 B⋆C ∈ Vα かつ {x1 B , x3 }, {x2C , x3 } ∈ E α を 満た す α を プルーフ ネ ッ ト と する 。 任意のス イ ッ チン グ σ ∈ S (α) に おいて 、 y ∈ T N(α) が σt に おいて 旅路 x3 ↓, · · · , y ↓ , · · · , y ↑, · · · , x3 ↑ を 満た すな ら ば、 e(x1 ) ∪ e(x2 ) ⊆ e(y) であ る 。 証明. α がプルーフ ネ ッ ト であ る こ と と 帝国の定義から 、 e(x1 ), e(x2 ) ⊆ e(x3 ) であ る 。 ま た 、 仮定よ り e(x3 ) ⊆ e(y) であ る 。 よ っ て 、 e(x1 ) ∪ e(x2 ) ⊆ e(y) であ る 。 次に 、 証明構造 α を ２ つに 分け る こ と を 保証する 定理を 示す。 先ほど の + 除去の 補題の ⋆ 結合子に 関する 定理であ る 。 定理 (分裂定理 (splitting theorem)). 終節点に ⋆ 結合子の論理式でラ ベル付け さ れ た 節点が少な く と も １ つ存在し 、 + 結合子の論理式でラ ベル付け さ れた 節点がな. 35.
図
Outline
関連したドキュメント
2 つ目の研究目的は、 SGRB の残光のスペクトル解析によってガス – ダスト比を調査し、 LGRB や典型 的な環境との比較検証を行うことで、
このように資本主義経済における競争の作用を二つに分けたうえで， 『資本
被祝賀者エーラーはへその箸『違法行為における客観的目的要素』二九五九年）において主観的正当化要素の問題をも論じ、その内容についての有益な熟考を含んでいる。もっとも、彼の議論はシュペンデルに近
インドの宗教に関して、合理主義的・人間中心主義的宗教理解がどちらかと言えば中
例えば，立証責任分配問題については，配分的正義の概念説明，立証責任分配が原・被告 間での手続負担公正配分の問題であること，配分的正義に関する
例えば，立証責任分配問題については，配分的正義の概念説明，立証責任分配が原・被告 間での手続負担公正配分の問題であること，配分的正義に関する
ところが， [Taylor4] ( の最新版 ) に於いて改良されたテイラーのモジュラー性持ち上げ定理 ([Taylor4] 定理 5.4) に於いては， ρ v がスタインバーグ表現の際に
[CPS] Cogdell, J., and Piatetski-Shapiro, I., Remarks on Rankin-Selberg convolutions, in “Contri- butions to automorphic forms, geometry, and number theory,” Johns Hopkins Univ.
