PPTX

Report
直観主義フレーム上の古典論理
東京工業大学 数理計算科学専攻
岩波 克
[email protected]
目次
• 直観主義フレーム
• 直観主義フレーム上の古典論理
• 補足・今後の課題
直観主義論理
• 古典論理から排中律を抜いた論理
– A∨¬A、¬¬A→A、(A→B)∨(B→A)は真にならな
いことがある
• プログラムの型理論と相性がいい
– カリー・ハワード対応
• クリプキモデルやハイティング代数の意味論
が知られる
論理式
• 命題論理を考える
– 命題変数:可算個p,q,r,……
– A,Bが論理式なら、A∧B、A∨B、¬A、A→Bも論理
式
クリプキフレーム
• 反射推移性を持つ順序集合(W,R)
付値
• 直観主義のクリプキモデルは、クリプキフレー
ム(W,R)と付値Vの組(W,R,V)
• 各命題変数に対して、真となる世界の集合を
遺伝性
w∈V(p)⇒(∀w’ wRw’⇒w’∈V(p))
を持つように定める。
遺伝性
p:真
p:真
p:真
p:真
p:真
p:真
p:真
p:真
q:真
q:真
q:真
q:真
付値の拡張(∧、∨)
• V(A∧B)=V(A)∩V(B)
• V(A∨B)=V(A)∪V(B)
A:真 B:真
A∧B:真
A∧B:真 C:偽 (A
∧B)∨C:真
付値の拡張(→)
• V(A→B)={a∈W;∀b aRb⇒(b∈V(A)⇒b∈V(B))}
A:真
A:偽 B:偽
A→B:真
A:真
B:真
B:真
A:真
A:偽
B:真
A:偽
B:偽
B:偽
A:偽
A:偽
B:真
B:真
A:真
A→B:偽
B:偽
付値の拡張(¬)
• V(¬A)={a∈W;∀b aRb⇒b∉V(A)}
A:偽
A:偽
¬A:真
A:偽
A:偽
A:偽
付値の拡張
•
•
•
•
V(A∧B)=V(A)∩V(B)
V(A∨B)=V(A)∪V(B)
V(A→B)={a∈W;∀b aRb⇒(b∈V(A)⇒b∈V(B)))}
V(¬A)={a∈W;∀b aRb⇒b∉V(A)}
• このように定義すると、論理式に関する遺伝性
w∈V(A)⇒∀w’ (wRw’⇒w’∈V(A))
が成り立つ。
• (∀(W,R,V) V(A)=W)⇔論理式Aは直観主義で真
と定義する。
モデルの解釈の一例
• クリプキモデル(W,R,V)の世界w∈Wで論理式A
が真ということを、「wで得ている知識(=命題
変数)でAが判明する」と解釈する。
– ¬Aは、「これ以後どのように知識が増えても、A
とは分からない」と解釈する。
– 「時間が経てば知識は増える」というのが、命題
変数の遺伝性。「知識が増えれば分かることも増
えていく」というのが論理式の遺伝性。
– 特に、一点からなるクリプキモデル(=古典論理
のモデル)は知識が増えないモデルになる。
p∨¬p
p
p∨¬p
p
P∨¬p?
p∨¬p
p
¬p
¬p
P∨¬p?
¬p
¬p
¬p
¬p
¬p
¬p
p∨¬p
p
¬p
¬p
P∨¬p:偽
¬p
¬p
¬p
¬p
¬p
¬p
直観主義フレーム上の古典論理
• では、直観主義クリプキフレームの立場から、
古典論理を見るとどのように見えるだろう
か?
• 直観主義フレームと命題変数に対する付値
は同じにして、
「 (∀(W,R,V) V(A)=W) ⇔Aは古典論理で真」
が成り立つようにVの解釈を定めたい。
極大点を見る
• 極大点では、これ以上知識が増えることはな
いので、古典論理のモデルと変わらない。
• よって、w∈Wの真偽を極大点(無限遠点)で
の真偽と一致するようにすれば、古典論理の
モデルになる。
– 直観主義の付値Vを用いて、
V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))}
とすればよい。
V’(p∨¬p)=W
V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))}
p
V’(p∨¬p)=W
V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))}
p
¬p
¬p
¬p
¬p
¬p
¬p
¬p
¬p
V’(p∨¬p)=W
V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))}
P∨¬p
P∨¬p
P∨¬p
¬p
P∨¬p
P∨¬p
¬p
¬p
P∨¬p
V’(p∨¬p)=W
V’(A)={a∈W;∀b aRb⇒∃c (bRc∧c∈V(A))}
p
¬p
¬p
¬p
¬p
P∨¬p
¬p
¬p
¬p
¬p
V’の意味
• 極大元で成り立つ論理式の共通部分が全体
で成り立つ。
p:真
P:偽
V’の意味
• 極大元で成り立つ論理式の共通部分が全体
で成り立つ。
Pが真の古典論理の付
値で真となる論理式
Pが真な付値でも偽な付値でも
真となる論理式
Pが偽の古典論理の付
値で真となる論理式
V’の意味
• V’(A)=V(¬¬A)なので、
「(∀(W,R,V) V’(A)=W)⇔Aが古典論理で真」
は、グリベンコの定理
「 ¬¬Aが直観主義で真⇔ Aが古典論理で真」
を意味している。
直観主義フレーム上の古典論理2
• 次のように(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)
V’’(p∨¬p)=W
p
¬p
¬p
¬p
¬p
P∨¬p
¬p
¬p
¬p
¬p
補題 V(A)⊂V’’(A)⊂V’(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)は以下の通り。
A=B∧C
V’’(B)
V’’(C)
V’’(A)
V
V
V
その他
不明(V⊂V’’⊂V’)
V’
V’
V’
A=¬B
全て
全て
V=V’’=V’
A=B∨C
全て
全て
V’
V’’は古典論理
• (∀(W,R,V) V’’(A)=W)⇔Aは古典論理で真
を示す。
– ⇒は一点からなるクリプキモデルを考えれば成立。
⇐を示す。Aが古典論理で真のとき、
• ∀(W,R,V) (V’’(A)=W ⇐ V’(A)=W)
を言えば良い。
– Aの構成に関する帰納法
• Aが変数のときは条件を満たすものはない。
• A=B∨C、¬Bのときは補題の証明より成立
• 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)(IHより)
⇔ ∀(W,R,V) (V’’(B∧C)=W)
以上より示せた。
動機
• ∧と¬の断片では直観主義論理と古典論理
が一致することが、このモデルを使うと一目で
分かる。
– V゜(A∨B)={a∈W;∃b aRb∧(b∈V’’(A)またはb∈V’’(B))}
では論理式の遺伝性が成り立たず、古典論理にならない。
p
(p∨⊥)∧(¬p∨⊥)
¬P
MP
• (W,R,V’’)では意味論よりMPが成り立つことが
すぐには分からない。
B
B
B
A→B,A
B
B
今後の課題
• この性質を利用して面白い論理は作れない
か?
– 例えば、
V’’’(A∨B)=V(A∨B)
V’’’(A→B)=V’’(A→B)
とすると、MPが成り立たないが、公理化できるか?
(この例ではできない模様)
• 他の論理への拡張(直観主義二階命題論理
など)

similar documents