論理とは何か 2007/4/6 01 構成 ﻪ第一部 ﻩ論理体系の導入 ﻩcut除去定理 ﻪ第二部 ﻩ新しい論理体系への拡張 ﻩcut除去定理の成立条件 ﻪ結論 02 論理とは何か ﻪ論理的なもの ﻩ日常生活における論理的思考 ﻩ数学における証明過程 ﻩプログラムの動き ﻪ論理的な部分だけ取り出したい 03 例1.日常生活における論理 ﻪ例 ﻩ暖冬ならば雪が少ない ﻩ雪が少ないならばスキー場が困る ﻩよって、暖冬ならばスキー場が困る ﻪ一般化 ﻩ仮定: 「AならばB」と「BならばC」 ﻩ結論: 「AならばC」 04 例2.数学における論理 ﻪ例 ﻩ辺の長さが3,4,5ならば、三平方の定理を満たす ﻩ三平方の定理を満たすならば、直角三角形 ﻩよって、辺の長さが3,4,5ならば、直角三角形 ﻪ一般化 ﻩ仮定: 「AならばB」と「BならばC」 ﻩ結論: 「AならばC」 05 例3.プログラムにおける論理 ﻪ例 プログラム1 文字列S 整数n プログラム2 文字列S Yes or No ﻪ一般化 ﻩ仮定: 「AからB」と「BからC」 ﻩ結論: 「AからC」 06 論理体系LK 推論規則 Γ ⇒ Δ,X,Y,Π (e右) Γ ⇒ Δ,Y,X ,Π Σ,X,Y,Γ ⇒ Δ(e左) Σ,Y,X,Γ ⇒ Δ Y, Γ ⇒ Δ,Y (→右) Γ ⇒ Δ,X→Y Γ ⇒ Δ,X Y,Σ⇒ Π (→左) X→Y,Γ,Σ ⇒ Δ,Π AΓ ⇒ ⇒Δ,X B X,Σ⇒ B ⇒Π C (cut) (cut) Γ,Σ A ⇒ Δ,Π C X,X,Γ ⇒ Δ (c左) X,Γ ⇒ Δ X, Γ ⇒ Δ (¬右) Γ ⇒ Δ,¬X Γ ⇒ Δ,X (¬左) ¬X,Γ ⇒ Δ Γ ⇒ Δ (w左) X,Γ ⇒ Δ Γ ⇒ Δ,X,X (c右) Γ ⇒ Δ,X Γ ⇒ Δ,X (∨右1) Γ ⇒ Δ,X∨Y Γ ⇒ Δ,Y (∨右2) Γ ⇒ Δ,X∨Y 上段が仮定、下段が結論 Γ ⇒ Δ (w右) Γ ⇒ Δ,X X,Γ ⇒ Δ Y,Γ⇒ Δ (∨左) X∨Y,Γ ⇒ Δ Y, Γ ⇒ Δ (∧左2) Γ ⇒ Δ,X Γ⇒ Δ,Y (∧右) X, Γ ⇒ Δ (∧左1) X∧Y,Γ ⇒ Δ Γ ⇒ Δ,X∧Y X∧Y,Γ ⇒Δ ギリシャ文字は0個以上の論理式の列を表す 仮定: 4月(X)ならば、春(Δ)だ A,B,C ⇒ D,E の意味は、 結論: 4月(X)かつ金曜日(Y)ならば、春(Δ)だ 「AかつBかつC」ならば「DまたはE」 仮定: 男性(Δ)または女性(X)だ 結論: 女性でない(¬X)ならば男性(Δ)だ 公理 X⇒X 07 証明図 ﻪド・モルガンの法則 ¬(A∨B)⇒¬A∧¬B A B A ⇒ A (∨左) B ⇒ B (∨左) A⇒A∨B B⇒A∨B (¬右) (¬右) ⇒¬A, A∨B (¬左) ⇒¬B, A∨B (¬左) ¬(A∨B)⇒¬A ¬(A∨B)⇒¬B (∧右) ¬(A∨B)⇒¬A∧¬B 論理的に正しい式を証明できる 08 証明図の自動生成 ﻪ証明図が作れるかどうかを自動的に調べたい ﻩ例:対偶 A⇒A (¬右) B ⇒ B (¬左) A→B ⇒ ¬B→¬A (→右) ¬B, B⇒ (→左) A⇒B ⇒A,¬A B⇒C(cut) 最後をcut規則 ¬B, A→B ⇒と仮定 ¬A (¬右) A⇒C ¬B ⇒ ¬A, ¬(A→B) (¬左) A→B ⇒ A→B (¬左) ¬(A→B), A→B ⇒ (¬右) ¬B, ¬¬(A→B) ⇒ ¬A (→右) ??? ¬¬(A→B) C∧BK ⇒¬¬(A→B) F∨¬D→E G→H L→M→N K ¬D→E F¬¬I ¬¬I J ⇒ A∨C∧G→H B∧J L→M→N A∧??? . A→B (cut) ¬B→¬A ﻪパターンが無限にある! ﻩcut規則のみの特徴 ﻩcut規則を取り除きたい 09 cut除去定理 ﻪG. Gentzen(1934) ﻩ証明図からcut規則を取り除くことができる ﻳこの分野で最も重要な定理の1つ ﻳ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なしの証明図のみ考えればよい (cut) ⇒ ¬¬(A→B) ¬B, A→B ¬¬(A→B) ⇒ ¬A ⇒ ¬B→¬A (cut) ﻳA→B パターンの数が減る A→B ⇒ ¬B→¬A ﻳ証明図があるかどうかを調べられる 010 . . . . . . 第一部のまとめ ﻪ推論規則の導入 ﻩ日常、数学、プログラムなどの論理を記号で表現 ﻪ論理体系LKの形成 ﻩ推論規則を集めて論理の体系を作る ﻪcut除去定理 ﻩcut規則は取り除くことができる ﻩ証明図の自動生成などに役立つ 011 構成 ﻪ第一部 ﻩ論理体系の導入 ﻩcut除去定理 ﻪ第二部 ﻩ新しい論理体系への拡張 ﻩcut除去定理の成立条件 ﻪ結論 012 新しい論理 ﻪ論理体系LK ﻩ最も古い論理 ﻩ通常「論理的」と言われる論理 ﻪその他の論理体系 ﻩ時間とともに真偽が変わる論理 ﻳ例:「今日は雨だ」 ﻩ背理法を認めない論理 ﻩ正しさだけでなく、ものの量も考える論理 ﻩ意味は特にない論理 013 様々な論理におけるcut除去定理 cut除去定理 ○ ○ ○ (1934年) FL FL LJcw 線形論理の部分体系 部分構造論理 直観主義論理 古典論理 LKMALL FL ec c X⇒X 公理 (1934年) 推論規則 X,X,Γ ⇒ Δ (c左) X,Γ ⇒ Δ (1980年代) Γ ⇒ Δ (w左) Γ⇒Δ X,Γ ⇒ Δ Γ ⇒ Δ,X (1980年代)Γ ⇒ Δ,X × (1980年代) Γ ⇒ Δ,X (∨右1) Γ ⇒ Δ,X∨Y (1980年代) X, Γ ⇒ Δ (∧左1) …… …… X∧Y,Γ ⇒ Δ Γ ⇒ Δ,X ¬X,Γ ⇒ Δ その差は何か ? Γ ⇒ Δ,X Σ,X,Y,Γ ⇒ Δ(e左) (w右) × ○ Γ ⇒ Δ,X,X (c右) (¬左) Γ ⇒ Δ,X,Y,Π (e右) Γ ⇒ Δ,Y,X ,Π Γ ⇒ Δ,X Y,Σ⇒ Π (cut) Σ,Y,X,Γ ⇒ Δ 体系を一般化 Y,Σ⇒ Π (→左) X→Y,Γ,Σ ⇒ Δ,Π Γ ⇒ Δ,Y Γ ⇒ Δ,X∨Y (∧左2) X∧Y,Γ ⇒ Δ X, Γ ⇒ Δ Γ ⇒ Δ,¬X (¬右) Y, Γ ⇒ Δ,Y (→右) Γ ⇒ Δ,X→Y (∨右2) Y, Γ ⇒ Δ Γ,Σ ⇒ Δ,Π X,Γ ⇒ Δ Y,Γ⇒ Δ (∨左) cut除去が成り立つ X∨Y,Γ ⇒ Δ ための条件を与えたい Γ ⇒ Δ,X Γ⇒ Δ,Y (∧右) Γ ⇒ Δ,X∧Y X,Y ,Γ ⇒ Δ (*左) X*Y,Γ ⇒ Δ など 「⇒」の右には高々1つ 014 cut除去定理の成立条件 ﻪA.Ciabattoni, K.Terui (2006) ﻩ体系Lが還元性と代入性を満たす ⇒ Lでcut除去定理が成り立つ ﻪW.Sakagawa(2007 情報科学科の卒論) ﻩCiabattoni, Teruiの結果を部分的に改良 ﻯcutをどのように除去するか、具体的に示した ﻯ扱える範囲を広くした 015 問題点とその解決方法 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⇒B A,C,A,C⇒D 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 C⇒B A⇒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を上げる方向を指定 . 016 第二部のまとめ ﻪLK以外の論理体系 ﻩ現在まで数え切れないほどの論理が考案されてきた ﻩcut除去定理の成り立つものとそうでないものがある ﻪcut除去定理の成立条件 ﻩ2つの条件が2006年に与えられた ﻩそれをもとに卒業論文を製作 ﻩcut除去の具体的な手順を示した 017 構成 ﻪ第一部 ﻩ論理体系の導入 ﻩcut除去定理 ﻪ第二部 ﻩ新しい論理体系への拡張 ﻩcut除去定理の成立条件 ﻪ結論 018 結論 ﻪ論理とは(1つの答え) ﻩ推論規則を用いて表現できるもの ﻩ体系ごとに論理があり、1つではない ﻪ他の答えについて ﻩぜひ情報科学科へ! 019 論理とは何か おしまい 020 主な参考文献 ﻩ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. 021 補足1.本質的cut除去 ﻪcut除去に次の2つの条件を追加 ﻯ公理を追加してもcutを除去可能 ﻯ論理階数が増えないようにcutを除去可能 ﻳ論理階数 … 証明図中の論理規則をあるルールで数えた数 ﻪ条件の由来 ﻯ1つ目の条件のみを課すものをmodular cut除去と呼ぶ ﻯ2つ目の条件は本研究でのみ扱われる条件 ﻬ文献よりも体系の一般化を進めたため、必要となった 022 補足2.通常のcut除去との関係 通常のcut除去 異質な体系 1. 条件を満たさない規則があるが、 その規則を使う機会のない体系 2. cutを除去することで無駄が増えるような体系 本質的cut除去 還元性と代入性 023 補足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の高さが一時的に低くなることもある 024 補足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) 025
© Copyright 2024 ExpyDoc