Classical S5

This case study concerns the formalization of the modal logic Classical S5 in the particular way it is done in [http://www.cs.cmu.edu/~tom7/papers/csl05-19-distributed.pdf 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 STELF 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.

STELF 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 STELF’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
%sort world %.
%name world %.
%sort prop %.
%name prop %.
%%% Natural deduction
% truth assumptions and conclusions
%sort @ {_ prop} {_ world} %.
%name @ %.
%prec %none 1 @ %.
% falsehood (continuation) assumptions
%sort * {_ prop} {_ world} %.
%name * %.
%prec %none 1 * %.

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

% Implication
%term => %pi prop %-> prop %-> prop %.
%prec %right 8 => %.
%term =>I %pi (%pi (A @ W) %-> (B @ W)) %-> (A => B @ W) %.
%term =>E %pi (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
%term ! %pi prop %-> prop %.
%prec %prefix 9 ! %.
%term !I %pi ({o world} A @ o) %-> (! A @ W) %.
%term !E %pi (! A @ W) %-> (A @ W) %.
%term !G %pi (! A @ W') %-> (! A @ W) %.
% Possibility
%term ? %pi prop %-> prop %.
%prec %prefix 9 ? %.
%term ?I %pi (A @ W) %-> (? A @ W) %.
%term ?E %pi (? A @ W) %-> ({o world} %pi (A @ o) %-> (C @ W)) %-> (C @ W) %.
%term ?G %pi (? A @ W') %-> (? A @ W) %.

There are two modal connectives: $\Box A$, written !A and $\Diamond A$, 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
%term & %pi prop %-> prop %-> prop %.
%prec %none 9 & %.
%term &I %pi (A @ W) %-> (B @ W) %-> (A & B @ W) %.
%term &E1 %pi (A & B @ W) %-> (A @ W) %.
%term &E2 %pi (A & B @ W) %-> (B @ W) %.
% Falsehood
%scope &E2 %term |_ prop %.
%term |_E %pi (_|_ @ W) %-> (C @ W') %.
% Structural Rules
%term letcc %pi (%pi (A * W) %-> (A @ W)) %-> (A @ W) %.
%term throw %pi (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
%sort true {_ prop} {_ world} %.
%name true %.
%sort false {_ prop} {_ world} %.
%name false %.
%sort # %.

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
%term contra %pi (true A W) %-> (false A W) %-> # %.
% arrow
%term =>T %pi (%pi (false A W) %-> #) %-> (%pi (true B W) %-> #) %-> (true (A => B) W) %-> # %.
%term =>F %pi (%pi (true A W) %-> (false B W) %-> #) %-> (false (A => B) W) %-> # %.
% box
%term !T %pi (%pi (true A W') %-> #) %-> (true (! A) W) %-> # %.
%term !F %pi ({w world} %pi (false A w) %-> #) %-> (false (! A) W) %-> # %.
% dia
%term ?T %pi ({w world} %pi (true A w) %-> #) %-> (true (? A) W) %-> # %.
%term ?F %pi (%pi (false A W') %-> #) %-> (false (? A) W) %-> # %.

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

% conjunction
%term &T %pi (%pi (true A W) %-> (true B W) %-> #) %-> (true (A & B) W) %-> # %.
%term &F %pi (%pi (false A W) %-> #) %-> (%pi (false B W) %-> #) %-> (false (A & B) W) %-> # %.
% falsehood
%scope &F %term |_T %pi (true _|_ W) %-> # %.

Cut elimination

% admissibility of excluded middle (cut)
%sort xm {A prop} {W world} {_ %pi (true A W) %-> #} {_ %pi (false A W) %-> #} {_ #} %.
%mode xm %in %in %in %in %out %.

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
%term xt_init xm A W ([xt] contra xt D) ([xf] E xf) (E D) %.
%term xf_init xm A W ([xt] D xt) ([xf] contra E xf) (D E) %.
% unused assumptions
%term xt_unused xm A W ([x1] contra DT DF) E (contra DT DF) %.
%term 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.
%term xd_ct_|_ xm A W ([at] _|_T DD) _ (_|_T DD) %.
%term 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
%term xd_ct=>
  %pi (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)) %.
%term xe_ct=>
  %pi (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)) %.
%term xd_cf=>
  %pi (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)) %.
%term xe_cf=>
  %pi (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
%term xd_ct!
  %pi (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)) %.
%term xe_ct!
  %pi (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)) %.
%term xd_cf!
  %pi (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)) %.
%term xe_cf!
  %pi (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
%term xd_ct?
  %pi (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)) %.
%term xe_ct?
  %pi (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)) %.
%term xd_cf?
  %pi (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)) %.
%term xe_cf?
  %pi (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
%term xd_ct&
  %pi (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)) %.
%term xe_ct&
  %pi (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)) %.
%term xd_cf&
  %pi (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)) %.
%term xe_cf&
  %pi (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
%term x_=>
  %pi (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
%term x_!
  %pi (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
%term x_?
  %pi (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
%term x_&
  %pi (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 {w world}%.
%block blockt [A prop] [W world] {tt true A W}%.
%block blockf [A prop] [W world] {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
%sort ndseq {_ A @ W} {_ %pi (false A W) %-> #} %.
%mode ndseq %in %out %.
% conjunction
%term ns-&I %pi (ndseq (&I D1 D2) (&F F1 F2)) %<- (ndseq D1 F1) %<- (ndseq D2 F2) %.
%term ns-&E1
  %pi (ndseq (&E1 (%the (A & B @ W) D1)) ([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)) %.
%term ns-&E2
  %pi (ndseq (&E2 (%the (A & B @ W) D1)) ([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
%term ns-_|_E
  %pi (ndseq (_|_E (%the (_|_ @ W) D1)) ([af] F af))
  %<- (ndseq D1 ([_|_f] F2 _|_f))
  %<- ({af} xm _|_ W ([_|_t] _|_T _|_t) ([_|_f] F2 _|_f) (F af)) %.
% implication
%term ns-=>I
  %pi (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} %pi (ndseq a ([af] contra at af)) %-> (ndseq (D a) ([bf] F at bf))) %.
%term ns-=>E
  %pi (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
%term ns-!I
  %pi (ndseq (!I ([w] D1 w)) (!F ([w] [af false A w] F w af)))
  %<- ({w} ndseq (D1 w) (F w)) %.
%term ns-!E
  %pi (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)) %.
%term ns-!G
  %pi (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
%term ns-?I %pi (ndseq (?I D) ([?f] ?F ([af] F af) ?f)) %<- (ndseq D ([af] F af)) %.
%term ns-?E
  %pi (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'} %pi (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)) %.
%term ns-?G
  %pi (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
%sort contfalse {_ A * W} {_ false A W} %.
%mode contfalse %in %out %.
% note contraction: F in output uses af twice
%term ns-letcc
  %pi (ndseq (letcc ([ac] D ac)) ([af] F af af))
  %<- ({ac A * W} {af false A W} %pi (contfalse ac af) %-> (ndseq (D ac) (F af))) %.
% note weakening: [cf'] is unused.
%term ns-throw
  %pi (ndseq (throw D K) ([cf'] F AF))
  %<- (ndseq D ([af] F af))
  %<- (contfalse K AF) %.
%block blockh [A prop] [W world] {a A @ W} {at true A W} {_ ndseq a ([af] contra at af)}%.
%block block* [A prop] [W world] {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
%sort xs {_ {c} {w} %pi (A @ W) %-> (c @ w)} {_ %pi (A * W) %-> (B @ W')} {_ B @ W'} %.
%name xs %.
%mode xs %in %in %out %.
% 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!
%term xs-closed xs D ([a*] E) E %.
% falsehood
%term xs-_|_E %pi (xs D ([u] _|_E (EE u)) (_|_E EE')) %<- (xs D EE EE') %.
% conjunction
%term xs-&I %pi (xs D ([u] &I (EA u) (EB u)) (&I F1 F2)) %<- (xs D EA F1) %<- (xs D EB F2) %.
%term xs-&E1 %pi (xs D ([u] &E1 (E u)) (&E1 F)) %<- (xs D E F) %.
%term xs-&E2 %pi (xs D ([u] &E2 (E u)) (&E2 F)) %<- (xs D E F) %.
% implication
%term xs-=>I
  %pi (xs D ([u] =>I ([aw A @ W] E aw u)) (=>I ([aw] F aw)))
  %<- ({aw A @ W} xs D (E aw) (F aw)) %.
%term xs-=>E %pi (xs D ([u] =>E (DF u) (DA u)) (=>E FF FA)) %<- (xs D DF FF) %<- (xs D DA FA) %.
% box
%term xs-!I
  %pi (xs D ([u A * W] !I ([w] E u w)) (!I ([w] F w)))
  %<- ({w world} xs D ([u] E u w) (F w)) %.
%term xs-!G %pi (xs D ([u] !G (E u)) (!G F)) %<- (xs D E F) %.
%term xs-!E %pi (xs D ([u] !E (E u)) (!E F)) %<- (xs D E F) %.
% possibility
%term xs-?E
  %pi (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)) %.
%term xs-?I %pi (xs D ([u] ?I (E u)) (?I F)) %<- (xs D E F) %.
%term xs-?G %pi (xs D ([u] ?G (E u)) (?G F)) %<- (xs D E F) %.
%term xs-letcc
  %pi (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
%term xs-throwmiss %pi (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.
%term xs-throwhit %pi (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 : *
%sort seqnd {_ #} {_ {a} {w} a @ w} %.
%name seqnd %.
%sort truend {_ true A W} {_ A @ W} %.
%name truend %.
%sort falsend {_ false A W} {_ A * W} %.
%name falsend %.
%mode seqnd %in %out %.
%mode truend %in %out %.
%mode falsend %in %out %.
%term sn-contra
  %pi (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
%term sn-_|_T %pi (seqnd (_|_T FT) ([c] [w] _|_E FT')) %<- (truend FT FT') %.
% conjunction
%term sn-&T
  %pi (seqnd (&T ([at] [bt] D at bt) T&) ([c] [w] F (&E1 N&) (&E2 N&) c w))
  %<- ({at} {a}
  %pi (truend at a)
  %-> ({bt} {b} %pi (truend bt b) %-> (seqnd (D at bt) ([c] [w] F a b c w))))
  %<- (truend T& N&) %.
%term sn-&F
  %pi (seqnd (&F ([af] D1 af) ([bf] D2 bf) (%the (false (A & B) W) F&)) FF)
  %<- (falsend F& N&)
  %<- ({af} {a*} %pi (falsend af a*) %-> (seqnd (D1 af) ([c] [w] F1 a* c w)))
  %<- ({bf} {b*} %pi (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.
%term sn-=>T
  %pi (seqnd (=>T ([af false A W] D1 af) ([bt] D2 bt) (%the (true (A => B) W) T=>)) FF)
  %<- (truend T=> N=>)
  %<- ({af} {a*} %pi (falsend af a*) %-> (seqnd (D1 af) ([c] [w] F1 a* c w)))
  %<- ({bt} {b} %pi (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
%term sn-=>F
  %pi (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}
  %pi (truend at a)
  %-> ({bf} {b*} %pi (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
%term sn-=>F-letcc
  %pi (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}
  %pi (truend at a)
  %-> ({bf} {b*} %pi (falsend bf b*) %-> (seqnd (D at bf) ([c] [w] F1 a b* c w)))) %.
% box
%term sn-!T
  %pi (seqnd (!T ([at' true A W'] D at') T!) ([c] [w] F (!E (!G N!)) c w))
  %<- ({at'} {a'} %pi (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
%term sn-!F
  %pi (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'} %pi (falsend af' a*') %-> (seqnd (D w' af') ([c] [w] F w' a*' c w))) %.
% dia
% x : ?A@w |- let dia <y,w'> = get<w>x in IH end
%term sn-?T
  %pi (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'} %pi (truend at a') %-> (seqnd (D w' at) ([c] [w] F w' a' c w))) %.
%term sn-?F
  %pi (seqnd (?F ([af'] D af') F?) FF)
  %<- (falsend F? N?)
  %<- ({af' false A W'} {a*' A * W'} %pi (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 STELF to check them:

% for xs
%block blocku [A prop] [W world] {u A * W}%.
%block blocka [A prop] [W world] {u A @ W}%.
% for seqnd
%block blocknt [A prop] [W world] {at true A W} {a A @ W} {t truend at a}%.
%block blocknf [A prop] [W world] {af false A W} {a A * W} {t falsend af a}%.
%block blockp {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. check="true">STELF's output from this case study.

Category:STELF code