Documentation out of dateLearn more

Lax logic

In this article, we will take a presentation of a logic very close to that of Fairtlough and Mendler’s lax logic and show a translation into a polarized version of Pfenning and Davies’ judgmental reconstruction of lax logic. We will refer to the non-judgmental, non-polarized system as the source logic and to the judgmentally reconstructed, polarized system as the target logic. While we tend to see judgmentally reconstructed logics as Good $Things^{TM}$ , there’s nothing inherently interesting about polarization of the the target logic on its own — the target logic is polarized because it will make the proof of completeness for focused lax logic clearer.

Therefore, we have three separate things that are happening simultaneously.

First, we are formally establishing the connection between Fairtlough and Mendler’s system and Pfenning and Davies’ system.
Second, because the source logic has a cut rule and the target logic does not, we prove the admissibility of cut in the target logic and use it to eliminate instances of the cut rule during translation. Alternatively, we could have (presumably) proven cut elimination within Fairtlough and Mendler’s system, or we could have left a cut rule in the target logic and then proven cut elimination there.
Third, we are showing the connection between a non-polarized system and a polarized one. All three of these things could be done separately, but we did not find that it added to the overall complexity to do them all together.

The third point above, translation into a non-polarized system, is where most of the technical difficulty of the completeness proof happens, because a general translation from a non-polarized logic to a polarized one may add an arbitrary number of shift operations.

Preliminaries

We will be using a metric to make certain arguments about translation simpler - we can think of this metric as a tree T that is either a leaf (o), a parent with one child tree (x T), or a parent with two child trees (T1 | T2).

%sort metric %.
%name metric %.
%term o metric %.
%term x %pi metric %-> metric %.
%term | %pi metric %-> metric %-> metric %.
%prec %right 10 | %.
%sort id {_ metric} {_ metric} %.
%name id %.
%term id/refl id M M %.

We will also be, throughout, working in a universe of atomic propositions. Each atomic proposition has a defined polarity (pos or neg), though this is mostly irrelevant in the target logic and totally irrelevant in the source logic. Every theorem we prove will assume a universe of arbitrary atomic propositions of both polarities, so every %worlds declaration will include at least the blocks bl_atmpos (positive atomic propositions) and bl_atmneg (negative atomic propositions).

%sort polarity %.
%name polarity %.
%term pos polarity %.
%term neg polarity %.
%sort atm {_ polarity} %.
%name atm %.
%block bl_atmpos {qp atm pos}%.
%block bl_atmneg {qn atm neg}%.

Fairtlough and Mendler’s lax logic

Fairtlough and Mendler’s presentation of lax logic has a slight inconsistancy: the logic’s syntax is defined as

$M ::= Q \mid \mathsf{true} \mid \mathsf{false} \mid M \wedge M \mid M \vee M \mid M \supset M \mid \neg M \mid {\bigcirc}M$

However, rules are given for neither $\mathsf{true}$ nor $\mathsf{false}$ . A reasonable approach seemed to be to define $\mathsf{false}$ as $\neg \mathsf{true}$ .

%sort prop' %.
%name prop' %.
%term atom' %pi (atm S) %-> prop' %.
%term tt' prop' %.
%term /\ %pi prop' %-> prop' %-> prop' %.
%prec %right 9 /\ %.
%term \/ %pi prop' %-> prop' %-> prop' %.
%prec %right 8 \/ %.
%term => %pi prop' %-> prop' %-> prop' %.
%prec %right 7 => %.
%term not' %pi prop' %-> prop' %.
%term circ' %pi prop' %-> prop' %.
%define ff' prop' not' tt' %.

Sequent calculus

Fairtlough and Mendler present a Genzen-style intuitionstic sequent calculus for propositional lax logic in terms of sequents $\Gamma \vdash \Delta$ , where $\Gamma$ is a finite list of hypotheses and $\Delta$ is either 0 or 1 assertions. To prove $\Gamma \vdash$ is to say that the hypotheses in $\Gamma$ are contradictory, to prove $\Gamma \vdash M$ is to say that the hypotheses in $\Gamma$ establish the proposition $M$ .

We represent the hypotheses using the LF context; each $M \in \Gamma$ becomes an LF variable of type hyp' M, and we use the world bl_hyp' to describe all such contexts.

