%% 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 *. % Implication => : prop -> prop -> prop. %infix right 8 =>. =>I : (A @ W -> B @ W) -> (A => B @ W). =>E : (A => B @ W) -> A @ W -> B @ W. % 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. % 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'. % XXX add negation % Structural Rules letcc : (A * W -> A @ W) -> A @ W. throw : A @ W -> (A * W -> C @ W'). %%% Sequent calculus true : prop -> world -> type. %name true T t. false : prop -> world -> type. %name false F f. # : type. % judgmental contra : true A W -> false A W -> #. % there must be at least some world around to test % totality in the implicational fragment -- otherwise % there is no possible world argument to xm (alternately, % we can add blockw below in anticipation of box/dia) % here : world. % 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 -> #). % 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 -> #. % admissibility of excluded middle (cut) xm : {A:prop} {W:world} (true A W -> #) -> (false A W -> #) -> # -> type. %mode xm +A +W +D +E -F. % 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). %%% Translation from natural deduction to sequent calculus. % G;D |- A @ W then G # D,A 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} % here's our block % think of this as the base case for the % assumption we're making. 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 (excluded middle) for natural deduction %% This is the price we pay for using A * W instead of hoas for conts % 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. % special: 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) %%% 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. % judgmental 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&. % x.\ldb y.\sthrow{\langle}x, y{\rangle} \sto up / ub \rdb N_2\, / ua \brdb N_1 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)). % letcc-free version % u : A=>B |- throw \x:A . [[ c:B. throw \unused:A.c to u / XXX ]](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, world and totality verification for our theorems. % 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).