Classical S5

From The Twelf Project
Jump to: navigation, search

This case study concerns the formalization of the modal logic Classical S5 in the particular way it is done in Distributed Control Flow with Classical Modal Logic (Murphy, Harper, Crary; CSL 2005). The natural deduction calculus C5 is a nonstandard variation on the "obvious" classical S5 natural deduction which we chose for its operational interpretation, so that it can be used as a programming language. In the Twelf code below we prove that that C5 is equivalent to the "obvious" S5 by proving it equivalent to a standard cut-free sequent calculus for classical S5.

Twelf excels for this kind of proof. The only difficulty is that the most natural definition of falsehood assumptions leads to a third-order relation, which Twelf's termination checker did not support at the time this code was developed. Instead, we have an explicit substitution theorem for such assumptions.

Natural deduction

%% Classical Judgmental S5
%% Tom Murphy VII
%% Thanks: Frank Pfenning and Jason Reed
%%  8 Apr 2004

world : type.                           %name world W w.
prop : type.                            %name prop A.


%%% Natural deduction

% truth assumptions and conclusions
@ : prop -> world -> type.              %name @ N.
%infix none 1 @.
% falsehood (continuation) assumptions
* : prop -> world -> type.              %name * X.
%infix none 1 *.

We have two judgments: A true @ W and A false * W. We abbreviate these to A @ W and A * W.

% Implication
=> : prop -> prop -> prop.
%infix right 8 =>.
=>I : (A @ W -> B @ W) -> (A => B @ W).
=>E : (A => B @ W) -> A @ W -> B @ W.

This is an intrinsic encoding: Derivations of well-formedness play the role of proof terms in the logic.

% Necessity
! : prop -> prop.
%prefix 9 !.
!I : ({o:world} A @ o) -> ! A @ W.
!E : ! A @ W -> A @ W.
!G : ! A @ W' -> ! A @ W.

% Possibility
? : prop -> prop.
%prefix 9 ?.
?I : A @ W -> ? A @ W.
?E : ? A @ W -> ({o:world} A @ o -> C @ W) -> C @ W.
?G : ? A @ W' -> ? A @ W.

There are two modal connectives: , written !A and , written ?A. These two connectives are expressed in a non-standard way. The introduction and elimination forms all take place at the same world, and we give mobility forms !G and ?G that allow us to move modal terms from world to world.

% Conjunction
& : prop -> prop -> prop.
%infix none 9 &.
&I : A @ W -> B @ W -> (A & B @ W).
&E1 : (A & B @ W) -> A @ W.
&E2 : (A & B @ W) -> B @ W.

% Falsehood
_|_ : prop.
_|_E : _|_ @ W -> C @ W'.

% Structural Rules

letcc : (A * W -> A @ W) -> 
             A @ W.