%sort hyp' {_ prop'} %.
%block bl_hyp' [M prop'] {h hyp' M}%.

We represent the conclusion as conc' T D, where

T is a metric capturing the shape of the derivation
D = conc-#' represents proving a contradiction $\Gamma \vdash$ ; we abbreviate conc' T conc-#' as # T.
D = conc-true' M represents proving $\Gamma \vdash M$ ; we abbreviate conc' T (conc-true' M) as true' T M.

%sort conseq' %.
%name conseq' %.
%term conc-# conseq' %.
% Contradiction, length 0
%term conc-true' %pi prop' %-> conseq' %.
% Conclusion, length 1
%sort conc' {_ metric} {_ conseq'} %.
%inline # [m] conc' m conc-# %.
%inline true' [m] [x] conc' m (conc-true' x) %.

While our use of a structural metric embedded into the conclusion of a sequent needs to be justified by adequacy, it is less of an issue than other changes we have made to the system.

As previously mentioned, Fairtlough and Mendler’s system had no rule for $\mathsf{true}$ , and we need no rule for $\mathsf{false}$ as we defined it in terms of $\mathsf{true}$ . We do not write rules for weakening on the left or exchange on the left, as those are provided “for free” by the encoding into LF. In addition, we embed contraction into every left rule:

F&M left conjunction rule: $\frac{\Gamma, A, B \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta}$

Our left conjunction rule: $\frac{\Gamma, A \wedge B, A, B \vdash \Delta}{\Gamma, A \wedge B \vdash \Delta}$

With those caveats, we will continue to consider our source logic, presented here, to have the essential character of Fairtlough and Mendler’s.

Rules on paper

$\frac {~~~} {\Gamma \vdash \mathsf{true}} {\mathsf{true}}R$ $\frac {\Gamma \vdash M \qquad \Gamma \vdash N} {\Gamma \vdash M \wedge N} {\wedge}R$ $\frac {\Gamma, M \wedge N, M, N \vdash \Delta} {\Gamma, M \wedge N \vdash \Delta} {\wedge}L$

$\frac {\Gamma \vdash M} {\Gamma \vdash M \vee N} {\vee}R_1$ $\frac {\Gamma \vdash N} {\Gamma \vdash M \vee N} {\vee}R_2$ $\frac {\Gamma, M \vee N, M \vdash \Delta \qquad \Gamma, M \vee N, N \vdash \Delta} {\Gamma \vdash \Delta} {\vee}L$

$\frac {\Gamma, M \vdash N} {\Gamma \vdash M \supset N} {\supset}R$ $\frac {\Gamma, M \supset N \vdash M \qquad \Gamma, M \supset N, N \vdash \Delta} {\Gamma, M \supset N \vdash \Delta} {\supset}L$ $\frac {\Gamma, M \vdash} {\Gamma \vdash \neg M} {\neg}R$ $\frac {\Gamma, \neg M \vdash M} {\Gamma, \neg M \vdash} {\neg}L$

$\frac {\Gamma \vdash M} {\Gamma \vdash {\bigcirc} M} {\bigcirc}R$ $\frac {\Gamma, {\bigcirc} M, M \vdash {\bigcirc} N} {\Gamma, {\bigcirc} M \vdash {\bigcirc} N} {\bigcirc}L$

$\frac {~~~} {\Gamma, M \vdash M} {id}$ $\frac {\Gamma \vdash M \qquad \Gamma, M \vdash \Delta} {\Gamma \vdash \Delta} {cut}$ $\frac {\Gamma \vdash} {\Gamma \vdash M} {weakR}$

Rules in STELF

%term trueR' true' o tt' %.
% no trueL'
%term /\R' %pi (true' Tm M) %-> (true' Tn N) %-> (true' (Tm | Tn) (M /\ N)) %.
%term /\L'
  %pi (%pi (hyp' M) %-> (hyp' N) %-> (conc' T D))
  %-> (hyp' (M /\ N))
  %-> (conc' (x (x T)) D) %.
%term \/R1' %pi (true' T M) %-> (true' (x T) (M \/ N)) %.
%term \/R2' %pi (true' T N) %-> (true' (x T) (M \/ N)) %.
%term \/L'
  %pi (%pi (hyp' M) %-> (conc' Tm D))
  %-> (%pi (hyp' N) %-> (conc' Tn D))
  %-> (hyp' (M \/ N))
  %-> (conc' (x (Tm | Tn)) D) %.
%term =>R' %pi (%pi (hyp' M) %-> (true' T N)) %-> (true' (x T) (M => N)) %.
%term =>L'
  %pi (true' Tm M)
  %-> (%pi (hyp' N) %-> (conc' Tn D))
  %-> (hyp' (M => N))
  %-> (conc' (x (Tm | Tn)) D) %.
%term notR' %pi (%pi (hyp' M) %-> (# T)) %-> (true' (x T) (not' M)) %.
%term notL' %pi (true' T M) %-> (hyp' (not' M)) %-> (# (x (x T))) %.
%term circR' %pi (true' T M) %-> (true' (x T) (circ' M)) %.
%term circL'
  %pi (%pi (hyp' M) %-> (true' T (circ' N)))
  %-> (hyp' (circ' M))
  %-> (true' (x (x T)) (circ' N)) %.
%term id' %pi (hyp' M) %-> (true' o M) %.
%term cut' %pi (true' Ta M) %-> (%pi (hyp' M) %-> (conc' T D)) %-> (conc' (Ta | T) D) %.
%term weakR' %pi (# T) %-> (true' (x T) M) %.
%worlds (bl_atmpos bl_atmneg bl_hyp') (hyp' M) (conc' T M) %.
% = (# T) (true' T A)

Polarized judgmental lax logic

Polarized lax logic loses the $\neg$ but distinguishes between two different kinds of conjunction, $\wedge^+$ and $\wedge^-$ , and two variants of $\mathsf{true}$ which are the units of the two kinds of conjunction.

Every proposition has a polarity, not just atomic propositions, and this limits what we can write down. For instance, we cannot write $\top \vee 0$ , because $\vee$ expectes two positive things and $\top$ is negative. We could either write $1 \vee 0$ , or else we could write $({\downarrow}\top) \vee 0$ .

The full language of propositions is:

$A ::= P \mid N$

$P ::= Q^+ \mid {\downarrow}N \mid 1 \mid 0 \mid P \wedge^+ P \mid P \vee P$

$N ::= Q^- \mid {\uparrow}P \mid \top \mid N \wedge^- N \mid P \supset N \mid {\bigcirc}P$

The STELF versions of the the connectives resemble ones from linear logic, but we mean unrestricted implication $P \supset N$ when we write P -o N, not linear implication.

%sort prop {_ polarity} %.
%name prop %.
%term atom %pi (atm S) %-> (prop S) %.
%term up %pi (prop pos) %-> (prop neg) %.
%term down %pi (prop neg) %-> (prop pos) %.
%term top prop neg %.
%term 1 prop pos %.
%term 0 prop pos %.
%term * %pi (prop pos) %-> (prop pos) %-> (prop pos) %.
%prec %right 9 * %.
%term & %pi (prop neg) %-> (prop neg) %-> (prop neg) %.
%prec %right 8 & %.
%term + %pi (prop pos) %-> (prop pos) %-> (prop pos) %.
%prec %right 7 + %.
%scope + %term o %pi (prop pos) %-> (prop neg) %-> (prop neg) %.
%prec %right 6 -o %.
%term circ %pi (prop pos) %-> (prop neg) %.

Sequent calculus

Our assumptions are, as before, represented by LF variables, this time of type hyp A.

%sort hyp {_ prop S} %.
%block bl_hyp [S polarity] [A prop S] {h hyp A}%.

We are always trying to prove one of two judgments, and so our sequents either take the form $\Gamma \vdash A~true$ ( $A$ is true) or $\Gamma \vdash A~lax$ ( $A$ is true under a constraint).

%sort conseq %.
%name conseq %.
%term conc-lax %pi (prop S) %-> conseq %.
% A lax
%term conc-true %pi (prop S) %-> conseq %.
% A true
%sort conc {_ conseq} %.
%inline lax [x] conc (conc-lax x) %.
%inline true [x] conc (conc-true x) %.

Later on in the proof of soundness we will use identity of derivations in order to make a termination argument work; with this one trick, we avoid any need for a structural metric like we used before.

%sort idconc {_ conc C} {_ conc C'} %.
%term idconc/refl idconc D D %.

Rules on paper

$\frac {~~~} {\Gamma, Q^+ \vdash Q^+~true} {init}^+$ $\frac {~~~} {\Gamma, Q^- \vdash Q^-~true} {init}^-$ $\frac {\Gamma \vdash A~true} {\Gamma \vdash A~lax} {lax}R$

$\frac {\Gamma \vdash P~true} {\Gamma \vdash {\uparrow}P~true} {\uparrow}R$ $\frac {\Gamma, {\uparrow}P, P \vdash J} {\Gamma, {\uparrow}P \vdash J} {\uparrow}L$ $\frac {\Gamma \vdash N~true} {\Gamma \vdash {\downarrow}N~true} {\downarrow}R$ $\frac {\Gamma, {\downarrow}N, N \vdash J} {\Gamma, {\downarrow}N \vdash J} {\downarrow}L$

$\frac {~~~} {\Gamma \vdash 1~true} {1}R$ $\frac {\Gamma \vdash P_1~true \qquad \Gamma \vdash P_2~true} {\Gamma \vdash P_1 \wedge^+ P_2~true} {\wedge^+}R$ $\frac {\Gamma, P_1 \wedge^+ P_2, P_1, P_2 \vdash J} {\Gamma, P_1 \wedge^+ P_2 \vdash J} {\wedge^+}L$

$\frac {~~~} {\Gamma \vdash \top~true} {\top}R$ $\frac {\Gamma \vdash N_1~true \qquad \Gamma \vdash N_2~true} {\Gamma \vdash N_1 \wedge^- N_2~true} {\wedge^-}R$

$\frac {\Gamma, N_1 \wedge^+ N_2, N_1 \vdash J} {\Gamma, N_1 \wedge^+ N_2 \vdash J} {\wedge^-}L_1$ $\frac {\Gamma, N_1 \wedge^+ N_2, N_2 \vdash J} {\Gamma, N_1 \wedge^+ N_2 \vdash J} {\wedge^-}L_2$

$\frac {\Gamma \vdash P_1~true} {\Gamma \vdash P_1 \vee P_2~true} {\vee}R_1$ $\frac {\Gamma \vdash P_2~true} {\Gamma \vdash P_1 \vee P_2~true} {\vee}R_2$ $\frac {\Gamma, P_1 \vee P_2, P_1 \vdash J \qquad \Gamma, P_1 \vee P_2, P_2 \vdash J} {\Gamma, P_1 \vee P_2 \vdash J} {\vee}R$

$\frac {\Gamma, P \vdash N~true} {\Gamma \vdash P \supset N~true} {\supset}R$ $\frac {\Gamma, P_1 \supset P_2 \vdash P_1 \qquad \Gamma, P_1 \supset P_2, P_2 \vdash J} {\Gamma, P_1 \supset P_2 \vdash J} {\supset}L$

$\frac {\Gamma \vdash P~lax} {\Gamma \vdash {\bigcirc}P~true} {\bigcirc}R$ $\frac {\Gamma, {\bigcirc}P, P \vdash A~lax} {\Gamma, {\bigcirc}P \vdash A~lax} {\bigcirc}L$

Rules in STELF

%term init+ %pi (hyp (atom Qp)) %-> (true (atom (%the (atm pos) Qp))) %.
%term init- %pi (hyp (atom Qn)) %-> (true (atom (%the (atm neg) Qn))) %.
%term laxR %pi (true A) %-> (lax A) %.
%term upR %pi (true P) %-> (true (up P)) %.
%term upL %pi (%pi (hyp P) %-> (conc J)) %-> (hyp (up P)) %-> (conc J) %.
%term downR %pi (true N) %-> (true (down N)) %.
%term downL %pi (%pi (hyp N) %-> (conc J)) %-> (hyp (down N)) %-> (conc J) %.
%term 1R true 1 %.
% no 1L
%term *R %pi (true P1) %-> (true P2) %-> (true (P1 * P2)) %.
%term *L %pi (%pi (hyp P1) %-> (hyp P2) %-> (conc J)) %-> (hyp (P1 * P2)) %-> (conc J) %.
%term topR true top %.
% no topL
%term &R %pi (true N1) %-> (true N2) %-> (true (N1 & N2)) %.
%term &L1 %pi (%pi (hyp N1) %-> (conc J)) %-> (hyp (N1 & N2)) %-> (conc J) %.
%term &L2 %pi (%pi (hyp N2) %-> (conc J)) %-> (hyp (N1 & N2)) %-> (conc J) %.
% no 0R
%term 0L %pi (hyp 0) %-> (conc J) %.
%term +R1 %pi (true P1) %-> (true (P1 + P2)) %.
%term +R2 %pi (true P2) %-> (true (P1 + P2)) %.
%term +L
  %pi (%pi (hyp P1) %-> (conc J))
  %-> (%pi (hyp P2) %-> (conc J))
  %-> (hyp (P1 + P2))
  %-> (conc J) %.
%scope +L %term oR %pi (%pi (hyp P) %-> (true N)) %-> (true (P -o N)) %.
%term oL %pi (true P) %-> (%pi (hyp N) %-> (conc J)) %-> (hyp (P -o N)) %-> (conc J) %.
%term circR %pi (lax P) %-> (true (circ P)) %.
%term circL %pi (%pi (hyp P) %-> (lax A)) %-> (hyp (circ P)) %-> (lax A) %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (hyp A) (conc J) %.

Translation

Now we can define a nondeterminstic translation between our variant of Fairtlough and Mendler’s propositional lax logic and our target logic, polarized, judgmental lax logic. We will use a metric that essentially captures the structure of the term in the target logic (in fact, it would be worth seeing if we could use the term in the target logic in lieu of the metric.)

Propositions

The intent of the first relation we define is to be maximally general, which means that the t+- and t-+ rules can add an arbitrary number of shifts. Read in the reverse direction, the translation is not very nondeterminstic; however “P -o up 0” can still be translated to either “not M” or “M => (not' tt'),” which are different source logic expressions.

%sort trans {_ metric} {_ prop'} {S} {_ prop S} %.
%name trans %.
%term t+- %pi (trans T M pos P) %-> (trans (x T) M neg (up P)) %.
%term t-+ %pi (trans T M neg N) %-> (trans (x T) M pos (down N)) %.
%term tatom trans o (atom' Q) S (atom Q) %.
%term t+true trans o tt' pos 1 %.
%term t-true trans o tt' neg top %.
%term t+false trans o ff' pos 0 %.
%term t+and
  %pi (trans T1 M1 pos P1)
  %-> (trans T2 M2 pos P2)
  %-> (trans (T1 | T2) (M1 /\ M2) pos (P1 * P2)) %.
%term t-and
  %pi (trans T1 M1 neg N1)
  %-> (trans T2 M2 neg N2)
  %-> (trans (T1 | T2) (M1 /\ M2) neg (N1 & N2)) %.
%term t+or
  %pi (trans T1 M1 pos P1)
  %-> (trans T2 M2 pos P2)
  %-> (trans (T1 | T2) (M1 \/ M2) pos (P1 + P2)) %.
%term t-imp
  %pi (trans T1 M1 pos P)
  %-> (trans T2 M2 neg N)
  %-> (trans (T1 | T2) (M1 => M2) neg (P -o N)) %.
%term t+not %pi (trans T M pos P) %-> (trans (x T) (not' M) neg (P -o up 0)) %.
%term t+circ %pi (trans T M pos P) %-> (trans (x T) (circ' M) neg (circ P)) %.
%worlds (bl_atmpos bl_atmneg) (trans _ _ _ _) %.

Conclusions

We additionally define translation between right-hand-sides D in the source logic and judgments J in the target logic.

%sort trans-conc {_ metric} {_ conseq'} {_ conseq} %.
%name trans-conc %.
%term tc %pi (trans-conc T (conc-true' M) (conc-true A)) %<- (trans T M S A) %.
%term tc# trans-conc o conc-# (conc-true (up 0)) %.
%term tclax %pi (trans-conc T (conc-true' (circ' M)) (conc-lax A)) %<- (trans T M S A) %.
%worlds (bl_atmpos bl_atmneg) (trans-conc _ _ _) %.

Hypotheses

When we are showing soundness and completeness, we will need to know that for every hypothesis in the {source, target} logic we have a hypothesis in the {target, source} logic such that one is the translation of the other.

What we would like to do is define a single trans-hyp that allows us to translate from source logic hypotheses to target logic hypotheses, and vice versa. However, because we cannot assign multiple modes to the same relation, we’ll define two different relations, and use them to define two different worlds.

trans-soundhyp takes a target logic hypotheis H and obtains a translation TR and a source logic hypothesis H'.
trans-complhyp takes a source logic hypothesis H' and obtains a translation TR and a target logic hypothesis H.

%sort trans-soundhyp {_ hyp H} {_ trans Mh H' S H} {_ hyp' H'} %.
%mode trans-soundhyp %in %out %out %.
%block bl_trans-soundhyp [M metric] [S polarity] [A prop S] [A' prop'] [T trans M A' S A] {h hyp A} {h' hyp' A'} {t trans-soundhyp h T h'}%.
%worlds (bl_atmpos bl_atmneg bl_trans-soundhyp) (trans-soundhyp _ _ _) %.
%total [] (trans-soundhyp _ _ _) %.
%sort trans-complhyp {_ hyp' A} {_ trans Mt A S C} {_ hyp C} %.
%mode trans-complhyp %in %out %out %.
%block bl_trans-complhyp [M metric] [A prop'] [S polarity] [C prop S] [T trans M A S C] {h' hyp' A} {h hyp C} {t trans-complhyp h' T h}%.
%worlds (bl_atmpos bl_atmneg bl_trans-complhyp) (trans-complhyp _ _ _) %.
%total [] (trans-complhyp _ _ _) %.

Correspondence

A corollary to the theorem we will state below will say “If $\vdash A~true$ and $M~\texttt{trans}~A$ , then $\vdash M$ .” However, if there is no $M$ such that $M~\texttt{trans}~A$ , then the theorem will be vacuously true, which is not our intent. Therefore, we need to establish that our translations of propositions and conclusions are correspondences (left- and right-total).

STELF can verify that translation is right-total, that there is an M for every A and a D for every J, without any further work on our part: we just assign modes to the relation and state a totality assertion.

%mode trans %out %out %in %in %.
%mode trans-conc %out %out %in %.
%total (A C) (trans _ _ _ A) (trans-conc _ _ C) %.

However, in the forward direction, to show that the relation is left-total we will need to write an effectiveness lemma, which we will call can-trans.

The two lemmas can-switch are really just case analysis to establish that if you can translate something as a positive formula, you can apply an up shift to make it a negative formula, and vice versa.

%sort can-switch+ {_ trans M A S (%the (prop S) C)} {_ trans N A pos C'} %.
%term _ can-switch+ T T %.
%term _ can-switch+ T (t-+ T) %.
%mode can-switch+ %in %out %.
%worlds (bl_atmpos bl_atmneg) (can-switch+ _ _) %.
%total [] (can-switch+ _ _) %.
%sort can-switch- {_ trans M A S' C} {_ trans N A neg C'} %.
%term _ can-switch- T T %.
%term _ can-switch- T (t+- T) %.
%mode can-switch- %in %out %.
%worlds (bl_atmpos bl_atmneg) (can-switch- _ _) %.
%total [] (can-switch- _ _) %.
%sort can-trans {A} {_ trans M A S (%the (prop S) C)} %.
%mode can-trans %in %out %.
%term _ can-trans (atom' Qp) tatom %.
%term _ can-trans tt' t-true %.
%term _
  %pi (can-trans (A /\ B) (t-and T1' T2'))
  %<- (can-trans A T1)
  %<- (can-switch- T1 T1')
  %<- (can-trans B T2)
  %<- (can-switch- T2 T2') %.
%term _
  %pi (can-trans (A \/ B) (t+or T1' T2'))
  %<- (can-trans A T1)
  %<- (can-switch+ T1 T1')
  %<- (can-trans B T2)
  %<- (can-switch+ T2 T2') %.
%term _
  %pi (can-trans (A => B) (t-imp T1' T2'))
  %<- (can-trans A T1)
  %<- (can-switch+ T1 T1')
  %<- (can-trans B T2)
  %<- (can-switch- T2 T2') %.
%term _ %pi (can-trans (not' A) (t+not T')) %<- (can-trans A T) %<- (can-switch+ T T') %.
%term _ %pi (can-trans (circ' A) (t+circ T')) %<- (can-trans A T) %<- (can-switch+ T T') %.
%worlds (bl_atmpos bl_atmneg) (can-trans _ _) %.
%total A (can-trans A _) %.
%sort can-trans-conc {D} {_ trans-conc T D J} %.
%mode can-trans-conc %in %out %.
%term _ can-trans-conc conc-# tc# %.
%term _ %pi (can-trans-conc (conc-true' M) (tc TR)) %<- (can-trans M TR) %.
%worlds (bl_atmpos bl_atmneg) (can-trans-conc _ _) %.
%total A (can-trans-conc A _) %.

Metatheory of the target logic

The correctness of translation will rest on the standard metatheoretic results: the identity principle and the admissibility of cut. Note that we could have added a cut and id rule to the target logic, but we still would have eventually needed to do the work in this section in order to have confidence that our target logic was reasonable.

Identity

For all propositions $A$ , there exists a derivation of $A \vdash A~true$ .

The proof is by induction on the formula $A$ .

%sort identity {A} {_ %pi (hyp A) %-> (true A)} %.
%mode identity %in %out %.
%term _ identity (atom Q) init+ %.
%term _ identity (atom Q) init- %.
%term _
  %pi (identity (up P) ([h] upL ([h'] upR (D h')) h))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) D)) %.
%term _
  %pi (identity (down N) ([h] downL ([h'] downR (D h')) h))
  %<- (identity N (%the (%pi (hyp N) %-> (true N)) D)) %.
%term _ identity top ([_] topR) %.
%term _ identity 1 ([_] 1R) %.
%term _ identity 0 ([h] 0L h) %.
%term _
  %pi (identity (P1 * P2) ([h] *L ([h1] [h2] *R (D1 h1) (D2 h2)) h))
  %<- (identity P1 (%the (%pi (hyp P1) %-> (true P1)) D1))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D2)) %.
%term _
  %pi (identity (N1 & N2) ([h] &L1 ([h1] &L2 ([h2] &R (D1 h1) (D2 h2)) h) h))
  %<- (identity N1 (%the (%pi (hyp N1) %-> (true N1)) D1))
  %<- (identity N2 (%the (%pi (hyp N2) %-> (true N2)) D2)) %.
%term _
  %pi (identity (P1 + P2) ([h] +L ([h1] +R1 (D1 h1)) ([h2] +R2 (D2 h2)) h))
  %<- (identity P1 (%the (%pi (hyp P1) %-> (true P1)) D1))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D2)) %.
%term _
  %pi (identity (P -o N) ([h] -oR ([h1] -oL (D1 h1) ([h2] D2 h2) h)))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) D1))
  %<- (identity N (%the (%pi (hyp N) %-> (true N)) D2)) %.
%term _
  %pi (identity (circ P) ([h] circR (circL ([h'] laxR (D1 h')) h)))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) D1)) %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (identity _ _) %.
%total T (identity T _) %.

Cut admissibility

There are two cut principles which must be proven simultaneously; cut is the main theorem, and lcut is the cut principle for lax truth.

If $\Gamma \vdash A~true$ and $\Gamma, A \vdash J$ , then $\Gamma \vdash J$ (cut)
If $\Gamma \vdash A~lax$ and $\Gamma, A \vdash C~lax$ , then $\Gamma \vdash C~lax$ (lcut)

The proofs are by mutual lexographic induction; either the principal cut formula $A$ gets smaller, or else the principal cut formula stays the same and one or both of the input derivations get smaller. The proof is entirely standard other than the need for extra commutative cuts for tlax; more explanation is available at the article on the admissibility of cut.

%sort cut {A} {_ true A} {_ %pi (hyp A) %-> (conc J)} {_ conc J} %.
%sort lcut {A} {_ lax A} {_ %pi (hyp A) %-> (lax C)} {_ lax C} %.
%mode cut %in %in %in %out %.
%mode lcut %in %in %in %out %.

Principal cuts

%term _ cut (atom Q) (init+ H) ([h] init+ h) (init+ H) %.
%term _ cut (atom Q) (init- H) ([h] init- h) (init- H) %.
%term _
  %pi (cut (up P) (upR (%the (true P) D)) ([h] upL (%the (%pi (hyp P) %-> (conc J)) (E h)) h) G)
  %<- ({h' hyp P} cut (up P) (upR D) ([h] E h h') (F h'))
  %<- (cut P D ([h'] F h') (%the (conc J) G)) %.
%term _
  %pi (cut (down N) (downR (%the (true N) D)) ([h] downL (%the (%pi (hyp N) %-> (conc J)) (E h)) h) G)
  %<- ({h' hyp N} cut (down N) (downR D) ([h] E h h') (F h'))
  %<- (cut N D ([h'] F h') (%the (conc J) G)) %.
%term _
  %pi (cut (P1 * P2) (*R (%the (true P1) D1) (%the (true P2) D2)) ([h] *L (%the (%pi (hyp P1) %-> (hyp P2) %-> (conc J)) (E h)) h) G)
  %<- ({h1 hyp P1} {h2 hyp P2} cut (P1 * P2) (*R D1 D2) ([h] E h h1 h2) (F h1 h2))
  %<- ({h2 hyp P2} cut P1 D1 ([h1] F h1 h2) (F1 h2))
  %<- (cut P2 D2 ([h2] F1 h2) (%the (conc J) G)) %.
%term _
  %pi (cut (N1 & N2) (&R (%the (true N1) D1) (%the (true N2) D2)) ([h] &L1 (%the (%pi (hyp N1) %-> (conc J)) (E h)) h) G)
  %<- ({h1 hyp N1} cut (N1 & N2) (&R D1 D2) ([h] E h h1) (F h1))
  %<- (cut N1 D1 ([h1] F h1) (%the (conc J) G)) %.
%term _
  %pi (cut (N1 & N2) (&R (%the (true N1) D1) (%the (true N2) D2)) ([h] &L2 (%the (%pi (hyp N2) %-> (conc J)) (E h)) h) G)
  %<- ({h2 hyp N2} cut (N1 & N2) (&R D1 D2) ([h] E h h2) (F h2))
  %<- (cut N2 D2 ([h2] F h2) (%the (conc J) G)) %.
%term _
  %pi (cut (P1 + P2) (+R1 (%the (true P1) D1)) ([h] +L (%the (%pi (hyp P1) %-> (conc J)) (E1 h)) _ h) G)
  %<- ({h1 hyp P1} cut (P1 + P2) (+R1 D1) ([h] E1 h h1) (F h1))
  %<- (cut P1 D1 ([h1] F h1) G) %.
%term _
  %pi (cut (P1 + P2) (+R2 (%the (true P2) D2)) ([h] +L _ (%the (%pi (hyp P2) %-> (conc J)) (E2 h)) h) G)
  %<- ({h2 hyp P2} cut (P1 + P2) (+R2 D2) ([h] E2 h h2) (F h2))
  %<- (cut P2 D2 ([h2] F h2) G) %.
%term _
  %pi (cut (P -o N) (-oR (%the (%pi (hyp P) %-> (true N)) D)) ([h] -oL (%the (true P) (E1 h)) (%the (%pi (hyp N) %-> (conc J)) (E2 h)) h) G)
  %<- (cut (P -o N) (-oR D) ([h] E1 h) (%the (true P) F1))
  %<- ({h' hyp N} cut (P -o N) (-oR D) ([h] E2 h h') (%the (conc J) (F2 h')))
  %<- (cut P F1 ([h'] D h') (%the (true N) G1))
  %<- (cut N G1 ([h'] F2 h') (%the (conc J) G)) %.
%term _
  %pi (cut (circ P) (circR (%the (lax P) D)) ([h] circL (%the (%pi (hyp P) %-> (lax C)) (E h)) h) G)
  %<- ({h' hyp P} cut (circ P) (circR D) ([h] E h h') (%the (lax C) (F h')))
  %<- (lcut P D ([h'] F h') G) %.

Left commutative cuts

%term _ %pi (lcut P (laxR (%the (true P) D)) E F) %<- (cut P D E F) %.
%term _ %pi (cut A (upL D H) E (upL F H)) %<- ({h1} cut A (D h1) E (F h1)) %.
%term _ %pi (cut A (downL D H) E (downL F H)) %<- ({h1} cut A (D h1) E (F h1)) %.
%term _ cut A (0L H) E (0L H) %.
%term _ %pi (cut A (*L D H) E (*L F H)) %<- ({h1} {h2} cut A (D h1 h2) E (F h1 h2)) %.
%term _ %pi (cut A (&L1 D H) E (&L1 F H)) %<- ({h1} cut A (D h1) E (F h1)) %.
%term _ %pi (cut A (&L2 D H) E (&L2 F H)) %<- ({h2} cut A (D h2) E (F h2)) %.
%term _
  %pi (cut A (+L D1 D2 H) E (+L F1 F2 H))
  %<- ({h1} cut A (D1 h1) E (F1 h1))
  %<- ({h2} cut A (D2 h2) E (F2 h2)) %.
%term _ %pi (cut A (-oL D1 D2 H) E (-oL D1 F2 H)) %<- ({h'} cut A (D2 h') E (F2 h')) %.

Monadic left commutative cuts

%term _
  %pi (lcut A (circL ([h] D h) H) E (circL ([h] F h) H))
  %<- ({h'} lcut A (D h') E (F h')) %.
%term _ %pi (lcut A (upL D H) E (upL F H)) %<- ({h1} lcut A (D h1) E (F h1)) %.
%term _ %pi (lcut A (downL D H) E (downL F H)) %<- ({h1} lcut A (D h1) E (F h1)) %.
%term _ lcut A (0L H) E (0L H) %.
%term _ %pi (lcut A (*L D H) E (*L F H)) %<- ({h1} {h2} lcut A (D h1 h2) E (F h1 h2)) %.
%term _ %pi (lcut A (&L1 D H) E (&L1 F H)) %<- ({h1} lcut A (D h1) E (F h1)) %.
%term _ %pi (lcut A (&L2 D H) E (&L2 F H)) %<- ({h2} lcut A (D h2) E (F h2)) %.
%term _
  %pi (lcut A (+L D1 D2 H) E (+L F1 F2 H))
  %<- ({h1} lcut A (D1 h1) E (F1 h1))
  %<- ({h2} lcut A (D2 h2) E (F2 h2)) %.
%term _ %pi (lcut A (-oL D1 D2 H) E (-oL D1 F2 H)) %<- ({h'} lcut A (D2 h') E (F2 h')) %.

Right commutative cuts

%term _ cut A D ([h] init+ H) (init+ H) %.
%term _ cut A D ([h] init- H) (init- H) %.
%term _ %pi (cut A D ([h] laxR (E h)) (laxR F)) %<- (cut A D ([h] E h) F) %.
%term _ %pi (cut A D ([h] upR (E h)) (upR F)) %<- (cut A D ([h] E h) F) %.
%term _
  %pi (cut A D ([h] upL ([h'] E h h') H) (upL F H))
  %<- ({h'} cut A D ([h] E h h') (F h')) %.
%term _ %pi (cut A D ([h] downR (E h)) (downR F)) %<- (cut A D ([h] E h) F) %.
%term _
  %pi (cut A D ([h] downL ([h'] E h h') H) (downL F H))
  %<- ({h'} cut A D ([h] E h h') (F h')) %.
%term _ cut A D ([h] topR) topR %.
%term _ cut A D ([h] 1R) 1R %.
%term _ cut A D ([h] 0L H) (0L H) %.
%term _
  %pi (cut A D ([h] *R (E1 h) (E2 h)) (*R F1 F2))
  %<- (cut A D ([h] E1 h) F1)
  %<- (cut A D ([h] E2 h) F2) %.
%term _
  %pi (cut A D ([h] *L ([h1] [h2] E h h1 h2) H) (*L ([h1] [h2] F h1 h2) H))
  %<- ({h1} {h2} cut A D ([h] E h h1 h2) (F h1 h2)) %.
%term _
  %pi (cut A D ([h] &R (E1 h) (E2 h)) (&R F1 F2))
  %<- (cut A D ([h] E1 h) F1)
  %<- (cut A D ([h] E2 h) F2) %.
%term _
  %pi (cut A D ([h] &L1 ([h1] E1 h h1) H) (&L1 ([h1] F1 h1) H))
  %<- ({h1} cut A D ([h] E1 h h1) (F1 h1)) %.
%term _
  %pi (cut A D ([h] &L2 ([h2] E2 h h2) H) (&L2 ([h2] F2 h2) H))
  %<- ({h2} cut A D ([h] E2 h h2) (F2 h2)) %.
%term _ %pi (cut A D ([h] +R1 (E1 h)) (+R1 F1)) %<- (cut A D ([h] E1 h) F1) %.
%term _ %pi (cut A D ([h] +R2 (E2 h)) (+R2 F2)) %<- (cut A D ([h] E2 h) F2) %.
%term _
  %pi (cut A D ([h] +L ([h1] E1 h h1) ([h2] E2 h h2) H) (+L F1 F2 H))
  %<- ({h1} cut A D ([h] E1 h h1) (F1 h1))
  %<- ({h2} cut A D ([h] E2 h h2) (F2 h2)) %.
%term _
  %pi (cut A D ([h] -oR ([h'] E h h')) (-oR ([h'] F h')))
  %<- ({h'} cut A D ([h] E h h') (F h')) %.
%term _
  %pi (cut A D ([h] -oL (E1 h) ([h'] E2 h h') H) (-oL F1 ([h'] F2 h') H))
  %<- (cut A D ([h] E1 h) F1)
  %<- ({h'} cut A D ([h] E2 h h') (F2 h')) %.
%term _ %pi (cut A D ([h] circR (E h)) (circR F)) %<- (cut A D ([h] E h) F) %.
%term _
  %pi (cut A D ([h] circL ([h'] E h h') H) (circL ([h'] F h') H))
  %<- ({h'} cut A D ([h] E h h') (F h')) %.

Monadic right commutive cuts

%term _
  %pi (lcut A D ([h] upL ([h'] E h h') H) (upL F H))
  %<- ({h'} lcut A D ([h] E h h') (F h')) %.
%term _
  %pi (lcut A D ([h] downL ([h'] E h h') H) (downL F H))
  %<- ({h'} lcut A D ([h] E h h') (F h')) %.
%term _
  %pi (lcut A D ([h] *L ([h1] [h2] E h h1 h2) H) (*L ([h1] [h2] F h1 h2) H))
  %<- ({h1} {h2} lcut A D ([h] E h h1 h2) (F h1 h2)) %.
%term _
  %pi (lcut A D ([h] &L1 ([h1] E1 h h1) H) (&L1 ([h1] F1 h1) H))
  %<- ({h1} lcut A D ([h] E1 h h1) (F1 h1)) %.
%term _
  %pi (lcut A D ([h] &L2 ([h2] E2 h h2) H) (&L2 ([h2] F2 h2) H))
  %<- ({h2} lcut A D ([h] E2 h h2) (F2 h2)) %.
%term _
  %pi (lcut A D ([h] +L ([h1] E1 h h1) ([h2] E2 h h2) H) (+L F1 F2 H))
  %<- ({h1} lcut A D ([h] E1 h h1) (F1 h1))
  %<- ({h2} lcut A D ([h] E2 h h2) (F2 h2)) %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (cut _ _ _ _) (lcut _ _ _ _) %.
%total {(A1 A2) [(D1 D2) (E1 E2)]} (cut A1 D1 E1 F1) (lcut A2 D2 E2 F2) %.

Inversion lemmas

Proving invertability is an application of both cut and identity; it establishes that that for some rules, whenver the conclusion is true then the premises are always true as well.

In general, negative propositions are invertible on the right and positive propositions are invertible on the left, though in unfocused intutionstic logic up and down are invertible in both directions and both variants of conjunction are invertible on the right. This is not the full set of inversion lemmas, just the ones we needed.

%sort invupR {_ true (up P)} {_ true P} %.
%term _
  %pi (invupR D F)
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) EP))
  %<- (cut (up P) D (upL ([h] EP h)) F) %.
%mode invupR %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (invupR _ _) %.
%total [] (invupR _ _) %.
%sort invupL {_ %pi (hyp (up P)) %-> (conc J)} {_ %pi (hyp P) %-> (conc J)} %.
%term _
  %pi (invupL ([h] D h) ([h] F h))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) EP))
  %<- ({h hyp P} cut (up P) (upR (EP h)) D (F h)) %.
%mode invupL %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (invupL _ _) %.
%total [] (invupL _ _) %.
%sort invdownR {_ true (down P)} {_ true P} %.
%term _
  %pi (invdownR D F)
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) EP))
  %<- (cut (down P) D (downL ([h] EP h)) F) %.
%mode invdownR %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (invdownR _ _) %.
%total [] (invdownR _ _) %.
%sort invdownL {_ %pi (hyp (down P)) %-> (conc J)} {_ %pi (hyp P) %-> (conc J)} %.
%term _
  %pi (invdownL ([h] D h) ([h] F h))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) EP))
  %<- ({h hyp P} cut (down P) (downR (EP h)) D (F h)) %.
%mode invdownL %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (invdownL _ _) %.
%total [] (invdownL _ _) %.
%sort inv*R {_ true (P1 * P2)} {_ true P1} {_ true P2} %.
%term _
  %pi (inv*R D F1 F2)
  %<- (identity (P1 * P2) (%the (%pi (hyp (P1 * P2)) %-> (true (P1 * P2))) E))
  %<- (identity P1 (%the (%pi (hyp P1) %-> (true P1)) E1))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) E2))
  %<- (cut (P1 * P2) D (*L ([h1] [h2] E1 h1)) F1)
  %<- (cut (P1 * P2) D (*L ([h1] [h2] E2 h2)) F2) %.
%mode inv*R %in %out %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (inv*R _ _ _) %.
%total [] (inv*R _ _ _) %.
%sort inv&R {_ true (N1 & N2)} {_ true N1} {_ true N2} %.
%term _
  %pi (inv&R D F1 F2)
  %<- (identity (N1 & N2) (%the (%pi (hyp (N1 & N2)) %-> (true (N1 & N2))) E))
  %<- (identity N1 (%the (%pi (hyp N1) %-> (true N1)) E1))
  %<- (identity N2 (%the (%pi (hyp N2) %-> (true N2)) E2))
  %<- (cut (N1 & N2) D (&L1 ([h1] E1 h1)) F1)
  %<- (cut (N1 & N2) D (&L2 ([h2] E2 h2)) F2) %.
%mode inv&R %in %out %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (inv&R _ _ _) %.
%total [] (inv&R _ _ _) %.
%sort inv-oR {_ true (P -o N)} {_ %pi (hyp P) %-> (true N)} %.
%term _
  %pi (inv-oR D ([h] F h))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) EP))
  %<- (identity N (%the (%pi (hyp N) %-> (true N)) EN))
  %<- ({h' hyp P} cut (P -o N) D (-oL (EP h') ([h] EN h)) (F h')) %.
%mode inv-oR %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (inv-oR _ _) %.
%total [] (inv-oR _ _) %.
%sort invcircR {_ true (circ P)} {_ lax P} %.
%term _
  %pi (invcircR D F)
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) E))
  %<- (lcut (circ P) (laxR D) (circL ([h'] laxR (E h'))) F) %.
%mode invcircR %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (invcircR _ _) %.
%total [] (invcircR _ _) %.
%sort invcircL {_ %pi (hyp (circ P)) %-> (lax C)} {_ %pi (hyp P) %-> (lax C)} %.
%term _
  %pi (invcircL D F)
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) E))
  %<- ({h' hyp P} cut (circ P) (circR (laxR (E h'))) ([h] D h) (F h')) %.

Correctness of translation

Equivalence

This is an interesting theorem, because it captures the idea that the translation, while nondeterminstic (a single source logic proposition corresponds to many target logic propositions), is not significant (all target logic propositions in the image of a single source logic proposition are equivalent). Equivalence will be necessary for the completeness theorem in order to translate the identity rule in the source logic into the target logic.

If $M~\texttt{trans}~A_1$ and $\Gamma \vdash A_1~true$ and $M~\texttt{trans}~A_2$ , then $\Gamma \vdash A_2~true$ .

The theorem is proved by simultaneous induction on the unordered pair of the two translations, and therefore suffers from an annoying lack of expressivity in the STELF termination checker. There is no way to express the argument “the unordered pair of X and Y gets smaller,” and so when we need to switch the position of the arguments in the lambda case, we cannot convince STELF that something is getting smaller. The only way to do this seems to be to cut and paste the lemma into two copies which then call each other at the critical case; STELF can handle the unordered pair as mutual induction.

First we need a minor strenghtening lemma first, that expresses that if a hypothesis translated from true, then it isn’t needed.

%sort trans-equiv-str {_ %pi (hyp A) %-> (conc J)} {_ trans _ tt' pos A} {_ conc J} %.
%term _
  %pi (trans-equiv-str D (t-+ (t+- TR)) E)
  %<- (invdownL D D')
  %<- (invupL D' D'')
  %<- (trans-equiv-str D'' TR E) %.
%term _ %pi (trans-equiv-str D (t-+ t-true) E) %<- (cut (down top) (downR topR) D E) %.
%term _ %pi (trans-equiv-str D t+true E) %<- (cut 1 1R D E) %.
%mode trans-equiv-str %in %in %out %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (trans-equiv-str _ _ _) %.
%total TR (trans-equiv-str _ TR _) %.
%sort trans-equiv {_ trans _ M _ A1} {_ true A1} {_ trans _ M _ A2} {_ true A2} %.
%sort trans-equivX {_ trans _ M _ A1} {_ true A1} {_ trans _ M _ A2} {_ true A2} %.
%mode trans-equiv %in %in %in %out %.
%mode trans-equivX %in %in %in %out %.
%term _
  %pi (trans-equiv (t+- T1) D1 T2 D2)
  %<- (invupR D1 D1')
  %<- (trans-equiv T1 D1' T2 D2) %.
%term _
  %pi (trans-equiv (t-+ T1) D1 T2 D2)
  %<- (invdownR D1 D1')
  %<- (trans-equiv T1 D1' T2 D2) %.
%term _ %pi (trans-equiv T1 D1 (t+- T2) (upR D2)) %<- (trans-equiv T1 D1 T2 D2) %.
%term _ %pi (trans-equiv T1 D1 (t-+ T2) (downR D2)) %<- (trans-equiv T1 D1 T2 D2) %.
%term _ trans-equiv tatom D tatom D %.
%term _ trans-equiv t+true D t+true D %.
%term _ trans-equiv t+true D t-true topR %.
%term _ trans-equiv t-true D t+true 1R %.
%term _ trans-equiv t-true D t-true D %.
%term _ %pi (trans-equiv t+false D _ E) %<- (cut 0 D ([h] 0L h) E) %.
%term _
  %pi (trans-equiv (t+not T) D t+false E)
  %<- (inv-oR D (%the (%pi (hyp P1) %-> (true (up 0))) Da))
  %<- ({h} invupR (Da h) (Db h))
  %<- (trans-equiv-str Db T E) %.
%term _
  %pi (trans-equiv (t+and Ta Tb) D (t+and Sa Sb) (*R Ea Eb))
  %<- (inv*R D Da Db)
  %<- (trans-equiv Ta Da Sa Ea)
  %<- (trans-equiv Tb Db Sb Eb) %.
%term _
  %pi (trans-equiv (t-and Ta Tb) D (t+and Sa Sb) (*R Ea Eb))
  %<- (inv&R D Da Db)
  %<- (trans-equiv Ta Da Sa Ea)
  %<- (trans-equiv Tb Db Sb Eb) %.
%term _
  %pi (trans-equiv (t+and Ta Tb) D (t-and Sa Sb) (&R Ea Eb))
  %<- (inv*R D Da Db)
  %<- (trans-equiv Ta Da Sa Ea)
  %<- (trans-equiv Tb Db Sb Eb) %.
%term _
  %pi (trans-equiv (t-and Ta Tb) D (t-and Sa Sb) (&R Ea Eb))
  %<- (inv&R D Da Db)
  %<- (trans-equiv Ta Da Sa Ea)
  %<- (trans-equiv Tb Db Sb Eb) %.
%term _
  %pi (trans-equiv (t+or Ta Tb) D (t+or Sa Sb) E)
  %<- (identity P1 (%the (%pi (hyp P1) %-> (true P1)) D1))
  %<- ({h1} trans-equiv Ta (D1 h1) Sa (E1 h1))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D2))
  %<- ({h2} trans-equiv Tb (D2 h2) Sb (E2 h2))
  %<- (cut (P1 + P2) D (+L ([h1] +R1 (E1 h1)) ([h2] +R2 (E2 h2))) E) %.
%term _
  %pi (trans-equiv (t-imp Ta Tb) D (t-imp Sa Sb) (-oR E))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D1))
  %<- ({h1} trans-equivX Sa (D1 h1) Ta (E1 h1))
  %<- (inv-oR D (%the (%pi (hyp P1) %-> (true N1)) D2))
  %<- ({h1} trans-equiv Tb (D2 h1) Sb (E2 h1))
  %<- ({h2} cut P1 (E1 h2) ([h1] E2 h1) (%the (true N2) (E h2))) %.
%term _
  %pi (trans-equiv (t+not T) D (t+not S) (-oR E))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D1))
  %<- ({h1} trans-equivX S (D1 h1) T (E1 h1))
  %<- (inv-oR D (%the (%pi (hyp P1) %-> (true (up 0))) D2))
  %<- ({h2} cut P1 (E1 h2) ([h1] D2 h1) (%the (true (up 0)) (E h2))) %.
%term _
  %pi (trans-equiv (t+circ T) (%the (true (circ P)) D) (t+circ S) (circR F))
  %<- (invcircR D (%the (lax P) D1))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) D2))
  %<- ({h1} trans-equiv T (D2 h1) S (%the (true B) (E h1)))
  %<- (lcut P D1 ([h] laxR (E h)) F) %.
%% Cut and paste:
%term _
  %pi (trans-equivX (t+- T1) D1 T2 D2)
  %<- (invupR D1 D1')
  %<- (trans-equivX T1 D1' T2 D2) %.
%term _
  %pi (trans-equivX (t-+ T1) D1 T2 D2)
  %<- (invdownR D1 D1')
  %<- (trans-equivX T1 D1' T2 D2) %.
%term _ %pi (trans-equivX T1 D1 (t+- T2) (upR D2)) %<- (trans-equivX T1 D1 T2 D2) %.
%term _ %pi (trans-equivX T1 D1 (t-+ T2) (downR D2)) %<- (trans-equivX T1 D1 T2 D2) %.
%term _ trans-equivX tatom D tatom D %.
%term _ trans-equivX t+true D t+true D %.
%term _ trans-equivX t+true D t-true topR %.
%term _ trans-equivX t-true D t+true 1R %.
%term _ trans-equivX t-true D t-true D %.
%term _ %pi (trans-equivX t+false D _ E) %<- (cut 0 D ([h] 0L h) E) %.
%term _
  %pi (trans-equivX (t+not T) D t+false E)
  %<- (inv-oR D (%the (%pi (hyp P1) %-> (true (up 0))) Da))
  %<- ({h} invupR (Da h) (Db h))
  %<- (trans-equiv-str Db T E) %.
%term _
  %pi (trans-equivX (t+and Ta Tb) D (t+and Sa Sb) (*R Ea Eb))
  %<- (inv*R D Da Db)
  %<- (trans-equivX Ta Da Sa Ea)
  %<- (trans-equivX Tb Db Sb Eb) %.
%term _
  %pi (trans-equivX (t-and Ta Tb) D (t+and Sa Sb) (*R Ea Eb))
  %<- (inv&R D Da Db)
  %<- (trans-equivX Ta Da Sa Ea)
  %<- (trans-equivX Tb Db Sb Eb) %.
%term _
  %pi (trans-equivX (t+and Ta Tb) D (t-and Sa Sb) (&R Ea Eb))
  %<- (inv*R D Da Db)
  %<- (trans-equivX Ta Da Sa Ea)
  %<- (trans-equivX Tb Db Sb Eb) %.
%term _
  %pi (trans-equivX (t-and Ta Tb) D (t-and Sa Sb) (&R Ea Eb))
  %<- (inv&R D Da Db)
  %<- (trans-equivX Ta Da Sa Ea)
  %<- (trans-equivX Tb Db Sb Eb) %.
%term _
  %pi (trans-equivX (t+or Ta Tb) D (t+or Sa Sb) E)
  %<- (identity P1 (%the (%pi (hyp P1) %-> (true P1)) D1))
  %<- ({h1} trans-equivX Ta (D1 h1) Sa (E1 h1))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D2))
  %<- ({h2} trans-equivX Tb (D2 h2) Sb (E2 h2))
  %<- (cut (P1 + P2) D (+L ([h1] +R1 (E1 h1)) ([h2] +R2 (E2 h2))) E) %.
%term _
  %pi (trans-equivX (t-imp Ta Tb) D (t-imp Sa Sb) (-oR E))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D1))
  %<- ({h1} trans-equiv Sa (D1 h1) Ta (E1 h1))
  %<- (inv-oR D (%the (%pi (hyp P1) %-> (true N1)) D2))
  %<- ({h1} trans-equivX Tb (D2 h1) Sb (E2 h1))
  %<- ({h2} cut P1 (E1 h2) ([h1] E2 h1) (%the (true N2) (E h2))) %.
%term _
  %pi (trans-equivX (t+not T) D (t+not S) (-oR E))
  %<- (identity P2 (%the (%pi (hyp P2) %-> (true P2)) D1))
  %<- ({h1} trans-equiv S (D1 h1) T (E1 h1))
  %<- (inv-oR D (%the (%pi (hyp P1) %-> (true (up 0))) D2))
  %<- ({h2} cut P1 (E1 h2) ([h1] D2 h1) (%the (true (up 0)) (E h2))) %.
%term _
  %pi (trans-equivX (t+circ T) (%the (true (circ P)) D) (t+circ S) (circR F))
  %<- (invcircR D (%the (lax P) D1))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) D2))
  %<- ({h1} trans-equivX T (D2 h1) S (%the (true B) (E h1)))
  %<- (lcut P D1 ([h] laxR (E h)) F) %.
%worlds (bl_atmpos bl_atmneg bl_hyp) (trans-equiv _ _ _ _) (trans-equivX _ _ _ _) %.
%total [(T1 T2) (S1 S2)] (trans-equiv T1 _ S1 _) (trans-equivX S2 _ T2 _) %.

Soundness

If $\Gamma \vdash J$ and $\Gamma'~\texttt{trans}~\Gamma$ and $\Delta~\texttt{trans}~J$ , then $\Gamma' \vdash \Delta$ (trans-sound)

Proved by induction on the target logic derivation $\Gamma \vdash J$ .

%sort trans-sound {_ conc C} {_ trans-conc Mt C' C} {_ conc' Mc C'} %.
%mode trans-sound %in %in %out %.

Every case of translating a left rule needs to translate a hypothesis, and we can usefully predict the form of the output, except in the cases where the reverse translation is not determinstic. The first lemma, trans-init, is essentally just an output factoring lemma because the case of translating atomic formula really consists of two cases, the positive atoms and the negative atoms, and this triggers STELF’s output freeness check.

The second nondetermistic case is where we are translating an implication in the target logic and may encounter either an implication or a negation in the source logic. This case (trans-imp) becomes mutually inductive with the main theorem, and establishes a pattern that will continue in the completeness theorem.

One case in particular is worth pointing out. We have $\Gamma \vdash {\uparrow} 0~true$ in the target logic using the rule upR, which gives us a subderivation $\Gamma \vdash 0~true$ , and we are translating into a contradiction $\Gamma' \vdash$ in the target logic (let $\Gamma'$ be the translated $\Gamma$ ).

By the induction hypothesis we have $\Gamma' \vdash \mathsf{false}$ , which we have defined to be $\Gamma' \vdash \neg \mathsf{true}$ . We need to prove, however, $\Gamma' \vdash$ . Let me know if I’m wrong, but the only way I could figure out how to do this was by using the cut rule in the source logic, which means that we do not get cut elimination “for free” in the source logic by virtue of cut admissibility in the target logic.

$\frac {\frac {~~~~} {\Gamma \vdash \neg\mathsf{true}} {i.h.}\qquad \frac {\frac{}{\Gamma, \neg\mathsf{true}\vdash\mathsf{true}}{\mathsf{true}R}} {\Gamma, \neg\mathsf{true}\vdash}} {\neg}L {\Gamma \vdash} {cut}$

This awkwardness is a result of the slight mismatch between falsehood in the target logic and contradiction in the source logic, and is part of the reason we didn’t include falsehood as a primitive in the source logic.

%sort trans-init {_ trans Mt A' S (atom Q)} {_ hyp' A'} {_ hyp' (atom' Q)} %.
%term _ trans-init tatom H H %.
%mode trans-init %in %in %out %.
%worlds (bl_atmpos bl_atmneg bl_trans-soundhyp) (trans-init _ _ _) %.
%total [] (trans-init _ _ _) %.
%term _
  %pi (trans-sound (init+ H) (tc tatom) (id' H''))
  %<- (trans-soundhyp H T H')
  %<- (trans-init T H' H'') %.
%term _
  %pi (trans-sound (init- H) (tc tatom) (id' H''))
  %<- (trans-soundhyp H T H')
  %<- (trans-init T H' H'') %.
%term _ %pi (trans-sound (laxR D) (tclax T) (circR' E)) %<- (trans-sound D (tc T) E) %.
%term _ %pi (trans-sound (upR D) (tc (t+- T)) E) %<- (trans-sound D (tc T) E) %.
%term _
  %pi (trans-sound (upR D) tc# (cut' E ([h] notL' trueR' h)))
  %<- (trans-sound D (tc t+false) E) %.
%term _
  %pi (trans-sound (upL D H) T (E H'))
  %<- (trans-soundhyp H (t+- Th) H')
  %<- ({h} {h'} %pi (trans-soundhyp h Th h') %-> (trans-sound (D h) T (%the (conc' M C) (E h')))) %.
%term _ %pi (trans-sound (downR D) (tc (t-+ T)) E) %<- (trans-sound D (tc T) E) %.
%term _
  %pi (trans-sound (downL D H) T (E H'))
  %<- (trans-soundhyp H (t-+ Th) H')
  %<- ({h} {h'} %pi (trans-soundhyp h Th h') %-> (trans-sound (D h) T (%the (conc' M C) (E h')))) %.
%term _ trans-sound topR (tc t-true) trueR' %.
%term _ trans-sound 1R (tc t+true) trueR' %.
%term _ %pi (trans-sound (0L H) _ (notL' trueR' H')) %<- (trans-soundhyp H t+false H') %.
%term _
  %pi (trans-sound (0L H) _ (weakR' (notL' trueR' H')))
  %<- (trans-soundhyp H t+false H') %.
%term _
  %pi (trans-sound (*R D1 D2) (tc (t+and T1 T2)) (/\R' E1 E2))
  %<- (trans-sound D1 (tc T1) E1)
  %<- (trans-sound D2 (tc T2) E2) %.
%term _
  %pi (trans-sound (*L D H) T (/\L' ([h1] [h2] E h1 h2) H'))
  %<- (trans-soundhyp H (t+and Th1 Th2) H')
  %<- ({h1} {h1'}
  %pi (trans-soundhyp h1 Th1 h1')
  %-> ({h2} {h2'} %pi (trans-soundhyp h2 Th2 h2') %-> (trans-sound (D h1 h2) T (E h1' h2')))) %.
%term _
  %pi (trans-sound (&R D1 D2) (tc (t-and T1 T2)) (/\R' E1 E2))
  %<- (trans-sound D1 (tc T1) E1)
  %<- (trans-sound D2 (tc T2) E2) %.
%term _
  %pi (trans-sound (&L1 D H) T (/\L' ([h1] [h2] E h1) H'))
  %<- (trans-soundhyp H (t-and Th _) H')
  %<- ({h} {h'} %pi (trans-soundhyp h Th h') %-> (trans-sound (D h) T (E h'))) %.
%term _
  %pi (trans-sound (&L2 D H) T (/\L' ([h1] [h2] E h2) H'))
  %<- (trans-soundhyp H (t-and _ Th) H')
  %<- ({h} {h'} %pi (trans-soundhyp h Th h') %-> (trans-sound (D h) T (E h'))) %.
%term _ %pi (trans-sound (+R1 D) (tc (t+or T _)) (\/R1' E)) %<- (trans-sound D (tc T) E) %.
%term _ %pi (trans-sound (+R2 D) (tc (t+or _ T)) (\/R2' E)) %<- (trans-sound D (tc T) E) %.
%term _
  %pi (trans-sound (+L D1 D2 H) T (\/L' E1 E2 H'))
  %<- (trans-soundhyp H (t+or Th1 Th2) H')
  %<- ({h1} {h1'} %pi (trans-soundhyp h1 Th1 h1') %-> (trans-sound (D1 h1) T (E1 h1')))
  %<- ({h2} {h2'} %pi (trans-soundhyp h2 Th2 h2') %-> (trans-sound (D2 h2) T (E2 h2'))) %.
%term _
  %pi (trans-sound (-oR D) (tc (t-imp T1 T2)) (=>R' E))
  %<- ({h} {h'} %pi (trans-soundhyp h T1 h') %-> (trans-sound (D h) (tc T2) (E h'))) %.
%term _
  %pi (trans-sound (-oR D) (tc (t+not T)) (notR' E))
  %<- ({h hyp A} {h' hyp' A'} %pi (trans-soundhyp h T h') %-> (trans-sound (D h) tc# (E h'))) %.
%sort trans-imp {D conc C} {_ idconc D (-oL (%the (true A1) D1) (%the (%pi (hyp A2) %-> (conc C)) D2) H)} {_ trans-conc Mt C' C} {_ trans Mh A' neg (A1 -o A2)} {_ hyp' A'} {_ conc' Md C'} %.
%mode trans-imp %in %in %in %in %in %out %.
%term _
  %pi (trans-imp (-oL D1 D2 H) idconc/refl T (t-imp Th1 Th2) H' (=>L' E1 E2 H'))
  %<- (trans-sound D1 (tc Th1) E1)
  %<- ({h} {h'} %pi (trans-soundhyp h Th2 h') %-> (trans-sound (D2 h) T (E2 h'))) %.
%term _
  %pi (trans-imp (-oL D1 D2 H) idconc/refl T (t+not Th) (%the (hyp' (not' A')) H') (weakR' (notL' E1 H')))
  %<- (trans-sound D1 (tc Th) (%the (true' Md A') E1)) %.
%term _
  %pi (trans-imp (-oL D1 D2 H) idconc/refl tc# (t+not Th) (%the (hyp' (not' A')) H') (notL' E1 H'))
  %<- (trans-sound D1 (tc Th) (%the (true' Md A') E1)) %.
%term _
  %pi (trans-sound (-oL D1 D2 H) T F)
  %<- (trans-soundhyp H Th H')
  %<- (trans-imp (-oL D1 D2 H) idconc/refl T Th H' F) %.
%term _ %pi (trans-sound (circR D) (tc (t+circ T)) E) %<- (trans-sound D (tclax T) E) %.
%term _
  %pi (trans-sound (circL D H) (tclax T) (circL' E H'))
  %<- (trans-soundhyp H (t+circ Th) H')
  %<- ({h} {h'} %pi (trans-soundhyp h Th h') %-> (trans-sound (D h) (tclax T) (E h'))) %.
%worlds (bl_atmpos bl_atmneg bl_trans-soundhyp) (trans-sound _ _ _) (trans-imp _ _ _ _ _ _) %.
%total (D E) (trans-imp E _ _ _ _ _) (trans-sound D _ _) %.

Completeness

If $\Gamma' \vdash \Delta$ and $\Gamma'~\texttt{trans}~\Gamma$ and $\Delta~\texttt{trans}~J$ , then $\Gamma \vdash J$ .

By lexographic induction on the first derivation’s metric and then the second derivation’s metric. For every left rule, we need a mutually inductive lemma that strips off any unnecessary shifts from the translation of the hypothesis; within these lemmas, the first derivation will always stay the same, but the derivation of the translation of the hypothesis will get smaller.

%sort trans-compl {Td} {Tt} {_ conc' Td D} {_ trans-conc Tt D J} {_ conc J} %.
%mode trans-compl %in %in %in %in %out %.
%inline trans-compl' [d conc' Td D] [t trans-conc Tt D J] [e conc J] trans-compl Td Tt d t e %.

Shifts

%term _ %pi (trans-compl' D (tc (t+- T)) (upR E)) %<- (trans-compl' D (tc T) E) %.
%term _ %pi (trans-compl' D (tc (t-+ T)) (downR E)) %<- (trans-compl' D (tc T) E) %.

Truth

%term _ trans-compl' trueR' (tc t+true) 1R %.
%term _ trans-compl' trueR' (tc t-true) topR %.

Conjunction

%term _
  %pi (trans-compl' (/\R' D1 D2) (tc (t+and T1 T2)) (*R E1 E2))
  %<- (trans-compl' D1 (tc T1) E1)
  %<- (trans-compl' D2 (tc T2) E2) %.
%term _
  %pi (trans-compl' (/\R' D1 D2) (tc (t-and T1 T2)) (&R E1 E2))
  %<- (trans-compl' D1 (tc T1) E1)
  %<- (trans-compl' D2 (tc T2) E2) %.
%sort trans-andL {TD} {Th} {_ id TD (x Td)} {_ %pi (hyp' M1) %-> (hyp' M2) %-> (conc' Td D)} {_ trans-conc Tt D J} {_ trans Th (M1 /\ M2) S A} {_ %pi (hyp A) %-> (conc J)} %.
%mode trans-andL %in %in %in %in %in %in %out %.
%term _
  %pi (trans-andL _ _ id/refl (%the (%pi (hyp' M1) %-> (hyp' M2) %-> (conc' Td D')) D) (%the (trans-conc Tt D' J) T) (t-and T1 T2) ([h] &L1 ([h1] &L2 ([h2] E h1 h2) h) h))
  %<- ({h1'} {h1}
  %pi (trans-complhyp h1' T1 h1)
  %-> ({h2'} {h2} %pi (trans-complhyp h2' T2 h2) %-> (trans-compl' (D h1' h2') T (E h1 h2)))) %.
%term _
  %pi (trans-andL _ _ id/refl (%the (%pi (hyp' M1) %-> (hyp' M2) %-> (conc' Td D')) D) (%the (trans-conc Tt D' J) T) (t+and T1 T2) ([h] *L ([h1] [h2] E h1 h2) h))
  %<- ({h1'} {h1}
  %pi (trans-complhyp h1' T1 h1)
  %-> ({h2'} {h2} %pi (trans-complhyp h2' T2 h2) %-> (trans-compl' (D h1' h2') T (E h1 h2)))) %.
%term _ %pi (trans-andL _ _ Id D T (t+- Th) (upL E)) %<- (trans-andL _ _ Id D T Th E) %.
%term _ %pi (trans-andL _ _ Id D T (t-+ Th) (downL E)) %<- (trans-andL _ _ Id D T Th E) %.
%term _
  %pi (trans-compl' (/\L' D H') T (E H))
  %<- (trans-complhyp H' Th (%the (hyp A) H))
  %<- (trans-andL _ _ id/refl D T Th (%the (%pi (hyp A) %-> (conc D')) E)) %.

Disjunction

%term _
  %pi (trans-compl' (\/R1' (%the (true' Tt M1) D)) (tc (t+or T1 _)) (+R1 E))
  %<- (trans-compl' D (tc T1) E) %.
%term _
  %pi (trans-compl' (\/R2' (%the (true' Tt M2) D)) (tc (t+or _ T2)) (+R2 E))
  %<- (trans-compl' D (tc T2) E) %.
%sort trans-orL {TD} {Th} {_ id TD (Td1 | Td2)} {_ %pi (hyp' M1) %-> (conc' Td1 D')} {_ %pi (hyp' M2) %-> (conc' Td2 D')} {_ trans-conc Tt D' J} {_ trans Th (M1 \/ M2) S A} {_ %pi (hyp A) %-> (conc J)} %.
%mode trans-orL %in %in %in %in %in %in %in %out %.
%term _
  %pi (trans-orL _ _ id/refl D1 D2 T (t+or Th1 Th2) (+L ([h1] E1 h1) ([h2] E2 h2)))
  %<- ({h1' hyp' M1} {h1 hyp P1}
  %pi (trans-complhyp h1' Th1 h1)
  %-> (trans-compl' (D1 h1') T (%the (conc J) (E1 h1))))
  %<- ({h2' hyp' M2} {h2 hyp P2}
  %pi (trans-complhyp h2' Th2 h2)
  %-> (trans-compl' (D2 h2') T (%the (conc J) (E2 h2)))) %.
%term _
  %pi (trans-orL _ _ id/refl D1 D2 T (t+- Th) (upL E))
  %<- (trans-orL _ _ id/refl D1 D2 T Th E) %.
%term _
  %pi (trans-orL _ _ id/refl D1 D2 T (t-+ Th) (downL E))
  %<- (trans-orL _ _ id/refl D1 D2 T Th E) %.
%term _
  %pi (trans-compl' (\/L' D1 D2 H') T (E H))
  %<- (trans-complhyp H' Th H)
  %<- (trans-orL _ _ id/refl D1 D2 T Th E) %.

Implication

%term _
  %pi (trans-compl' (=>R' (%the (%pi (hyp' M1) %-> (true' Tt M2)) D)) (tc (t-imp T1 T2)) (-oR E))
  %<- ({h'} {h} %pi (trans-complhyp h' T1 h) %-> (trans-compl' (D h') (tc T2) (E h))) %.
%sort trans-impL {TD} {Th} {_ id TD (Td1 | Td2)} {_ true' Td1 M1} {_ %pi (hyp' M2) %-> (conc' Td2 D')} {_ trans-conc Tt D' J} {_ trans Th (M1 => M2) S A} {_ %pi (hyp A) %-> (conc J)} %.
%mode trans-impL %in %in %in %in %in %in %in %out %.
%term _
  %pi (trans-impL _ _ id/refl (%the (true' Td1 M1) D1) (%the (%pi (hyp' M2) %-> (conc' Td2 D')) D2) (%the (trans-conc Mt D' J) T) (t-imp T1 T2) (-oL E1 ([h] E2 h)))
  %<- (trans-compl' D1 (tc T1) (%the (true P) E1))
  %<- ({h' hyp' M2} {h hyp N} {t trans-complhyp h' T2 h} trans-compl' (D2 h') T (%the (conc J) (E2 h))) %.
%term _
  %pi (trans-impL _ _ id/refl D1 D2 T (t+- Th) (upL E))
  %<- (trans-impL _ _ id/refl D1 D2 T Th E) %.
%term _
  %pi (trans-impL _ _ id/refl D1 D2 T (t-+ Th) (downL E))
  %<- (trans-impL _ _ id/refl D1 D2 T Th E) %.
%term _
  %pi (trans-compl' (=>L' D1 D2 (%the (hyp' (M1 => M2)) H')) T (E H))
  %<- (trans-complhyp H' Th (%the (hyp A) H))
  %<- (trans-impL _ _ id/refl D1 D2 T Th E) %.

Negation

%term _
  %pi (trans-compl' (notR' (%the (%pi (hyp' tt') %-> (# _)) D)) (tc t+false) G)
  %<- ({h'} {h} %pi (trans-complhyp h' t+true h) %-> (trans-compl' (D h') tc# (E h)))
  %<- (cut 1 1R ([h] E h) F)
  %<- (invupR F G) %.
%term _
  %pi (trans-compl' (notR' (%the (%pi (hyp' M) %-> (# _)) D)) (tc (t+not T)) (-oR ([h] E h)))
  %<- ({h'} {h} %pi (trans-complhyp h' T h) %-> (trans-compl' (D h') tc# (E h))) %.
%sort trans-notL {TD} {Tt} {_ id TD (x Td)} {_ true' Td M} {_ trans Tt (not' M) S A} {_ %pi (hyp A) %-> (true (up 0))} %.
%mode trans-notL %in %in %in %in %in %out %.
%term _
  %pi (trans-notL _ _ id/refl (%the (true' Td M) D) (t+not T) (-oL E (upL 0L)))
  %<- (trans-compl' D (tc T) (%the (true P) E)) %.
%term _ trans-notL _ _ id/refl D t+false 0L %.
%term _ %pi (trans-notL _ _ Id D (t+- T) (upL E)) %<- (trans-notL _ _ Id D T E) %.
%term _ %pi (trans-notL _ _ Id D (t-+ T) (downL E)) %<- (trans-notL _ _ Id D T E) %.
%term _
  %pi (trans-compl' (notL' (%the (true' Td M) D) (%the (hyp' (not' M)) H')) tc# (E H))
  %<- (trans-complhyp H' Th (%the (hyp A) H))
  %<- (trans-notL _ _ id/refl D Th E) %.

Lax modality

%term _
  %pi (trans-compl' (circR' D) (tc (t+circ T)) (circR (laxR E)))
  %<- (trans-compl' D (tc T) E) %.
%term _ %pi (trans-compl' (circR' D) (tclax T) (laxR E)) %<- (trans-compl' D (tc T) E) %.
%sort trans-circL {TD} {Th} {_ id TD (x Td)} {_ %pi (hyp' M) %-> (true' Td (circ' D'))} {_ trans Tt D' S C} {_ trans Th (circ' M) Sh A} {_ %pi (hyp A) %-> (lax C)} %.
%mode trans-circL %in %in %in %in %in %in %out %.
%term _
  %pi (trans-circL _ _ id/refl D T (t+circ Th) (circL E))
  %<- ({h' hyp' M} {h hyp P} {t trans-complhyp h' Th h} trans-compl' (D h') (tclax T) (%the (lax C) (E h))) %.
%term _ %pi (trans-circL _ _ Id D T (t+- Th) (upL F)) %<- (trans-circL _ _ Id D T Th F) %.
%term _ %pi (trans-circL _ _ Id D T (t-+ Th) (downL F)) %<- (trans-circL _ _ Id D T Th F) %.
%term _
  %pi (trans-compl' (circL' (%the (%pi (hyp' M) %-> (true' Td (circ' D'))) D) H') (tc (t+circ (%the (trans Tt D' pos J) T))) (circR (E H)))
  %<- (trans-complhyp H' Th (%the (hyp A) H))
  %<- (trans-circL _ _ id/refl D T Th E) %.
%term _
  %pi (trans-compl' (circL' (%the (%pi (hyp' M) %-> (true' Td (circ' D'))) D) H') (tclax (%the (trans Tt D' S J) T)) (E H))
  %<- (trans-complhyp H' Th (%the (hyp A) H))
  %<- (trans-circL _ _ id/refl D T Th E) %.

Structural Rules

For translating a cut, we need to come up with a translation of a source logc expression to a target logic expression; we have already established this was possible when we proved can-trans to show that translation was left-total.

%term _
  %pi (trans-compl' (cut' (%the (true' _ M) Da) Dc) T F)
  %<- (can-trans M (%the (trans _ M S A) TRa))
  %<- (trans-compl' Da (tc TRa) (%the (true A) Ea))
  %<- ({h'} {h} %pi (trans-complhyp h' TRa h) %-> (trans-compl' (Dc h') T (Ec h)))
  %<- (cut A Ea Ec F) %.

Due to the mismatch between the lax judgment and the circle, we need three cases for translating identity. The first case is the most important one and is straightforward, however: we are translating $\Gamma', M \vdash M$ and need to show $\Gamma, A_M \vdash A_M~true$ , where $M~\texttt{trans}~A_M$ .

Identity is a terminal rule, so we will not use induction here. We know because $M$ is a hypothesis that there is a hypothesis $A$ such that $M~\texttt{trans}~A$ , and so by the identity principle we can prove $\Gamma, A \vdash A~true$ ; then, trans-equiv allows us to prove $\Gamma, A_M \vdash A_M~true$ , which is what we actually need.

%term _
  %pi (trans-compl' (id' (%the (hyp' M) H')) (tc (%the (trans _ M S Am) T)) E)
  %<- (trans-complhyp H' Th (%the (hyp A) H))
  %<- (identity A (%the (%pi (hyp A) %-> (true A)) D2))
  %<- (trans-equiv Th (D2 H) T (%the (true Am) E)) %.

When we are translating to a lax judgment in the target language, what we get out of the translation isn’t exactly what we want, we need $\Gamma \vdash A~lax$ but the best we can get is $\Gamma \vdash {\bigcirc}P~true$ or $\Gamma \vdash {\bigcirc}{\downarrow}N~true$ . However, we can use inversion lemmas (and lax cut, in the second case) to get what we need.

%term _
  %pi (trans-compl' (id' (%the (hyp' (circ' M)) H')) (tclax (%the (trans _ M pos Pm) T)) F)
  %<- (trans-complhyp H' Th (%the (hyp P) H))
  %<- (identity P (%the (%pi (hyp P) %-> (true P)) D2))
  %<- (trans-equiv Th (D2 H) (t+circ T) (%the (true (circ Pm)) E))
  %<- (invcircR E (%the (lax Pm) F)) %.
%term _
  %pi (trans-compl' (id' (%the (hyp' (circ' M)) H')) (tclax (%the (trans _ M neg Nm) T)) G)
  %<- (trans-complhyp H' Th (%the (hyp N) H))
  %<- (identity N (%the (%pi (hyp N) %-> (true N)) D2))
  %<- (trans-equiv Th (D2 H) (t+circ (t-+ T)) (%the (true (circ (down Nm))) E))
  %<- (invcircR E (%the (lax (down Nm)) F))
  %<- (identity _ (%the (%pi (hyp Nm) %-> (true Nm)) Id))
  %<- (lcut _ F ([h] laxR (downL ([h'] Id h') h)) (%the (lax Nm) G)) %.
%term _
  %pi (trans-compl' (weakR' D) _ F)
  %<- (trans-compl' D tc# E)
  %<- (cut (up 0) E ([h] upL 0L h) F) %.
%worlds (bl_atmpos bl_atmneg bl_trans-complhyp) (trans-compl _ _ _ _ _) (trans-andL _ _ _ _ _ _ _) (trans-impL _ _ _ _ _ _ _ _) (trans-orL _ _ _ _ _ _ _ _) (trans-notL _ _ _ _ _ _) (trans-circL _ _ _ _ _ _ _) %.
%total {(D1 D2 D3 D4 D5 D6) (T1 T2 T3 T4 T5 T6)} (trans-compl D1 T1 _ _ _) (trans-andL D2 T2 _ _ _ _ _) (trans-orL D3 T3 _ _ _ _ _ _) (trans-impL D4 T4 _ _ _ _ _ _) (trans-notL D5 T5 _ _ _ _) (trans-circL D6 T6 _ _ _ _ _) %.