クリプキ可能世界意味論を、Alloy で。

possibleworld.als

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