c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../first-order/model_theory/universe.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%sig Kripke = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Universes %open.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder acc' : elem (world → world → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder acc : elem world -> elem world -> elem bool' = [v][w] acc' @ v @ w.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder exists_world : ded exists [x : elem world] true.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Base-Kripke : Base -> Kripke = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder o := elem (world → bool').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ded := [f] ded forall [w] f @ w eq 1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Prop-Kripke : MPL -> Kripke = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-Kripke.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ⇒ := [f][g] λ[w] (f @ w) ⇒ (g @ w).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Necessity-Kripke : Necessity -> Kripke = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-Kripke.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder □ := [f] λ[w] ∀[w'] (acc w w') ⇒ (f @ w').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view Possibility-Kripke : Possibility -> Kripke = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Base-Kripke.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ◇ := [f] λ[w] ∃[w'] (acc w w') ∧ (f @ w').
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view ML-Kripke : ML -> Kripke = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Prop-Kripke.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Necessity-Kripke.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include Possibility-Kripke.