throw :     A @ W ->
        (A * W -> C @ W').

The calculus is classical, which we achieve by including letcc (which binds the current continuation) and throw (which throws an expression, perhaps remotely, to a continuation). There are no terms of falsehood type, except for variables u bound by letcc. Those are not represented explicitly because we use higher-order abstract syntax.

% here : world.

In order for some propositions to exist, we may wish to declare some world constant. Otherwise, our metatheorems may be vacuously true due to empty quantification. Alternatively, we choose to prove our metatheorems with respect to a (LF level) regular world where (object language) hypothetical worlds may occur in the context. See the declaration of blockw below.

Sequent calculus

%%% Sequent calculus

true  : prop -> world -> type.       %name true T t.
false : prop -> world -> type.       %name false F f.

# : type.

Sequents in the sequent calculus are represented by the judgment #, read as "contradiction." Sequents are derived in a context with true and false assumptions. For instance, the initial sequent says that if A is both true and false at the same world, then a contradiction arises:

% initial sequent
contra : true A W -> false A W -> #.

% arrow
=>T : 
      (false A W -> #)    ->    (true B W -> #)    ->
            (true (A => B) W -> #).
=>F :
      (true A W -> false B W -> #) ->
        (false (A => B) W -> #).


% box
!T :
      (true A W' -> #) ->
      (true (! A) W -> #).
!F :
      ({w:world} false A w -> #) ->
      (false (! A) W -> #).

% dia
?T :
      ({w:world} true A w -> #) ->
      (true (? A) W -> #).
?F :
      (false A W' -> #) ->
      (false (? A) W -> #).

Unlike the natural deduction, this presentation of the and connectives is completely standard.

% conjunction
&T :
      (true A W -> true B W -> #) ->
        (true (A & B) W -> #).
&F :
      (false A W -> #)   ->   (false B W -> #) ->
             (false (A & B) W -> #).                                 

% falsehood

_|_T : true _|_ W -> #.

Cut elimination

% admissibility of excluded middle (cut)

xm : {A:prop} {W:world} (true A W -> #) -> (false A W -> #) -> # -> type.
%mode xm +A +W +D +E -F.

Cut elimination for a classical sequent calculus is the law of the excluded middle: If in some ambient context, the assumption that A is true is contradictory, and the assumption that A is false is also contradictory, then the ambient context is also contradictory. The proof proceeds mostly like cut elimination for intuitionistic logic.

% initial cuts
xt_init : xm A W ([xt] contra xt D) ([xf] E xf) (E D).
xf_init : xm A W ([xt] D xt) ([xf] contra E xf) (D E).

% unused assumptions
xt_unused : xm A W ([x1] contra DT DF) E (contra DT DF).
xf_unused : xm A W D ([x1] contra ET EF) (contra ET EF).

% falsehood. actually falsehood is trivial because a principal
% cut is impossible, and the "commutative" cases aren't even inductive.
xd_ct_|_ : xm A W ([at] _|_T DD) _ (_|_T DD).
xe_ct_|_ : xm A W _ ([af] _|_T EE) (_|_T EE).

% commutative cases.
% note that we need to consider each rule in both D and E, so
% there are four cases for each connective.

% implication
xd_ct=> : xm A W ([at : true A W] =>T 
                  ([cf : false C W'] D1 at cf) 
                  ([dt : true D W'] D2 at dt) DD) ([af] E af)
               (=>T ([cf : false C W'] F1 cf) ([dt : true D W'] F2 dt) DD)
           <- ({cf : false C W'} xm A W ([at] D1 at cf) E (F1 cf))
           <- ({dt : true D W'}  xm A W ([at] D2 at dt) E (F2 dt)).

xe_ct=> : xm A W ([at] DD at) ([af : false A W] =>T 
                               ([cf : false C W'] E1 af cf)
                               ([dt : true D W'] E2 af dt) EE)
               (=>T ([cf] F1 cf) ([dt] F2 dt) EE)
           <- ({cf : false C W'} xm A W DD ([af] E1 af cf) (F1 cf))
           <- ({dt : true D W'}  xm A W DD ([af] E2 af dt) (F2 dt)).

xd_cf=> : xm A W ([at : true A W] =>F
                  ([ct : true C W'] [df : false D W'] D' at ct df) DD)
               ([af : false A W] E af)
               (=>F ([ct : true C W'][df : false D W'] F ct df) DD)
           <- ({ct : true C W'} {df : false D W'}
                 xm A W ([at] D' at ct df) E (F ct df)).

xe_cf=> : xm A W ([at : true A W] DD at)
               ([af : false A W] =>F
                  ([ct : true C W'] [df : false D W'] E' af ct df) EE)
               (=>F ([ct : true C W'][df : false D W'] F ct df) EE)
           <- ({ct : true C W'} {df : false D W'}
                 xm A W DD ([af] E' af ct df) (F ct df)).

% box
xd_ct! : xm A W ([at : true A W] !T ([bt : true B W'] D1 at bt) DD)
                ([af] E af)
                (!T ([bt : true B W'] F1 bt) DD)
          <- ({bt : true B W'} xm A W ([at] D1 at bt) E (F1 bt)).

xe_ct! : xm A W ([at] D at) 
                ([af : false A W] !T ([bt : true B W'] E1 af bt) EE)
                (!T ([bt : true B W'] F1 bt) EE)
          <- ({bt : true B W'} xm A W D ([af] E1 af bt) (F1 bt)).

xd_cf! : xm A W ([at : true A W] !F ([w][bf : false B w] D1 at w bf) DD)
                ([af] E af)
                (!F ([w][bf] F1 w bf) DD)
          <- ({w : world}{bf : false B w}
                xm A W ([at] D1 at w bf) E (F1 w bf)).

xe_cf! : xm A W ([at] D at)
                ([af] !F ([w][bf : false B w] E1 af w bf) EE)
                (!F ([w][bf] F1 w bf) EE)
          <- ({w}{bf} xm A W D ([af] E1 af w bf) (F1 w bf)).

% dia
xd_ct? : xm A W ([at : true A W] ?T ([w][bt] D1 at w bt) DD)
                ([af] E af)
                (?T ([w][bt] F1 w bt) DD)
          <- ({w}{bt} xm A W ([at] D1 at w bt) ([af] E af) (F1 w bt)).

xe_ct? : xm A W ([at] D at)
                ([af] ?T ([w][bt] E1 af w bt) EE)
                (?T ([w][bt] F1 w bt) EE)
          <- ({w}{bt} xm A W ([at] D at) ([af] E1 af w bt) (F1 w bt)).

xd_cf? : xm A W ([at] ?F ([bf : false B W'] D1 at bf) DD)
                ([af] E af)
                (?F ([bf] F1 bf) DD)
          <- ({bf} xm A W ([at] D1 at bf) ([af] E af) (F1 bf)).

xe_cf? : xm A W ([at] D at)
                ([af] ?F ([bf : false B W'] E1 af bf) EE)
                (?F ([bf] F1 bf) EE)
          <- ({bf} xm A W ([at] D at) ([af] E1 af bf) (F1 bf)).

% conjunction
xd_ct& : xm A W ([at] &T ([ct][dt] D1 at ct dt) DD)
                ([af] E af)
                (&T ([ct][dt] F1 ct dt) DD)
          <- ({ct}{dt} xm A W ([at] D1 at ct dt) ([af] E af) (F1 ct dt)).

xe_ct& : xm A W ([at] D at)
                ([af] &T ([ct][dt] E1 af ct dt) EE)
                (&T ([ct][dt] F1 ct dt) EE)
          <- ({ct}{dt} xm A W ([at] D at) ([af] E1 af ct dt) (F1 ct dt)).

xd_cf& : xm A W ([at] &F ([cf] D1 at cf) ([df] D2 at df) DD)
                ([af] E af)
                (&F ([cf] F1 cf) ([df] F2 df) DD)
          <- ({cf} xm A W ([at] D1 at cf) ([af] E af) (F1 cf))
          <- ({df} xm A W ([at] D2 at df) ([af] E af) (F2 df)).

xe_cf& : xm A W ([at] D at)
                ([af] &F ([cf] E1 af cf) ([df] E2 af df) EE)
                (&F ([cf] F1 cf) ([df] F2 df) EE)
          <- ({cf} xm A W ([at] D at) ([af] E1 af cf) (F1 cf))
          <- ({df} xm A W ([at] D at) ([af] E2 af df) (F2 df)).


% principal cuts. there is one case for each connective;
% a use of the true  rule on A in D, and
% a use of the false rule on A in E.

% implication
x_=> : xm (A => B) W
          ([it : true  (A => B) W] =>T ([af : false A W] D1 it af)
                                       ([bt : true  B W] D2 it bt) it)
          ([if : false (A => B) W] =>F ([at : true  A W]
                                        [bf : false B W] E1 if at bf) if)
          F
        <- ({at : true A W} {bf : false B W}
            xm (A => B) W ([it] =>T ([af : false A W] D1 it af) 
                                    ([bt] D2 it bt) it)
                          ([if] E1 if at bf) (E1' at bf))
        <- ({af : false A W}
            xm (A => B) W ([it] D1 it af)
                          ([if] =>F ([at][bf] E1 if at bf) if) (D1' af))
        <- ({bt : true B W}
            xm (A => B) W ([it] D2 it bt)
                          ([if] =>F ([at][bf] E1 if at bf) if) (D2' bt))
        <- ({bf : false B W}
            xm A W ([at : true A W] E1' at bf) 
	           ([af : false A W] D1' af) (F' bf))
        <- xm B W ([bt] D2' bt) ([bf] F' bf) F.

% box
x_! : xm (! A) W ([nt] !T ([at : true A W'] D1 nt at) nt)
                 ([nf] !F ([w][af : false A w] E1 nf w af) nf)
                 F
       <- ({w : world}{af : false A w}
           xm (! A) W ([nt] !T ([at] D1 nt at) nt) 
	              ([nf] E1 nf w af) (E1' w af))
       <- ({at : true A W'}
           xm (! A) W ([nt] D1 nt at) 
	              ([nf] !F ([w][af] E1 nf w af) nf) (D1' at))
       <- xm A W' ([at : true A W'] D1' at) 
	          ([af : false A W'] E1' W' af) F.

% dia

x_? : xm (? A) W ([nt] ?T ([w][at] D1 nt w at) nt)
                 ([nf] ?F ([af] E1 nf af) nf)
                 F
       <- ({w : world}{at : true A w}
           xm (? A) W ([nt] D1 nt w at) 
	              ([nf] ?F ([af] E1 nf af) nf) (D1' w at))
       <- ({af : false A W'}
           xm (? A) W ([nt] ?T ([w][at] D1 nt w at) nt) 
	              ([nf] E1 nf af) (E1' af))
       <- xm A W' ([at : true A W'] D1' W' at) ([af] E1' af) F.

% conjunction

x_& : xm (A & B) W ([&t] &T ([at][bt] D1 &t at bt) &t)
                   ([&f] &F ([af] E1 &f af) ([bf] E2 &f bf) &f)
                   F
       <- ({at}{bt} xm (A & B) W ([&t] D1 &t at bt) 
                                 ([&f] &F ([af] E1 &f af) 
				          ([bf] E2 &f bf) &f)
                                 (D1' at bt))
       <- ({af} xm (A & B) W ([&t] &T ([at][bt] D1 &t at bt) &t)
                             ([&f] E1 &f af)
                             (E1' af))
       <- ({bf} xm (A & B) W ([&t] &T ([at][bt] D1 &t at bt) &t)
                             ([&f] E2 &f bf)
                             (E2' bf))
       <- ({bt} xm A W ([at] D1' at bt) ([af] E1' af) (D1'' bt))
       <- (xm B W ([bt] D1'' bt) ([bf] E2' bf) F).


%block blockw : block {w : world}.
%block blockt : some {A : prop} {W : world} block {tt : true  A W}.
%block blockf : some {A : prop} {W : world} block {ff : false A W}.

%worlds (blockw | blockt | blockf) (xm A W D E F).

%total {A [D E]} (xm A W D E F).

Natural deduction to sequent calculus

The admissibility of excluded middle allows us to straightforwardly translate natural deduction proofs to sequent calculus proofs. The theorem we prove is that if Γ;Δ A @ W then Γ # A * W, Δ. Operationally, we can think of this as follows: if we have a program of type A, then we can pass the result of that program to a continuation expecting A to get a contradiction.

%%% Translation from natural deduction to sequent calculus.

% G;D |- A @ W    then   G # D,A * W
ndseq : A @ W -> (false A W -> #) -> type.
%mode ndseq +D -F.

% conjunction 

ns-&I : ndseq (&I D1 D2) (&F F1 F2)
         <- ndseq D1 F1
         <- ndseq D2 F2.

ns-&E1 : ndseq (&E1 (D1 : A & B @ W))
          ([af] F af)
          <- ndseq D1 ([&f] F2 &f)
          <- ({af} xm (A & B) W ([&t] &T ([at][bt] contra at af) &t) 
		                ([&f] F2 &f) (F af)).

ns-&E2 : ndseq (&E2 (D1 : A & B @ W))
          ([bf] F bf)
          <- ndseq D1 ([&f] F2 &f)
          <- ({bf} xm (A & B) W ([&t] &T ([at][bt] contra bt bf) &t) 
		                ([&f] F2 &f) (F bf)).


% falsehood

ns-_|_E : ndseq (_|_E (D1 : _|_ @ W))
	        ([af] F af)
	        <- ndseq D1 ([_|_f] F2 _|_f)
		<- ({af} xm (_|_) W ([_|_t] _|_T _|_t)
		                    ([_|_f] F2 _|_f) (F af)).

% implication

ns-=>I : ndseq (=>I ([a : A @ W] D a))
               ([=>f : false (A => B) W] 
		=>F ([at : true A W][bf : false B W] F at bf) =>f)
          <- ({a : A @ W}{at : true A W}
              ndseq a ([af] contra at af) -> 

              ndseq (D a) ([bf] F at bf)).

ns-=>E : ndseq (=>E D1 D2)
               ([bf] F bf)
          <- ndseq D1 ([if] F1 if)
          <- ndseq D2 ([af] F2 af)
          <- ({bf} xm (A => B) W 
                ([it] =>T ([af] F2 af) ([bt] contra bt bf) it)
                ([if] F1 if) (F bf)).

% box

ns-!I : ndseq (!I [w] D1 w) (!F [w][af : false A w] F w af)
         <- ({w} ndseq (D1 w) (F w)).

ns-!E : ndseq (!E D1) ([af] F af)
         <- ndseq D1 ([!f] F1 !f)
         <- ({af} xm (! A) W ([!t] !T ([at] contra at af) !t) 
                             ([!f] F1 !f) (F af)).

ns-!G : ndseq (!G D1) ([!f] F !f)
         <- ndseq D1 ([!f'] F1 !f')
         <- ({!f} xm (! A) W' 
               ([!t' : true (! A) W'] 
                  !F ([w'' : world][af'' : false A w''] 
                      (!T ([at'' : true A w''] contra at'' af'') !t')) !f)
               ([!f' : false (! A) W'] F1 !f')
               (F !f)).

% dia

ns-?I : ndseq (?I D) ([?f] ?F ([af] F af) ?f)
         <- ndseq D ([af] F af).

ns-?E : ndseq (?E D1 ([w : world][a : A @ w] D2 w a)) 
	      ([cf : false C W] F cf)
         <- ndseq D1 ([?f] F1 ?f)
         <- ({w' : world}{a : A @ w'}{at : true A w'} 
               % another use of our block
               ndseq a ([af] contra at af) ->
               ndseq (D2 w' a) ([cf] F2 w' at cf))
         <- ({cf : false C W} 
               xm (? A) W ([?t] ?T ([w][a] F2 w a cf) ?t)
                          ([?f] F1 ?f) (F cf)).

ns-?G : ndseq (?G D) ([?f : false (? A) W] F ?f)
         <- ndseq D ([?f' : false (? A) W'] F1 ?f')
         <- ({?f : false (? A) W}
               xm (? A) W'
               ([?t'] ?T ([w''][at''] ?F ([af''] contra at'' af'') ?f) ?t')
               ([?f'] F1 ?f')
               (F ?f)).

% we need a way of connecting nd continuation assumptions 
% with sequent false assumptions 
contfalse : A * W -> false A W -> type.
%mode contfalse +D -F.

% note contraction: F in output uses af twice
ns-letcc : ndseq (letcc ([ac] D ac)) ([af] F af af)
            <- ({ac : A * W} {af : false A W}
                  contfalse ac af ->
                  ndseq (D ac) (F af)).

% note weakening: [cf'] is unused.
ns-throw : ndseq (throw D K) ([cf'] F AF)
            <- ndseq D ([af] F af)
            <- contfalse K AF.

%block blockh : some {A:prop} {W:world}
               block {a : A @ W} {at : true A W} 
		     {_ : ndseq a ([af] contra at af)}.

%block block* : some {A:prop} {W:world}
               block {ac : A * W} {af : false A W} {_ : contfalse ac af}.

%worlds (blockw | blockh | block*) (contfalse D F).
%worlds (blockw | blockh | block*) (ndseq D F).

%total D (contfalse D F).
%total D (ndseq D F).

Continuation substitution

We must prove a substitution theorem for falsehood assumptions, because we did not use the most higher-order abstract syntax encoding for them. Nonetheless, the theorem is interesting. It says that if we have a term M with a hypothesis for a (true) term of type A, and we have a term N with a hypothesis for a (false) continuation expecting type A, then our substitution operation can substitute M into N to satisfy the hypothesis. M must be well-typed at all types and all worlds.

%% Continuation Substitution (excluded middle) for natural deduction

% if   G,x:A@W; D |- M : *
% and  G; D,u:A@W |- N : B
% then G; D       |- [[ x.M/u ]] N : B

xs : ({c}{w} A @ W -> c @ w) ->
     (A * W -> B @ W') ->
         (B @ W') -> type.                %name xs U.
%mode xs +D +E -F.

% trick: for any term closed wrt the continuation assumption,
%   substitution is the identity. This keeps us from having to
%   treat the case of @ variables, since they are always closed
%   wrt * variables. Without this trick, world subsumption forces
%   cases of xs to infect any later theorem that uses it!

xs-closed : xs D ([a*] E) E.

% falsehood

xs-_|_E : xs D ([u] _|_E (EE u)) (_|_E EE')
	   <- xs D EE EE'.

% conjunction

xs-&I : xs D ([u] &I (EA u) (EB u)) (&I F1 F2)
         <- xs D EA F1
         <- xs D EB F2.

xs-&E1 : xs D ([u] &E1 (E u)) (&E1 F)
	  <- xs D E F.

xs-&E2 : xs D ([u] &E2 (E u)) (&E2 F)
	  <- xs D E F.

% implication

xs-=>I : xs D ([u] =>I ([aw : A @ W] E aw u)) (=>I ([aw] F aw))
	  <- ({aw : A @ W} xs D (E aw) (F aw)).

xs-=>E : xs D ([u] =>E (DF u) (DA u)) (=>E FF FA)
	  <- xs D DF FF
	  <- xs D DA FA.

% box


xs-!I : xs D ([u : A * W] !I ([w] E u w)) (!I ([w] F w))
	 <- ({w : world} xs D ([u] E u w) (F w)).


xs-!G : xs D ([u] !G (E u)) (!G F)
	 <- xs D E F.

xs-!E : xs D ([u] !E (E u)) (!E F)
	 <- xs D E F.

% possibility

xs-?E : xs D ([u] (?E (E1 u) ([w][a] E2 w a u))) (?E F1 ([w][a] F2 w a))
	 <- xs D E1 F1
	 <- ({w:world}{aw: A @ w} 
	       xs D (E2 w aw) (F2 w aw)).

xs-?I : xs D ([u] ?I (E u)) (?I F)
	 <- xs D E F.

xs-?G : xs D ([u] ?G (E u)) (?G F)
	 <- xs D E F.

xs-letcc : xs D ([u] letcc ([v] E v u)) (letcc ([v] F v))
	 <- ({v : B * W'} xs D (E v) (F v)).

% throw to different cont
xs-throwmiss : xs D ([u] throw (E u) V) (throw F V)
	 <- xs D E F.

% when reaching the throw, pass the term we're throwing
% to D instead.
xs-throwhit  : xs D ([u] throw (E u) u) (D B W' F)
		<- xs D E F.

% world and totality decls come after seqnd, which uses xs.
% they infect each other somewhat, but the worlds decls for
% xs are not substantially different than if it is checked
% alone (there are just some extra unrelated additions)

Sequent calculus to natural deduction

With substitution defined, we can now translate sequent calculus proofs back into C5 natural deduction. The theorem we prove is that if Γ # Δ then ∀C. ∀ω. Γ; Δ C @ ω.

%%% Translation from Sequent Calculus to Natural Deduction

%       G # D     then   G ; D |- M : * 
seqnd :   #         -> ({a}{w} a @ w) -> type.  %name seqnd S.
truend :  true A W  -> A @ W -> type.           %name truend T t.
falsend : false A W -> A * W -> type.           %name falsend F f.
%mode seqnd +D -F.
%mode truend +D -F.
%mode falsend +D -F.


sn-contra : seqnd (contra AT AF) ([c : prop][w : world] throw A AC)
             <- truend AT A
             <- falsend AF AC.

% For each connective, the T side is easy -- it just corresponds to
% the elimination rule. The F side requires the "excluded substitution"
% theorem above, and is often quite tricky.

% falsehood

sn-_|_T : seqnd (_|_T FT) ([c][w] _|_E FT') <- truend FT FT'.

% conjunction

sn-&T : seqnd (&T ([at][bt] D at bt) T&) ([c][w] F (&E1 N&) (&E2 N&) c w)
         <- ({at}{a} 
		truend at a ->
             {bt}{b} 
		truend bt b ->
             seqnd (D at bt) ([c][w] F a b c w))
         <- truend T& N&.

sn-&F : seqnd (&F ([af] D1 af) ([bf] D2 bf) (F& : false (A & B) W))
	      FF
	 <- falsend F& N&
	 <- ({af}{a*} falsend af a* ->
             seqnd (D1 af) ([c][w] F1 a* c w))
         <- ({bf}{b*} falsend bf b* ->
             seqnd (D2 bf) ([c][w] F2 b* c w))
         <- ({cc}{ww}{b : B @ W}
	     xs ([c][w] [a] throw (&I a b) N&)
	        ([a*] F1 a* cc ww)
	        (F1' b cc ww))
	 <- ({cc : prop}{ww}
	     xs ([c][w] [b] F1' b c w)
	        ([b*] F2 b* cc ww)
	        (FF cc ww)).

% implication

% actually, implication is not just the elim rule, because
% classical implication is phrased differently.

sn-=>T : seqnd (=>T ([af : false A W] D1 af) ([bt] D2 bt) 
		    (T=> : true (A => B) W))
	       FF
	  <- truend T=> N=>
	  <- ({af}{a*} falsend af a* ->
	      seqnd (D1 af) ([c][w] F1 a* c w))
	  <- ({bt}{b} 
		truend bt b ->
              seqnd (D2 bt) ([c][w] F2 b c w))
	  <- ({cc}{ww}
		xs ([c][w] [a] (F2 (=>E N=> a) c w))
		   ([a*] F1 a* cc ww)
		   (FF cc ww)).

There are two ways to translate the =>F rule; we can avoid using letcc if we like. We give both, taking advantage of the fact that LF relations need not be deterministic functions.

% letcc-free version
% u : A=>B |- throw \x:A . [[ c:B. throw \unused:A.c to u / ... ]](IH) to u
sn-=>F : seqnd (=>F ([at : true A W][bf : false B W] D at bf) F=>)
	       ([c][w] throw (=>I [a] FZ a B W) N=> )
	  <- falsend F=> N=>
	  <- ({at}{a}  
		truend  at a  ->
              {bf}{b*} falsend bf b* ->
	      seqnd (D at bf) ([c][w] F1 a b* c w))
	  <- ({a : A @ W}
	      {cc}{ww}
		xs ([c][w] [b] throw (=>I [a-unused : A @ W] b) N=>)
		   ([b*] F1 a b* cc ww)
		   (FZ a cc ww)).
		

% also include simpler letcc version
% u : A=>B |- throw (\x:A . letcc v : b* in (IH) end) to u
sn-=>F-letcc : 
        seqnd (=>F ([at : true A W][bf : false B W] D at bf) F=>)
	      ([c][w] throw (=>I [a] letcc [b*] F1 a b* B W) N=>)
	  <- falsend F=> N=>
	  <- ({at}{a}  
		truend  at a  ->
              {bf}{b*} falsend bf b* ->
	      seqnd (D at bf) ([c][w] F1 a b* c w)).

% box

sn-!T : seqnd (!T ([at' : true A W'] D at') T!) ([c][w] F (!E (!G N!)) c w)
	 <- ({at'}{a'} 
	       truend at' a' ->
	     seqnd (D at') ([c][w] F a' c w))
	 <- truend T! N!.

% this is the only necessary letcc in the proof
% u : []A * w |- throw (box w'. letcc v:A*w' in (IH) end) to u
sn-!F : seqnd (!F ([w' : world][af : false A w'] D w' af) F!)
	      ([c][w] (throw (!I [w'] letcc ([a*'] F w' a*' A w')) N!))
	 <- falsend F! N!
	 <- ({w' : world}{af' : false A w'}{a*' : A * w'} 
	       falsend af' a*' ->
             seqnd (D w' af') ([c][w] F w' a*' c w)).

% dia

% x : ?A@w |- let dia  = getx in IH end
sn-?T : seqnd (?T ([w'][at] D w' at) T?)
	 ([c][w] ?E (?G N?) ([w'][a'] F w' a' c w))
	 <- truend T? N?
	 <- ({w'}{at : true A w'}{a' : A @ w'}
	       truend at a' ->
             seqnd (D w' at) ([c][w] F w' a' c w)).

sn-?F : seqnd (?F ([af'] D af') F?)
	 FF
	 <- falsend F? N?
	 <- ({af' : false A W'}{a*' : A * W'}
	       falsend af' a*' ->
             seqnd (D af') ([c][w] F1 a*' c w))
	 <- ({cc}{ww}
	       xs ([c][w] [a'] (throw (?G (?I a')) N?))
	          ([a*'] F1 a*' cc ww)
	          (FF cc ww)).

Finally, we can declare the worlds for our metatheorems and ask Twelf to check them:

% for xs
%block blocku : some {A : prop} {W : world}
		block {u : A * W}.

%block blocka : some {A : prop} {W : world}
		block {u : A @ W}.


% for seqnd
%block blocknt : some {A:prop} {W:world}
                 block {at:true A W} {a:A @ W} 
		  {t:truend at a}.
%block blocknf : some {A:prop} {W:world}
                 block {af:false A W} {a:A * W} {t:falsend af a}.

%block blockp : block {a:prop}.

%worlds (blockw | blocka | blocknt | blocknf | blocku | blockp) 
     (xs D E F) (seqnd D F) (truend D F) (falsend D F).

%total E (xs D E F).

%total (D T F) (seqnd D FF) (truend T N) (falsend F M).

All code from this case study. Twelf's output from this case study.


Read more Twelf case studies and other Twelf documentation.