Download presentation
1
東京工業大学 数理計算科学専攻 岩波 克 iwanami.s.aa@m.titech.ac.jp
直観主義フレーム上の古典論理 東京工業大学 数理計算科学専攻 岩波 克
2
目次 直観主義フレーム 直観主義フレーム上の古典論理 補足・今後の課題
3
直観主義論理 古典論理から排中律を抜いた論理 プログラムの型理論と相性がいい クリプキモデルやハイティング代数の意味論が知られる
A∨￢A、￢￢A→A、（A→B)∨（B→A)は真にならないことがある プログラムの型理論と相性がいい カリー・ハワード対応 クリプキモデルやハイティング代数の意味論が知られる
4
論理式 命題論理を考える 命題変数：可算個p,q,r,…… A,Bが論理式なら、A∧B、A∨B、￢A、A→Bも論理式
5
クリプキフレーム 反射推移性を持つ順序集合（W,R）
6
付値 直観主義のクリプキモデルは、クリプキフレーム（W,R）と付値Vの組（W,R,V） 各命題変数に対して、真となる世界の集合を遺伝性
w∈V(p)⇒(∀w’ wRw’⇒w’∈V(p)) を持つように定める。
7
遺伝性 p：真 q：真
8
付値の拡張（∧、∨） V(A∧B)＝V（A）∩V（B） V(A∨B)＝V（A）∪V（B） Ａ：真 Ｂ:真 Ａ∧Ｂ:真
Ａ：真 Ｂ:真 Ａ∧Ｂ:真 Ａ∧Ｂ:真 Ｃ:偽 (Ａ∧Ｂ)∨Ｃ:真
9
付値の拡張（→） V（A→B）＝｛a∈W;∀b aRb⇒(b∈V(A)⇒b∈V(B))｝ Ａ：真 Ｂ：真 Ａ：偽 Ａ：偽 Ｂ：偽 Ｂ：偽
Ａ：偽 Ｂ：偽 Ａ→Ｂ：真 Ａ：偽 Ｂ：偽 Ａ：真 Ｂ：真 Ａ：偽 Ｂ：偽 Ａ→Ｂ：偽
10
付値の拡張（￢） V(￢A)＝｛a∈Ｗ;∀b aRb⇒b∉V（A）｝ Ａ：偽 ￢Ａ：真 Ａ：偽
11
付値の拡張 V(A∧B)＝V（A）∩V（B） V(A∨B)＝V（A）∪V（B）
V（A→B）＝｛a∈Ｗ;∀b aRb⇒（b∈V（A）⇒b∈V（B）））｝ V（￢A）＝｛a∈Ｗ;∀b aRb⇒b∉V（A）｝ このように定義すると、論理式に関する遺伝性 w∈V(A)⇒∀w’ (wRw’⇒w’∈V(A)) が成り立つ。 (∀(W,R,V) V(A)=W)⇔論理式Aは直観主義で真 と定義する。
12
モデルの解釈の一例 クリプキモデル(W,R,V)の世界w∈Wで論理式Aが真ということを、「wで得ている知識（＝命題変数）でAが判明する」と解釈する。 ￢Aは、「これ以後どのように知識が増えても、Aとは分からない」と解釈する。 「時間が経てば知識は増える」というのが、命題変数の遺伝性。「知識が増えれば分かることも増えていく」というのが論理式の遺伝性。 特に、一点からなるクリプキモデル（＝古典論理のモデル）は知識が増えないモデルになる。
13
p∨￢p p
14
p∨￢p P∨￢p？ p
15
p∨￢p P∨￢p？ p ￢p
16
p∨￢p P∨￢p：偽 p ￢p
17
直観主義フレーム上の古典論理 では、直観主義クリプキフレームの立場から、古典論理を見るとどのように見えるだろうか？
直観主義フレームと命題変数に対する付値は同じにして、 「 (∀(W,R,V) V(A)=W) ⇔Ａは古典論理で真」 が成り立つようにＶの解釈を定めたい。
18
極大点を見る 極大点では、これ以上知識が増えることはないので、古典論理のモデルと変わらない。
よって、w∈Wの真偽を極大点（無限遠点）での真偽と一致するようにすれば、古典論理のモデルになる。 直観主義の付値Vを用いて、 V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))} とすればよい。
19
V’(p∨￢p)=W V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))} p
20
V’(p∨￢p)=W V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))} p ￢p
21
V’(p∨￢p)=W V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))} P∨￢p ￢p
22
V’(p∨￢p)=W V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))} P∨￢p p ￢p
23
V’の意味 極大元で成り立つ論理式の共通部分が全体で成り立つ。 p:真 P：偽
24
Pが真な付値でも偽な付値でも真となる論理式
V’の意味 極大元で成り立つ論理式の共通部分が全体で成り立つ。 Pが真な付値でも偽な付値でも真となる論理式 Pが真の古典論理の付値で真となる論理式 Pが偽の古典論理の付値で真となる論理式
25
V’の意味 V’(A)=V(￢￢A)なので、 「(∀(W,R,V) V’(A)=W)⇔Aが古典論理で真」 は、グリベンコの定理
「 ￢￢Aが直観主義で真⇔ Aが古典論理で真」 を意味している。
26
直観主義フレーム上の古典論理２ 次のように(W,R)上の付値V’’を定める。 命題変数については、Vと同様、遺伝性を持つように定める。
次のように論理式全体へ拡張する。 V’’(A∧B)＝V’’(A)∩V’’(B) V’’(￢A)＝{a∈W;∀b aRb⇒b∉V’’(A)} V’’(A∨B)＝{a∈W;∀b aRb⇒(∃c bRc∧(c∈V’’(A)またはc∈V’’(B)))} V’’（A→B）＝V’’(￢A∨B)
27
V’’(p∨￢p)=W P∨￢p p ￢p
28
補題 V(A)⊂V’’(A)⊂V’(A) Aの構成に関する帰納法で示せる。
任意の、フレーム(W,R)と命題変数の割り当てVに対して、V(A)⊂V’’(A)⊂V’(A)が成り立つ。 Aの構成に関する帰納法で示せる。 V(B)⊂V’’(B)⊂V’(B)、V(C)⊂V’’(C)⊂V’(C)のとき、V’’(A)は以下の通り。 V’’(B) V’’(Ｃ) V’’（A） A=B∧C V その他 不明（V⊂V’’⊂V’） V’ A=￢B 全て V=V’’=V’ A=B∨C
29
V’’は古典論理 (∀(W,R,V) V’’(A)=W)⇔Aは古典論理で真 を示す。
∀(W,R,V) （V’’(A)=W ⇐ V’(A)=W） を言えば良い。 Aの構成に関する帰納法 Aが変数のときは条件を満たすものはない。 A=B∨C、￢Bのときは補題の証明より成立
30
A=B∧Cのとき ∀(W,R,V) V’(B∧C)=W ⇔ ∀(W,R,V) (V’(B)=WかつV’(C)=W) ⇔ ∀(W,R,V) (V’’(B)=WかつV’’(C)=W)(ＩＨより) ⇔ ∀(W,R,V) (V’’(B∧C)=W) 以上より示せた。
31
動機 ∧と￢の断片では直観主義論理と古典論理が一致することが、このモデルを使うと一目で分かる。 p (p∨⊥)∧(￢p∨⊥) ￢P
V゜(A∨B)＝{a∈W;∃b aRb∧(b∈V’’(A)またはb∈V’’(B))} では論理式の遺伝性が成り立たず、古典論理にならない。 (p∨⊥)∧(￢p∨⊥) p ￢P
32
ＭＰ (W,R,V’’)では意味論よりMPが成り立つことがすぐには分からない。 A→B,A B
33
今後の課題 この性質を利用して面白い論理は作れないか？ 他の論理への拡張（直観主義二階命題論理など） 例えば、
V’’’(A∨B)=V(A∨B) V’’’(A→B)=V’’(A→B) とすると、MPが成り立たないが、公理化できるか？ （この例ではできない模様） 他の論理への拡張（直観主義二階命題論理など）
