Modally Propositional Logic

Modally-Propositional Logic

%sort world %.
%name world %.
%term world1 world %.
%term succ %pi world %-> world %.
%% so it doesn't split worlds, which makes the coverage checking output annoying
%block worldb {w world}%.
%worlds (worldb) (world) %.
%sort acc {_ world} {_ world} %.
%term refl acc W W %.
%term trans %pi (acc W1 W2) %-> (acc W2 W3) %-> (acc W1 W3) %.
%block accb [W1 _] [W2 _] {a acc W1 W2}%.
%worlds (worldb accb) (acc _ _) %.
%sort prop {_ world} %.
%name prop %.
%inline boxprop (%pi world %-> %type) [w] {w'} %pi (acc w w') %-> (prop w') %.
%term box %pi (boxprop W) %-> (prop W) %.
%term imp %pi (prop W) %-> (prop W) %-> (prop W) %.
%term at %pi (prop W') %-> (prop W) %.
%term down %pi (boxprop W) %-> (prop W) %.
%block propb [W world] {a prop W}%.
%worlds (worldb accb propb) (prop _) %.
%sort hyp {_ prop W} %.
%sort conc {_ prop W} %.
%term impL %pi (conc C) %<- (hyp (imp A B)) %<- (conc A) %<- (%pi (hyp B) %-> (conc C)) %.
%term impR %pi (conc (imp A B)) %<- (%pi (hyp A) %-> (conc B)) %.
%term atL %pi (conc C) %<- (hyp (at A)) %<- (%pi (hyp A) %-> (conc C)) %.
%term atR %pi (conc (at A)) %<- (conc A) %.
%term boxR %pi (conc (box (%the (boxprop W) A))) %<- ({w'} {a acc W w'} conc (A w' a)) %.
%term boxL {a acc W W'}
  %pi (conc C)
  %<- (hyp (box (%the (boxprop W) A)))
  %<- (%pi (hyp (A W' a)) %-> (conc C)) %.
%term downR %pi (conc (%the (prop W) (down A))) %<- (conc (A W refl)) %.
%term downL
  %pi (conc C)
  %<- (hyp (%the (prop W) (down A)))
  %<- (%pi (hyp (A W refl)) %-> (conc C)) %.
%block hypb [W _] [A prop W] {x hyp A}%.
%block prophypb [W _] {a prop W} {h %pi (hyp a) %-> (conc a)}%.
%worlds (worldb accb prophypb hypb) (hyp _) (conc _) %.
%sort id {A prop W} {_ %pi (hyp A) %-> (conc A)} %.
%mode id %in %out %.
%term _ %pi (id (imp A B) ([f] impR ([x] impL E' (E x) f))) %<- (id A E) %<- (id B E') %.
%term _
  %pi (id (box (%the (boxprop W) A)) ([b] boxR ([w'] [a] boxL a (E w' a) b)))
  %<- ({w} {a acc W w} id (A w a) (E w a)) %.
%term _
  %pi (id (down A) ([d] downR (downL (E _ refl) d)))
  %<- ({w} {a acc W w} id (A w a) (E w a)) %.
%% ambipolar:
% - : id (down A) ([d] downL ([x] downR (E _ refl x)) d)
%      <- {w} {a : acc W w} id (A w a) (E w a).
%term _ %pi (id (at A) ([a] atR (atL E a))) %<- (id A E) %.
%% ambipolar:
% - : id (at A) ([a] (atL ([x1] atR (E x1)) a))
%      <- id A E.
%block idcase [W _] {a prop W} {h %pi (hyp a) %-> (conc a)} {_ id a h}%.
%worlds (worldb accb idcase hypb) (id _ _) %.
%total A (id A _) %.
%sort ca {A} {_ conc A} {_ %pi (hyp A) %-> (conc C)} {_ conc C} %.
%mode ca %in %in %in %out %.
%term _
  %pi (ca _ (atR D) ([x] atL ([y] E x y) x) E'')
  %<- ({y} ca _ (atR D) ([x] E x y) (E' y))
  %<- (ca _ D E' E'') %.
%term _
  %pi (ca _ (boxR D) ([x] boxL A ([y] E x y) x) E'')
  %<- ({y} ca _ (boxR D) ([x] E x y) (E' y))
  %<- (ca _ (D _ A) E' E'') %.
%term _
  %pi (ca _ (downR D) ([x] downL ([y] E x y) x) E'')
  %<- ({y} ca _ (downR D) ([x] E x y) (E' y))
  %<- (ca _ D E' E'') %.
%term _
  %pi (ca (%the (prop WAB) (imp A B)) (impR D) ([x] impL ([y] E x y) (Arg x) x) (%the (conc (%the (prop WC) C)) E''))
  %<- ({y} ca (imp A B) (impR D) ([x] E x y) (E' y))
  %<- (ca (imp A B) (impR D) ([x] Arg x) Arg')
  %<- (ca A Arg' D D')
  %<- (ca B D' E' E'') %.
%% left commutative
%term _ %pi (ca _ (atL D D') E (atL D1 D')) %<- ({y} ca _ (D y) E (D1 y)) %.
%term _ %pi (ca _ (boxL A D D') E (boxL A D1 D')) %<- ({y} ca _ (D y) E (D1 y)) %.
%term _ %pi (ca _ (impL D A D') E (impL D1 A D')) %<- ({y} ca _ (D y) E (D1 y)) %.
%term _ %pi (ca _ (downL D D') E (downL D1 D')) %<- ({y} ca _ (D y) E (D1 y)) %.
%% right commutative
%term _ %pi (ca _ D ([x] impR ([y] E x y)) (impR F)) %<- ({y} ca _ D ([x] E x y) (F y)) %.
%term _ %pi (ca _ D ([x] atR (E x)) (atR F)) %<- (ca _ D ([x] E x) F) %.
%term _ %pi (ca _ D ([x] downR (E x)) (downR F)) %<- (ca _ D ([x] E x) F) %.
%term _
  %pi (ca _ D ([x] boxR ([w'] [a] E w' a x)) (boxR F))
  %<- ({w'} {a} ca _ D ([x] E w' a x) (F w' a)) %.
%term _
  %pi (ca _ D ([x] boxL A ([y] E x y) Y) (boxL A F Y))
  %<- ({y} ca _ D ([x] E x y) (F y)) %.
%term _
  %pi (ca _ D ([x] downL ([y] E x y) Y) (downL F Y))
  %<- ({y} ca _ D ([x] E x y) (F y)) %.
%term _ %pi (ca _ D ([x] atL ([y] E x y) Y) (atL F Y)) %<- ({y} ca _ D ([x] E x y) (F y)) %.
%term _
  %pi (ca _ D ([x] impL ([y] E x y) (Arg x) Y) (impL F Arg' Y))
  %<- ({y} ca _ D ([x] E x y) (F y))
  %<- (ca _ D ([x] Arg x) Arg') %.
%block capropb [W _] {a prop W} {init %pi (hyp a) %-> (conc a)} {_ {y hyp a} ca a (init y) init (init y)} {_ {W' world} {A prop W'} {D conc A} {y hyp a} ca A D ([_] init y) (init y)}%.
%% FIXME: this shouldn't pass:
%% propb is not equivalent to prophypb for hyp and conc.
%% does twelf only check world subsumption on subgoals?
%% %worlds (worldb | accb | propb | hypb) (ca _ _ _ _).
%worlds (worldb accb capropb hypb) (ca _ _ _ _) %.
%total {A D E} (ca A D E _) %.