Alloy でクリプキの可能世界意味論をエンコードしてみた記録。
論理学をきちんと勉強した訳じゃないので、もし誤りがあったら是非教えてください。
可能世界意味論と云うのは、偉大な論理学者ソール・クリプキが、なんと高校生の頃に思い付いた様相論理の意味論です。
様相論理って云うのは、通常の命題論理に、「□P (必然的に P)」とか「◇P (Pであることが可能)」と云う二つの記号を付け加えて出来る論理体系です。要は可能性を扱う論理学ですね！
ひとくちに様相論理と云っても色々種類があるそうで、「必然的にP なんだったらどう考えてもPだろうよ」「必然的にPであるためにはまずPが可能じゃないといけないんじゃね？」「必然から可能が必然だよな*1！」とかみんな色々な法則を提唱してるんだとか。みんながみんなオレオレ様相論理を作るので、それぞれが一体どういう関係にあるのか？とか、本当にそれで大丈夫なの？とか、混沌とした状態ですね。
そこに光明を齎したのが若き日のクリプキで、「可能世界同士の二項関係を考えればいいよな！」と云う一言で各体系の関係を綺麗に纏め上げてしまったのだそうです。すごい！
それがクリプキの可能世界意味論。平たく説明すると、
- 沢山の「可能な世界」の集合とその間の"到達"可能性を考える。
- ある世界 w で「P が必然的」であるとは、w から到達可能な全ての世界で P が成立すること
- 同様に「Pが可能」であるとは、w から到達可能な世界のうち少なくとも一つで P が成立すること
と云う考え方に基いています。到達可能性は世界同士の二項関係で、色々と提唱されてきた様相論理の公理は、二項関係が満たす性質と一対一に対応するよ、と云うのがクリプキの発見でした(ですよね？)。
例えば、反射律(a R a)と「必然的にPならP」と云う命題、推移律(a R b, b R c ⇒ a R c)「必然的にPなら必然的に『必然的にP』」と云う命題がそれぞれ対応していたりします。
と云う訳で、それを Alloy で書き下してみたのが以下のソースです。
module possibleworld
sig World {}
sig Atom {}
enum TruthValue { True, False }
sig KripkeFrame {
worlds : some World,
accessible: World -> World
}
abstract sig Formula {}
sig Atm extends Formula { atom : one Atom }
sig Neg extends Formula { var: one Formula }
sig Imp extends Formula { left, right: one Formula }
sig Nec extends Formula { var : one Formula }
sig Pos extends Formula { var : one Formula }
fact NoRecursiveFormula {
no iden & ^(Neg <: var + Nec <: var + Pos <: var + left + right)
}
sig Model {
frame : one KripkeFrame,
valuation: World -> Atom -> one TruthValue,
eval : World -> Formula -> one TruthValue
} {
(valuation.univ).univ in frame.worlds
(eval.univ).univ in frame.worlds
all w : frame.worlds {
all exp : Atm |
eval[w, exp] = valuation [w, exp.atom]
all exp : Neg |
eval[w, exp] = True <=> eval [w, exp.var] = False
all exp : Imp |
eval[w, exp] = True <=>
(eval [w, exp.left] = False or eval [w, exp.right] = True)
all exp : Nec |
eval [w, exp] = True <=>
all w' : frame.accessible[w] | eval [w', exp.var] = True
all exp : Pos |
eval [w, exp] = True <=>
some w' : frame.accessible[w] | eval [w', exp.var] = True
}
}
pred valid(m : Model, A : Formula) {
all w : m.frame.worlds | m.eval [w, A] = True
}
pred valid(f : KripkeFrame, A : Formula) {
all m : Model | (m.frame in f) => valid [m, A]
}
one sig atmP, atmQ in Atom {}
one sig P in Atm {} { atom in atmP }
one sig Q in Atm {} { atom in atmQ }
one sig NecP in Nec {} { var in P }
one sig NecQ in Nec {} { var in Q }
one sig PosP in Pos {} { var in P }
one sig PimpQ in Imp {} { left in P and right in Q }
one sig NecPimpQ in Nec {} { var in PimpQ }
one sig NecPImpNecQ in Imp {} { left in NecP and right in NecQ }
one sig K in Imp {} { left in NecPimpQ and right in NecPImpNecQ}
one sig D in Imp {} { left in NecP and right in PosP }
one sig T in Imp {} {left in NecP and right in P}
one sig NecNecP in Nec {} { var in NecP }
one sig Four in Imp {} { left in NecP and right in NecNecP }
one sig NecPosP in Nec {} { var in PosP }
one sig B in Imp {} { left in P and right in NecPosP }
one sig Five in Imp {} { left in PosP and right in NecPosP }
fact {some Model}
-- K : □(P → Q) → (□P → □Q)
assert Kは常に成立 {
all f : KripkeFrame | valid [f, K]
}
check Kは常に成立 for 5
-- D : □P → ◇P
assert Dとserialの同値性 {
all f : KripkeFrame |
(all w : f.worlds | some f.accessible [w]) <=> valid [f, D]
}
check Dとserialの同値性 for 5
-- T : □P → P
assert Tと反射律の同値性 {
all f : KripkeFrame |
iden in f.accessible <=> valid [f, T]
}
check Tと反射律の同値性 for 5
-- 4 : □P → □□P
assert Fourと推移律の同値性 {
all f : KripkeFrame | let r = f.accessible |
r.r in r <=> valid [f, Four]
}
check Fourと推移律の同値性 for 5
-- B : P → □◇P
assert Bと対称律の同値性 {
all f : KripkeFrame | let r = f.accessible |
~r in r <=> valid [f, B]
}
check Bと対称律の同値性 for 5
-- 5 : ◇P → □◇P
assert Fiveとユークリッド律の同値性 {
all f : KripkeFrame | let r = f.accessible |
valid [f, Five] <=>
all w, w', w'' : f.worlds |
w -> w' + w -> w'' in r => w' -> w'' in r
}
check Fiveとユークリッド律の同値性 for 5スコープを 5 までにしても、それぞれの assertion 反例は見付からないので、ちゃんと成立しているとみて良さそうですね！わいわい！
参考文献
可能世界意味論に関しては、この本の末尾の方をぱらぱら捲りながら書きました：
まだ読んでいる途中ですが、論理学の基礎から発展的な内容まで、1から丁寧に解説した self-contained な教科書です。語り口も軽妙で、読んでいると論理学って楽しいなあ、と云うのをしみじみと感じます。興味を持たれた方は是非。
