2005/05/18 志村先生 # 前回までは、ヒルベルト流でやったが、今回は、ゲンツェン流 我々の目的 : 特定な命題論理式が恒真かどうかを判定する方法が欲しかった def A が恒真 <=> 任意の付値 v に対して v(A) = 1 # これまでは、以下の方法を学んでいる # 真偽表を使う # ヒルベルト流で証明 # 今回からは、 # ゲンツェン流で証明 # をやる 定義を少し書き換えると A が恒真 <=> 任意の付値 v に対して v(A) = 1 <=> 任意の付値 v に対して 「v(A) = 0 でない」 # この文は、よくない形 ( 『』の位置で意味が変る ) <=> v(A) = 0 となる v が存在しない # と書換えて、考えたらどうなるだろうか ? 例: A = ((p\and q)\imp r)\imp(p\imp r)\or(q\imp r) ここで v(A) = v(((p\and q)\imp r)\imp(p\imp r)\or(q\imp r)) = 0 となるような場合があるとしたら.. 真中の \imp に着目すると.. # \imp の真偽表から.. v((p\and q)\imp r)) = 1 v((p\imp r)\or(q\imp r))) = 0 が成立しないといけない。 # ここで、前半はおいておいて、後半に着目すると.. \or から v(p\imp r) = 0 v(q\imp r) = 0 これから、 v(p)=1, v(r)=0, v(q)=1 .. (*) が出てしまう。 # そこで、この条件を他の式 ( i.e. v((p\and q)\imp r)) = 1 ) に入れると、矛盾している ( 0 になる ) ことから、このような v が存在しないことがわかってしまうのだが.. # 今度は、視点をかえて、最初の式の上 ( v((p\and q)\imp r) ) を考える v((p\and q)\imp r) = 1 より v(p\and q)=0 または v(r)=1 v(p\and q)=0 より v(p)=0 または v(q)=0 つまり、 v(r)=1 .. (1) v(p)=0 .. (2) v(q)=0 .. (3) の何れか。 しかし、(1),(2),(3) のいずれの場合も、(*) に矛盾する ので、結局このような v が存在しない。 すなわち、A は恒真式 # このような仕組を、わかりやすく行うのが、資料の p.7 からの内容 まず、世界を二つ ( 恒真式と、恒偽式の世界 ) に分ける 縦線の左は真に、右は偽になる ( なってほしい.. ) ↓ 恒真 恒偽 | |((p\and q)\imp r)\imp(p\imp r)\or(q\imp r) | ↑ これが偽になって欲しい ((p\and q)\imp r) |(p\imp r)\or(q\imp r) |(p\imp r) |(q\imp r) p |r q |r | +---------------+-----------------------+ ← 場合分けがおきた | p\and q r | +-------+-------+ * ← 葉 | p |q * * 上記の図がタブロー ( tableau ) 図 def それぞれの葉に到る道の.. 左に現れる論理式全体を \Ganma 右に現れる論理式全体を \Delta としたときに \Ganma と \Delta に共通に現れる論理式がある ならば、 「この葉は閉じている」 と呼ぶ。 def 全ての葉が閉じているタブロー図を、「閉じたタブロー図」と呼ぶ タブロー図の書かた (資料 p.6 から..) # 注意: 資料の \or と \imp に誤り、以下に訂正 \or の図 | A \or B ↓ | A \or B | A | B A \or B | ↓ | A \or B --------+-------+ A | B | \imp の図 | A \imp B ↓ | A \or B A | B A \imp B | ↓ A \imp B | +-------+-------+ B | | A \not の図 | \not A ↓ | \not A A | \not A | ↓ \not A | | A == タブロー図を作成する ということは 元の式が偽になるような葉を探す という行為 => 全ての葉が閉じれば、元の波は偽にならない.. もし、ある葉が閉じていなければ、それはそれで意味がある def あるタブローの閉じていない葉 左に現れる論理式全体を \Ganma 右に現れる論理式全体を \Delta としたときに \Ganma と \Delta に現れる論理記号をもった論理式は どれもタブローを作る規則が適用されている ならば、 \Ganma → \Delta は「飽和している」と呼ぶ。 # 現在のタブロー図に現れるどの論理式に規則を適用しても、新しい論理式が生れない状態を指す。 [補題] \Ganma → \Delta が飽和しているとき、付値 v を次のように定める v(p) = 1 ( p \in \Ganma ) = 0 ( p \not\in \Ganma ) # p は、原始式(命題変数)であることに注意 # 「\Ganma → \Delta が飽和している」点がポイント このとき、 \Ganma または \Delta に現れる論理式 B に対して # ここでは、「一般の論理式 B 」であることに注意 v(B) = 1 ( p \in \Ganma ) = 0 ( p \in \Delta ) が成立する。 Q. 飽和していない場合は ? A. 沢山可能性がある 展開を途中までおこなっている状態であれば、常に飽和していない Q. 飽和してない場合でも、必ず飽和させることができるか ? A. Yes, この後、その話がでてきる ( 重要な補題 ) # もちろん、「閉じていないタブロー式」も沢山ある # ( 恒真でない式に対するタブロー図は、閉じないことになる ) [補題の証明] # 論理式 B に含まれる論理記号の個数に関する帰納法(構成に関する帰納法)による 1) B が命題変数 p の時 v(p) = 1 <=> p \in \Ganma v(p) = 0 <=> p \not \in \Ganma <=> p \in \Delta # where ( <= ) は 「\Delta \cap \Ganma = \phai」 であることを利用する 2) B が C \imp D の形の時 [B \in \Delta の場合] 図が飽和しているので、 | C \imp D C | D となっているはず、従って C, D の帰納法の仮定から v(C)=1, v(D)=0 よって、 v(B)=v(C \imp D)= v(C)=>v(D) = 1=>0 = 0 [B \in \Ganma の場合] 図が飽和しているので、 C \imp D | +-------+-------+ D | |C よって、場合わけ [D \in \Ganma の場合] 帰納法の仮定より v(D)=1 v(B)=v(C\imp D)= v(C)=>v(D) = v(C) => 1 = 1 [C \in \Delta の場合] 帰納法の仮定より v(C)=0 v(B)=v(C\imp D)= v(C)=>v(D) = 0 => v(D) = 1 [補題] どんなタブローも、さらにタブローを作る規則を適用して、 どの葉も次の条件うち一方を満すようにできる 閉じている 飽和している # 別の言葉で言うと... # 閉じてもいないし飽和もしていない葉が存在できないようにできる # ということ ## [注意] 規則を適用すれば展開はできる可能性がある ( 飽和してない.. ) ## しかし、閉じている葉が展開できないわけではない ## 経路の中の左右に同じ式ができたらそこで閉じるので、それ以上、展開する必要がないから... [証明] # タブローを作る規則を、適用されていない論理式に含まれる論理記号の総数は、規則を適用することで ( 論理記号の個数は.. ) 減る。 => タブローを作るという操作は、有限回で終る # 暗黙の内に一つのタブロー内の式に適用できる適用規則が有限個であることを利用している # より一般的に、「枝の幅と深さの有限な木は、有限の葉しかない」 [定理] 論理式 A が与えられたとする | A にタブローを作る規則を適用してゆくと次のいずれかが起きる 飽和した葉が現れる 閉じたタブローができる 「飽和した葉が現れる」場合 飽和した葉から作られる \Ganma → \Delta において A \in \Delta であり、先程の補題でつくった付値 v に関して v(A) = 0 となる。 「閉じたタブローができる」場合 A は恒真になる # .. はずだが.. ## タブローの作り方によって、最終的なタブロー図の形は違う ## 閉じたタブロー図がどのような形になるかを調べないと、この図から、「A が恒真」というのは難しい # 閉じたタブロー図を扱うには、タブロー図の左 ( 恒真になって欲しい式のリスト ) と、タブロー図の右 ( 恒偽となっている欲しい式のリスト ) を上手くあつかう仕組が欲しい ## このような形を扱うためのに、ゲンツェン流の記法を利用する ( べつにゲンツェン流を使わなければならない理由はないが、まあ、この講議では、「こうしよう」ということ.. == [ゲンツェン流] \Ganma, \Delta : 論理式の列 \Ganma → \Delta : sequent (シークエント) と呼ぶ # sequent は造語で、辞書にはない def v を勝手な付値とするときに v(\Ganma → \Delta) を次のように定義する v(\Ganma → \Delta) = 1 (A \in \Ganma で v(A)=0 となるものがある か B \in \Delta で v(B)=1 となるものがある ) = 0 (それ以外) # 注意: \Ganma, \Delta は空列も許す def 任意の v に対して v(\Ganma → \Delta) = 1 となるとき、 \Ganma → \Delta は「恒真」であるという 例 v(A) = 1 <=> v(→A) = 1 例 ( 恒真な sequent の例 ) A, \Ganma → \Delta, A [Prof] [v(A)=1 となる v の時] A は \Delta, A に現れるので v(A, \Ganma → \Delta, A) = 1 [v(A)=0 となる v の時] A は A, \Ganma に現れるので v(A, \Ganma → \Delta, A) = 1 # この話は、「タブローの閉じた葉から作られる sequent は恒真」ということを意味する == [連絡事項] Mathematica の Version up / License が欲しいかた ( ただし、大学からかりている Note-PC への Install に限る ) は、志村先生 ( か、栗野.. ) に問い合わせてください。