シークエント計算の体系における cut除去定理の成立条件 2007/2/16 01 導入 ‫ ﻪ‬例 ‫ ﻩ‬ならば ‫ ﻩ‬傘が必要ならば荷物が増える ‫ ﻩ‬よって、雨ならば荷物が増える ‫ ﻪ‬一般化 ‫ ﻩ‬仮定 : 「 A ならば B 」と「 B ならば C 」 ‫ ﻩ‬結論 : 「 A ならば C 」 02 体系LK 公理 X⇒X 構造規則 Γ ⇒ Δ (w左) X,Γ ⇒ Δ X,X,Γ ⇒ Δ (c左) X,Γ ⇒ Δ Γ ⇒ Δ,X,X (c右) Γ ⇒ Δ,X Γ ⇒ Δ,X,Y,Π (e右) Γ ⇒ Δ,Y,X ,Π Σ,X,Y,Γ ⇒ Δ(e左) Σ,Y,X,Γ ⇒ Δ Γ ⇒ Δ (w右) Γ ⇒ Δ,X AΓ ⇒ ⇒Δ,X B X,Σ⇒ B ⇒Π C (cut) (cut) 論理規則 Γ,Σ A⇒ ⇒ Δ,Π C Γ ⇒ Δ,X Y,Σ⇒ Π (→左) X→Y,Γ,Σ ⇒ Δ,Π Γ ⇒ Δ,X (∨右1) Γ ⇒ Δ,X∨Y X, Γ ⇒ Δ (∧左1) X∧Y,Γ ⇒ Δ Γ ⇒ Δ,Y (∨右2) Γ ⇒ Δ,X∨Y Y, Γ ⇒ Δ,Y (→右) Γ ⇒ Δ,X→Y X,Γ ⇒ Δ Y,Γ⇒ Δ (∨左) X∨Y,Γ ⇒ Δ 上段が仮定、下段が結論 Y, Γ ⇒ Δ (∧左2) X∧Y,Γ ⇒ Δ Γ ⇒ Δ,X Γ⇒ Δ,Y (∧右) Γ ⇒ Δ,X∧Y Γ ⇒ Δ,X (¬左) ¬X,Γ ⇒ Δ X, Γ ⇒ Δ (¬右) Γ ⇒ Δ,¬X 03 cut除去定理 ‫ ﻪ‬G. Gentzen(1934) ‫ ﻩ‬LKのどの証明図に対しても、cut規則なしで同じ結論を持つものが存在する ‫ ﻳ‬数理論理学の最も重要な定理の１つ ‫ ﻳ‬cutの場所を上げていくことで証明 A⇒A (¬右) B ⇒ B (¬左) (¬右) (¬左) ⇒A,¬A (→右) ¬B, B⇒ (→左) (→左) ¬B, A→B ⇒ ¬A (¬右) (cut) (→右) ¬B ⇒ ¬A, ¬(A→B) (¬左)(cut) A→B ⇒ A→B (¬左) ¬(A→B), A→B ⇒ (¬右) ¬B, ¬¬(A→B) ⇒ ¬A (→右) ‫ ﻩ‬無駄のない証明図が作れる (cut) ⇒ ¬¬(A→B) ¬B, A→B ¬¬(A→B) ⇒ ¬A ⇒ ¬B→¬A (cut) ‫ﻳ‬A→B 変形途中でcutの数が増えることもあるが、最後には必ず cutなしの証明図が得られる A→B ⇒ ¬B→¬A 04 ‫ ﻩ‬例 . . . . . . 様々な体系におけるcut除去定理 cut除去定理 ○ ○ ○ × × ○ FL FL FL LJcw 線形論理の部分体系部分構造論理直観主義論理古典論理 LKMALL ec c X⇒X 公理 X,X,Γ ⇒ Δ (c左) 構造規則 X,Γ ⇒ Δ Γ⇒Δ Γ ⇒ Δ (w左) X,Γ ⇒ Δ (∧左1) X∧Y,Γ ⇒ Δ ¬X,Γ ⇒ Δ その差は何か ? Y,Σ⇒ Π (→左) Γ ⇒ Δ,Y (∨右2) Γ ⇒ Δ,X∨Y X, Γ ⇒ Δ (¬左) Γ ⇒ Δ,Y,X ,Π Γ ⇒ Δ,X Y,Σ⇒ Π (cut) Σ,Y,X,Γ ⇒ Δ X→Y,Γ,Σ ⇒ Δ,Π (∨右1) Γ ⇒ Δ,X,Y,Π (e右) 体系を一般化 (w右) Γ ⇒ Δ,X Γ ⇒ Δ,X∨Y Γ ⇒ Δ,X Γ ⇒ Δ,X Σ,X,Y,Γ ⇒ Δ(e左) Γ ⇒ Δ,X 論理規則 Γ ⇒ Δ,X Γ ⇒ Δ,X,X (c右) Y, Γ ⇒ Δ (∧左2) X∧Y,Γ ⇒ Δ X, Γ ⇒ Δ Γ ⇒ Δ,¬X (¬右) Γ,Σ ⇒ Δ,Π Y, Γ ⇒ Δ,Y (→右) cut除去が成り立つ Γ ⇒ Δ,X→Y ための必要十分条件 X,Γ ⇒ Δ Y,Γ⇒ Δ (∨左) X∨Y,Γ ⇒ Δ を与えたい Γ ⇒ Δ,X Γ⇒ Δ,Y (∧右) Γ ⇒ Δ,X∧Y X,Y ,Γ ⇒ Δ (＊左) X＊Y,Γ ⇒ Δ など「⇒」の右には高々１つ 05 A.Ciabattoni、照井(2006)による結果 L を任意の体系とする L で本質的cut除去が成立具体的な変型方法がわからない本研究の結果 L が意味論的に与えた条件を満たす変型方法がわかる十分性必要性 L が還元性と代入性を満たす十分性 06 還元性と代入性 ‫ ﻪ‬還元性 … 一段で消える論理記号を省くことが可能 ‫ ﻩ‬例「LKは還元性を満たす (記号∧についての例)」 A⇒B A⇒B A⇒C(∧右) B⇒D B⇒D (∧左) A⇒B∧C B∧C⇒D(cut) A⇒D (cut) ‫ ﻪ‬代入性…結論への代入は仮定への代入から導出可能 ‫ ﻩ‬例「LKは代入性を満たす (規則(c)の A に (X,Y) を代入した例)」 A,A⇒B (c) A⇒B X,Y, X,Y (e) X,X,Y,Y⇒B (c) X,Y,Y⇒B (c) X,Y 07 問題点とその解決方法 B⇒D (w) A⇒B C⇒B (min) B,B⇒D (c) B⇒D(cut) A,C⇒B A, C⇒D A⇒B C⇒B B⇒D A⇒BA,C⇒B C⇒B B,B⇒D B,B⇒D (2-cut) (cut) (2-cut) A,C,A,C⇒D A,C⇒B A,C, B⇒D(cut) A,C,A,C⇒D A, C⇒D C⇒D A,C,A,C⇒D A, . . . ‫ ﻩ‬問題点1. cutが高くならない ‫ ﻯ‬解決策. 拡張したn-cutを定義 Γ⇒X Σ1,X,Σ2,X,…,Σn,X,Σn+1,⇒Δ(n-cut) A⇒B C⇒B B⇒D (1-cut) B,B⇒D(2-cut) A,C⇒B A,C,A,C⇒D ‫ ﻩ‬問題点2. n-cutの仮定が増える A, C⇒D ‫ ﻯ‬解決策1. n-cutをさらに拡張(複数の仮定へ) Σ1,Γ,Σ2,Γ,…,Σn,Γ,Σn+1,⇒Δ ‫ ﻯ‬解決策2. cutを上げる方向を指定 . 08 まとめと今後の課題 ‫ ﻪ‬まとめ ‫ ﻯ‬本質的cut除去 ⇔ 還元性と代入性 ‫ ﻯ‬具体的な規則が不明でも変型方法を示すことができる ‫ ﻪ‬今後の課題 ‫ ﻯ‬さらなる一般化（様相論理なども扱える体系へ） ‫ ﻯ‬cut除去以外の定理への応用 09 主な参考文献 ‫ ﻩ‬A. Ciabattoni and K. Terui. "Towards a semantic characterization of cut-elimination". Studia Logica. Vol. 82(1). pp. 95 - 119. 2006. ‫ ﻩ‬A. Ciabattoni and K. terui. "Modular CutElimination: Finding Proofs or Counterexamples". Proceedings of Logic for Programming and Automated Reasoning (LPAR'2006), LNAI. Phnom Pehn, November 2006. 010 補足1.本質的cut除去 ‫ ﻪ‬cut除去に次の２つの条件を追加 ‫ ﻯ‬公理を追加してもcutを除去可能 ‫ ﻯ‬論理階数が増えないようにcutを除去可能 ‫ ﻳ‬論理階数 … 証明図中の論理規則をあるルールで数えた数 ‫ ﻪ‬条件の由来 ‫ ﻯ‬１つ目の条件のみを課すものをmodular cut除去と呼ぶ ‫ ﻯ‬２つ目の条件は本研究でのみ扱われる条件 ‫ ﻬ‬文献よりも体系の一般化を進めたため、必要となった 011 補足2.通常のcut除去との関係通常のcut除去異質な体系 1. 条件を満たさない規則があるが、その規則を使う機会のない体系 2. cutを除去することで無駄が増えるような体系本質的cut除去還元性と代入性 012 補足3. cut除去定理の証明方法 ‫ ﻪ‬変数の定義 ‫ ﻩ‬degree … cutされる論理式の複雑さ (≧ 0) ‫ ﻩ‬rank … cutされる論理式が出続ける高さ (≧ 2) ‫ ﻪ‬二重数学的帰納法 ‫( ﻩ‬d1, r1) > (d2, r2) ((d1 > d2) or (d1 = d2 and r1 > r2)) ‫ ﻳ‬例 (2,3) > (2,2) >(1,10)>(1,9)>…>(1,2)>(0,14)>…>(0,2) ‫ ﻩ‬この順序関係に対して数学的帰納法を適用 ‫ ﻳ‬cutの高さが一時的に低くなることもある 013 補足4. 一般化した体系公理構造規則 X⇒X Υ1 ⇒ Ψ1 … Υn ⇒ Ψn Θl, ★(X), Θr ⇒ Ξ Υ1 ⇒ Ψ1 … Υn ⇒ Ψn (R) Θ⇒Ξ 論理規則 Υ1 ⇒ Ψ1 … Υn ⇒ Ψn 左) Θ ⇒ Ξl, ★(X),Ξr (★ cut規則 Θ ⇒ Ξ1, X, Ξr Θl, X, Θr ⇒ Ξ Θl,Θ,Θr ⇒ Ξl,Ξ,Ξr (★右) (cut) 014