# Lax logic

 This is Literate TwelfCode: hereStatus: %% OK %% Output: here.

In this article, we will take a presentation of a logic very close to that of Fairtlough and Mendler's lax logic[1] and show a translation into a polarized version of Pfenning and Davies' judgmental reconstruction of lax logic.[2] 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 ThingsTM, 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.

1. Matt Fairtlough, Michael Mendler - Propositional lax logic
Inf. Comput. 137(1):1--33, Duluth, MN, USA,1997
Bibtex
Author : Matt Fairtlough, Michael Mendler
Title : Propositional lax logic
In : Inf. Comput. -
Date : 1997
2. Frank Pfenning, Rowan Davies - A judgmental reconstruction of modal logic
Mathematical. Structures in Comp. Sci. 11(4):511--540, New York, NY, USA,2001
Bibtex
Author : Frank Pfenning, Rowan Davies
Title : A judgmental reconstruction of modal logic
In : Mathematical. Structures in Comp. Sci. -
Address : New York, NY, USA
Date : 2001

## 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).

```metric : type.                          %name metric T.
o : metric.
x : metric -> metric.
| : metric -> metric -> metric.         %infix right 10 |.

id : metric -> metric -> type.          %name id ID.
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).

```polarity : type.			%name polarity S.
pos : polarity.
neg : polarity.
atm : polarity -> type.                 %name atm Q q.
%block bl_atmpos : block {qp:atm pos}.
%block bl_atmneg : block {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



However, rules are given for neither  nor . A reasonable approach seemed to be to define  as .

```prop' : type.                           %name prop' M.

atom'  : atm S -> prop'.
tt'    : prop'.
/\     : prop' -> prop' -> prop'.       %infix right 9 /\.
\/     : prop' -> prop' -> prop'.       %infix right 8 \/.
=>     : prop' -> prop' -> prop'.       %infix right 7 =>.
not'   : prop' -> prop'.
circ'  : prop' -> prop'.
ff'    : prop' = not' tt'.```

### Sequent calculus

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

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

```hyp' : prop' -> type.
%block bl_hyp' : some {M: prop'} block {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 ; we abbreviate conc' T conc-#' as # T.
• D = conc-true' M represents proving ; we abbreviate conc' T (conc-true' M) as true' T M.
```conseq' : type.                         %name conseq' D.
conc-# : conseq'.                       % Contradiction, length 0
conc-true' : prop' -> conseq'.          % Conclusion, length 1
conc' : metric -> conseq' -> type.

%abbrev # = [m] conc' m conc-#.
%abbrev 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 , and we need no rule for  as we defined it in terms of . 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: 

Our left conjunction rule: 

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

                      

                      

                                 

           

                      

#### Rules in Twelf

```trueR' : true' o tt'.
% no trueL'

/\R' : true' Tm M
-> true' Tn N
-> true' (Tm | Tn) (M /\ N).
/\L'  : (hyp' M -> hyp' N -> conc' T D)
-> (hyp' (M /\ N) -> conc' (x (x T)) D).

\/R1' : true' T M
-> true' (x T) (M \/ N).
\/R2' : true' T N
-> true' (x T) (M \/ N).
\/L' : (hyp' M -> conc' Tm D)
-> (hyp' N -> conc' Tn D)
-> (hyp' (M \/ N) -> conc' (x (Tm | Tn)) D).

=>R' : (hyp' M -> true' T N)
-> true' (x T) (M => N).
=>L' : true' Tm M
-> (hyp' N -> conc' Tn D)
-> (hyp' (M => N) -> conc' (x (Tm | Tn)) D).

notR' : (hyp' M -> # T)
-> (true' (x T) (not' M)).
notL' : true' T M
-> (hyp' (not' M) -> # (x (x T))).

circR' : true' T M
-> true' (x T) (circ' M).
circL' : (hyp' M -> true' T (circ' N))
-> (hyp' (circ' M) -> true' (x (x T)) (circ' N)).

id' : hyp' M -> true' o M.

cut' : true' Ta M
-> (hyp' M -> conc' T D)
-> conc' (Ta | T) D.

weakR' : # 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  but distinguishes between two different kinds of conjunction,  and , and two variants of  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 , because  expectes two positive things and  is negative. We could either write , or else we could write .

The full language of propositions is:







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

```prop : polarity -> type.                %name prop A.

atom : atm S -> prop S.
up : prop pos -> prop neg.
down : prop neg -> prop pos.
top : prop neg.
1 : prop pos.
0 : prop pos.
* : prop pos -> prop pos -> prop pos.   %infix right 9 *.
& : prop neg -> prop neg -> prop neg.   %infix right 8 &.
+ : prop pos -> prop pos -> prop pos.   %infix right 7 +.
-o : prop pos -> prop neg -> prop neg.  %infix right 6 -o.
circ : prop pos -> prop neg.```

### Sequent calculus

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

```hyp : prop S -> type.
%block bl_hyp : some {S: polarity} {A: prop S} block {h: hyp A}.```

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

```conseq : type.                          %name conseq J.
conc-lax : prop S -> conseq.            % A lax
conc-true : prop S -> conseq.           % A true
conc : conseq -> type.

%abbrev lax = [x] conc (conc-lax x).
%abbrev 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.

```idconc : conc C -> conc C' -> type.
idconc/refl : idconc D D.```

#### Rules on paper

                      

                                 

                      

           

           

                      

           

           

#### Rules in Twelf

```init+ : hyp (atom Qp) -> true (atom (Qp: atm pos)).
init- : hyp (atom Qn) -> true (atom (Qn: atm neg)).

laxR : true A
-> lax A.

upR : true P
-> true (up P).
upL : (hyp P -> conc J)
-> (hyp (up P) -> conc J).

downR : true N
-> true (down N).
downL : (hyp N -> conc J)
-> (hyp (down N) -> conc J).

1R : true 1.
% no 1L

*R : true P1
-> true P2
-> true (P1 * P2).
*L : (hyp P1 -> hyp P2 -> conc J)
-> (hyp (P1 * P2) -> conc J).

topR : true top.
% no topL

&R : true N1
-> true N2
-> true (N1 & N2).
&L1 : (hyp N1 -> conc J)
-> (hyp (N1 & N2) -> conc J).
&L2 : (hyp N2 -> conc J)
-> (hyp (N1 & N2) -> conc J).

% no 0R
0L : (hyp 0 -> conc J).

+R1 : true P1
-> true (P1 + P2).
+R2 : true P2
-> true (P1 + P2).
+L : (hyp P1 -> conc J)
-> (hyp P2 -> conc J)
-> (hyp (P1 + P2) -> conc J).

-oR : (hyp P -> true N)
-> true (P -o N).
-oL : true P
-> (hyp N -> conc J)
-> (hyp (P -o N) -> conc J).

circR : lax P
-> true (circ P).
circL : (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.

```trans : metric -> prop' -> {S} prop S -> type. %name trans TR.

t+- : trans T M pos P -> trans (x T) M neg (up P).
t-+ : trans T M neg N -> trans (x T) M pos (down N).

tatom : trans o (atom' Q) S (atom Q).
t+true : trans o tt' pos 1.
t-true : trans o tt' neg top.
t+false: trans o ff' pos 0.
t+and  : trans T1 M1 pos P1
-> trans T2 M2 pos P2
-> trans (T1 | T2) (M1 /\ M2) pos (P1 * P2).
t-and  : trans T1 M1 neg N1
-> trans T2 M2 neg N2
-> trans (T1 | T2) (M1 /\ M2) neg (N1 & N2).
t+or   : trans T1 M1 pos P1
-> trans T2 M2 pos P2
-> trans (T1 | T2) (M1 \/ M2) pos (P1 + P2).
t-imp  : trans T1 M1 pos P
-> trans T2 M2 neg N
-> trans (T1 | T2) (M1 => M2) neg (P -o N).
t+not  : trans T M pos P -> trans (x T) (not' M) neg (P -o up 0).
t+circ : 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.

```trans-conc : metric -> conseq' -> conseq -> type. %name trans-conc TC.

tc : trans-conc T (conc-true' M) (conc-true A) <- trans T M S A.
tc# : trans-conc o conc-# (conc-true (up 0)).
tclax : 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.
```trans-soundhyp : hyp H -> trans Mh H' S H -> hyp' H' -> type.
%mode trans-soundhyp +H' -T -H.

%block bl_trans-soundhyp
: some {M: metric}{S: polarity}{A: prop S}{A': prop'}{T: trans M A' S A}
block {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 _ _ _).

trans-complhyp : hyp' A -> trans Mt A S C -> hyp C -> type.
%mode trans-complhyp +H' -T -H.

%block bl_trans-complhyp
: some {M: metric}{A: prop'}{S: polarity}{C: prop S}{T: trans M A S C}
block {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  and , then ." However, if there is no  such that , 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).

Twelf 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 -T -M +S +A.
%mode trans-conc -T -D +J.
%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.

```can-switch+ : trans M A S (C: prop S) -> trans N A pos C' -> type.
- : can-switch+ T T.
- : can-switch+ T (t-+ T).
%mode can-switch+ +A -B.
%worlds (bl_atmpos | bl_atmneg) (can-switch+ _ _).
%total [] (can-switch+ _ _).

can-switch- : trans M A S' C -> trans N A neg C' -> type.
- : can-switch- T T.
- : can-switch- T (t+- T).
%mode can-switch- +A -B.
%worlds (bl_atmpos | bl_atmneg) (can-switch- _ _).
%total [] (can-switch- _ _).

can-trans : {A} trans M A S (C: prop S) -> type.
%mode can-trans +A -T.

- : can-trans (atom' Qp) tatom.
- : can-trans tt' t-true.
- : can-trans (A /\ B) (t-and T1' T2')
<- can-trans A T1
<- can-switch- T1 T1'
<- can-trans B T2
<- can-switch- T2 T2'.
- : can-trans (A \/ B) (t+or T1' T2')
<- can-trans A T1
<- can-switch+ T1 T1'
<- can-trans B T2
<- can-switch+ T2 T2'.
- : can-trans (A => B) (t-imp T1' T2')
<- can-trans A T1
<- can-switch+ T1 T1'
<- can-trans B T2
<- can-switch- T2 T2'.
- : can-trans (not' A) (t+not T')
<- can-trans A T
<- can-switch+ T T'.
- : 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 _).

can-trans-conc : {D} trans-conc T D J -> type.
%mode can-trans-conc +D -T.

- : can-trans-conc conc-# tc#.
- : 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 , there exists a derivation of .

The proof is by induction on the formula .

```identity : {A} (hyp A -> true A) -> type.
%mode identity +A -D.

- : identity (atom Q) init+.
- : identity (atom Q) init-.
- : identity (up P) ([h] upL ([h'] upR (D h')) h)
<- identity P (D: hyp P -> true P).
- : identity (down N) ([h] downL ([h'] downR (D h')) h)
<- identity N (D: hyp N -> true N).
- : identity top ([_] topR).
- : identity 1 ([_] 1R).
- : identity 0 ([h] 0L h).
- : identity (P1 * P2) ([h] *L ([h1][h2] *R (D1 h1) (D2 h2)) h)
<- identity P1 (D1: hyp P1 -> true P1)
<- identity P2 (D2: hyp P2 -> true P2).
- : identity (N1 & N2) ([h] &L1 ([h1] &L2 ([h2] &R (D1 h1) (D2 h2)) h) h)
<- identity N1 (D1: hyp N1 -> true N1)
<- identity N2 (D2: hyp N2 -> true N2).
- : identity (P1 + P2) ([h] +L ([h1] +R1 (D1 h1)) ([h2] +R2 (D2 h2)) h)
<- identity P1 (D1: hyp P1 -> true P1)
<- identity P2 (D2: hyp P2 -> true P2).
- : identity (P -o N) ([h] -oR ([h1] -oL (D1 h1) ([h2] D2 h2) h))
<- identity P (D1: hyp P -> true P)
<- identity N (D2: hyp N -> true N).
- : identity (circ P) ([h] circR (circL ([h'] laxR (D1 h')) h))
<- identity P (D1: hyp P -> true P).

%worlds (bl_atmpos | bl_atmneg | bl_hyp) (identity _ _).
%total T (identity T _).```

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  and , then  (cut)
• If  and , then  (lcut)

The proofs are by mutual lexographic induction; either the principal cut formula  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.

```cut : {A} true A -> (hyp A -> conc J) -> conc J -> type.
lcut : {A} lax A -> (hyp A -> lax C) -> lax C -> type.
%mode cut +A +D +E -F.
%mode lcut +A +D +E -F.```

#### Principal cuts

```- : cut (atom Q) (init+ H) ([h] init+ h) (init+ H).
- : cut (atom Q) (init- H) ([h] init- h) (init- H).

- : cut (up P) (upR (D: true P)) ([h] upL (E h : hyp P -> conc J) h) G
<- ({h': hyp P} cut (up P) (upR D) ([h] E h h') (F h'))
<- cut P D ([h'] F h') (G: conc J).

- : cut (down N) (downR (D: true N)) ([h] downL (E h : hyp N -> conc J) h) G
<- ({h': hyp N} cut (down N) (downR D) ([h] E h h') (F h'))
<- cut N D ([h'] F h') (G: conc J).

- : cut (P1 * P2) (*R (D1: true P1) (D2: true P2))
([h] *L (E h : hyp P1 -> hyp P2 -> conc J) 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) (G: conc J).

- : cut (N1 & N2) (&R (D1: true N1) (D2: true N2))
([h] &L1 (E h : hyp N1 -> conc J) h) G
<- ({h1: hyp N1} cut (N1 & N2) (&R D1 D2) ([h] E h h1) (F h1))
<- cut N1 D1 ([h1] F h1) (G: conc J).

- : cut (N1 & N2) (&R (D1: true N1) (D2: true N2))
([h] &L2 (E h : hyp N2 -> conc J) h) G
<- ({h2: hyp N2} cut (N1 & N2) (&R D1 D2) ([h] E h h2) (F h2))
<- cut N2 D2 ([h2] F h2) (G: conc J).

- : cut (P1 + P2) (+R1 (D1: true P1)) ([h] +L (E1 h : hyp P1 -> conc J) _ h) G
<- ({h1: hyp P1} cut (P1 + P2) (+R1 D1) ([h] E1 h h1) (F h1))
<- cut P1 D1 ([h1] F h1) G.

- : cut (P1 + P2) (+R2 (D2: true P2)) ([h] +L _ (E2 h : hyp P2 -> conc J) h) G
<- ({h2: hyp P2} cut (P1 + P2) (+R2 D2) ([h] E2 h h2) (F h2))
<- cut P2 D2 ([h2] F h2) G.

- : cut (P -o N) (-oR (D: hyp P -> true N))
([h] -oL (E1 h: true P) (E2 h: hyp N -> conc J) h) G
<- cut (P -o N) (-oR D) ([h] E1 h) (F1: true P)
<- ({h': hyp N} cut (P -o N) (-oR D) ([h] E2 h h') (F2 h' : conc J))
<- cut P F1 ([h'] D h') (G1: true N)
<- cut N G1 ([h'] F2 h') (G: conc J).

- : cut (circ P) (circR (D: lax P)) ([h] circL (E h : hyp P -> lax C) h) G
<- ({h': hyp P} cut (circ P) (circR D) ([h] E h h') (F h': lax C))
<- lcut P D ([h'] F h') G.```

#### Left commutative cuts

```- : lcut P (laxR (D: true P)) E F
<- cut P D E F.
- : cut A (upL D H) E (upL F H)
<- {h1} cut A (D h1) E (F h1).
- : cut A (downL D H) E (downL F H)
<- {h1} cut A (D h1) E (F h1).
- : cut A (0L H) E (0L H).
- : cut A (*L D H) E (*L F H)
<- {h1}{h2} cut A (D h1 h2) E (F h1 h2).
- : cut A (&L1 D H) E (&L1 F H)
<- {h1} cut A (D h1) E (F h1).
- : cut A (&L2 D H) E (&L2 F H)
<- {h2} cut A (D h2) E (F h2).
- : 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)).
- : cut A (-oL D1 D2 H) E (-oL D1 F2 H)
<- {h'} cut A (D2 h') E (F2 h').```

```- : lcut A (circL ([h] D h) H) E (circL ([h] F h) H)
<- {h'} lcut A (D h') E (F h').
- : lcut A (upL D H) E (upL F H)
<- {h1} lcut A (D h1) E (F h1).
- : lcut A (downL D H) E (downL F H)
<- {h1} lcut A (D h1) E (F h1).
- : lcut A (0L H) E (0L H).
- : lcut A (*L D H) E (*L F H)
<- {h1}{h2} lcut A (D h1 h2) E (F h1 h2).
- : lcut A (&L1 D H) E (&L1 F H)
<- {h1} lcut A (D h1) E (F h1).
- : lcut A (&L2 D H) E (&L2 F H)
<- {h2} lcut A (D h2) E (F h2).
- : 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)).
- : lcut A (-oL D1 D2 H) E (-oL D1 F2 H)
<- {h'} lcut A (D2 h') E (F2 h').```

#### Right commutative cuts

```- : cut A D ([h] init+ H) (init+ H).
- : cut A D ([h] init- H) (init- H).
- : cut A D ([h] laxR (E h)) (laxR F)
<- cut A D ([h] E h) F.
- : cut A D ([h] upR (E h)) (upR F)
<- cut A D ([h] E h) F.
- : cut A D ([h] upL ([h'] E h h') H) (upL F H)
<- {h'} cut A D ([h] E h h') (F h').
- : cut A D ([h] downR (E h)) (downR F)
<- cut A D ([h] E h) F.
- : cut A D ([h] downL ([h'] E h h') H) (downL F H)
<- {h'} cut A D ([h] E h h') (F h').
- : cut A D ([h] topR) topR.
- : cut A D ([h] 1R) 1R.
- : cut A D ([h] 0L H) (0L H).
- : 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.
- : 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).
- : 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.
- : 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).
- : 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).
- : cut A D ([h] +R1 (E1 h)) (+R1 F1)
<- cut A D ([h] E1 h) F1.
- : cut A D ([h] +R2 (E2 h)) (+R2 F2)
<- cut A D ([h] E2 h) F2.
- : 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)).
- : cut A D ([h] -oR [h'] E h h') (-oR [h'] F h')
<- {h'} cut A D ([h] E h h') (F h').
- : 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').
- : cut A D ([h] circR (E h)) (circR F)
<- cut A D ([h] E h) F.
- : 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').```

```- : lcut A D ([h] upL ([h'] E h h') H) (upL F H)
<- {h'} lcut A D ([h] E h h') (F h').
- : lcut A D ([h] downL ([h'] E h h') H) (downL F H)
<- {h'} lcut A D ([h] E h h') (F h').
- : 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).
- : 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).
- : 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).
- : 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.

```invupR : true (up P) -> true P -> type.
- : invupR D F
<- identity P (EP : hyp P -> true P)
<- cut (up P) D (upL ([h] EP h)) F.
%mode invupR +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invupR _ _).
%total [] (invupR _ _).

invupL : (hyp (up P) -> conc J) -> (hyp P -> conc J) -> type.
- : invupL ([h] D h) ([h] F h)
<- identity P (EP : hyp P -> true P)
<- {h: hyp P} cut (up P) (upR (EP h)) D (F h).
%mode invupL +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invupL _ _).
%total [] (invupL _ _).

invdownR : true (down P) -> true P -> type.
- : invdownR D F
<- identity P (EP : hyp P -> true P)
<- cut (down P) D (downL ([h] EP h)) F.
%mode invdownR +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invdownR _ _).
%total [] (invdownR _ _).

invdownL : (hyp (down P) -> conc J) -> (hyp P -> conc J) -> type.
- : invdownL ([h] D h) ([h] F h)
<- identity P (EP : hyp P -> true P)
<- {h: hyp P} cut (down P) (downR (EP h)) D (F h).
%mode invdownL +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invdownL _ _).
%total [] (invdownL _ _).

inv*R : true (P1 * P2) -> true P1 -> true P2 -> type.
- : inv*R D F1 F2
<- identity (P1 * P2) (E : hyp (P1 * P2) -> true (P1 * P2))
<- identity P1 (E1 : hyp P1 -> true P1)
<- identity P2 (E2 : hyp P2 -> true P2)
<- cut (P1 * P2) D (*L [h1][h2] E1 h1) F1
<- cut (P1 * P2) D (*L [h1][h2] E2 h2) F2.
%mode inv*R +D -F1 -F2.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (inv*R _ _ _).
%total [] (inv*R _ _ _).

inv&R : true (N1 & N2) -> true N1 -> true N2 -> type.
- : inv&R D F1 F2
<- identity (N1 & N2) (E : hyp (N1 & N2) -> true (N1 & N2))
<- identity N1 (E1 : hyp N1 -> true N1)
<- identity N2 (E2 : hyp N2 -> true N2)
<- cut (N1 & N2) D (&L1 [h1] E1 h1) F1
<- cut (N1 & N2) D (&L2 [h2] E2 h2) F2.
%mode inv&R +D -F1 -F2.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (inv&R _ _ _).
%total [] (inv&R _ _ _).

inv-oR : true (P -o N) -> (hyp P -> true N) -> type.
- : inv-oR D ([h] F h)
<- identity P (EP : hyp P -> true P)
<- identity N (EN : hyp N -> true N)
<- {h': hyp P} cut (P -o N) D (-oL (EP h') ([h] EN h)) (F h').
%mode inv-oR +D -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (inv-oR _ _).
%total [] (inv-oR _ _).

invcircR : true (circ P) -> lax P -> type.
- : invcircR D F
<- identity P (E: hyp P -> true P)
<- lcut (circ P) (laxR D) (circL ([h'] laxR (E h'))) F.
%mode invcircR +A -B.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (invcircR _ _).
%total [] (invcircR _ _).

invcircL : (hyp (circ P) -> lax C) -> (hyp P -> lax C) -> type.
- : invcircL D F
<- identity P (E: hyp P -> true P)
<- {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  and  and , then .

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 Twelf 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 Twelf 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; Twelf 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.

```trans-equiv-str : (hyp A -> conc J) -> trans _ tt' pos A -> conc J -> type.

- : trans-equiv-str D (t-+ (t+- TR)) E
<- invdownL D D'
<- invupL D' D''
<- trans-equiv-str D'' TR E.
- : trans-equiv-str D (t-+ t-true) E
<- cut (down top) (downR topR) D E.
- : trans-equiv-str D t+true E
<- cut 1 1R D E.

%mode trans-equiv-str +D +TR -F.
%worlds (bl_atmpos | bl_atmneg | bl_hyp) (trans-equiv-str _ _ _).
%total TR (trans-equiv-str _ TR _).

trans-equiv : trans _ M _ A1 -> true A1 -> trans _ M _ A2 -> true A2 -> type.
trans-equivX: trans _ M _ A1 -> true A1 -> trans _ M _ A2 -> true A2 -> type.
%mode trans-equiv +T1 +D1 +T2 -D2.
%mode trans-equivX +T1 +D1 +T2 -D2.

- : trans-equiv (t+- T1) D1 T2 D2
<- invupR D1 D1'
<- trans-equiv T1 D1' T2 D2.
- : trans-equiv (t-+ T1) D1 T2 D2
<- invdownR D1 D1'
<- trans-equiv T1 D1' T2 D2.
- : trans-equiv T1 D1 (t+- T2) (upR D2)
<- trans-equiv T1 D1 T2 D2.
- : trans-equiv T1 D1 (t-+ T2) (downR D2)
<- trans-equiv T1 D1 T2 D2.

- : trans-equiv tatom D tatom D.
- : trans-equiv t+true D t+true D.
- : trans-equiv t+true D t-true topR.
- : trans-equiv t-true D t+true 1R.
- : trans-equiv t-true D t-true D.
- : trans-equiv t+false D _ E
<- cut 0 D ([h] 0L h) E.
- : trans-equiv (t+not T) D t+false E
<- inv-oR D (Da : hyp P1 -> true (up 0))
<- ({h} invupR (Da h) (Db h))
<- trans-equiv-str Db T E.
- : 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.
- : 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.
- : 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.
- : 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.
- : trans-equiv (t+or Ta Tb) D (t+or Sa Sb) E
<- identity P1 (D1 : hyp P1 -> true P1)
<- ({h1} trans-equiv Ta (D1 h1) Sa (E1 h1))
<- identity P2 (D2 : hyp P2 -> true P2)
<- ({h2} trans-equiv Tb (D2 h2) Sb (E2 h2))
<- cut (P1 + P2) D (+L ([h1] +R1 (E1 h1)) ([h2] +R2 (E2 h2))) E.
- : trans-equiv (t-imp Ta Tb) D (t-imp Sa Sb) (-oR E)
<- identity P2 (D1 : hyp P2 -> true P2)
<- ({h1} trans-equivX Sa (D1 h1) Ta (E1 h1))
<- inv-oR D (D2 : hyp P1 -> true N1)
<- ({h1} trans-equiv Tb (D2 h1) Sb (E2 h1))
<- ({h2} cut P1 (E1 h2) ([h1] E2 h1) (E h2: true N2)).
- : trans-equiv (t+not T) D (t+not S) (-oR E)
<- identity P2 (D1: hyp P2 -> true P2)
<- ({h1} trans-equivX S (D1 h1) T (E1 h1))
<- inv-oR D (D2 : hyp P1 -> true (up 0))
<- ({h2} cut P1 (E1 h2) ([h1] D2 h1) (E h2: true (up 0))).
- : trans-equiv (t+circ T) (D: true (circ P)) (t+circ S) (circR F)
<- invcircR D (D1 : lax P)
<- identity P (D2 : hyp P -> true P)
<- ({h1} trans-equiv T (D2 h1) S (E h1: true B))
<- lcut P D1 ([h] laxR (E h)) F.

%% Cut and paste:

- : trans-equivX (t+- T1) D1 T2 D2
<- invupR D1 D1'
<- trans-equivX T1 D1' T2 D2.
- : trans-equivX (t-+ T1) D1 T2 D2
<- invdownR D1 D1'
<- trans-equivX T1 D1' T2 D2.
- : trans-equivX T1 D1 (t+- T2) (upR D2)
<- trans-equivX T1 D1 T2 D2.
- : trans-equivX T1 D1 (t-+ T2) (downR D2)
<- trans-equivX T1 D1 T2 D2.

- : trans-equivX tatom D tatom D.
- : trans-equivX t+true D t+true D.
- : trans-equivX t+true D t-true topR.
- : trans-equivX t-true D t+true 1R.
- : trans-equivX t-true D t-true D.
- : trans-equivX t+false D _ E
<- cut 0 D ([h] 0L h) E.
- : trans-equivX (t+not T) D t+false E
<- inv-oR D (Da : hyp P1 -> true (up 0))
<- ({h} invupR (Da h) (Db h))
<- trans-equiv-str Db T E.
- : 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.
- : 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.
- : 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.
- : 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.
- : trans-equivX (t+or Ta Tb) D (t+or Sa Sb) E
<- identity P1 (D1 : hyp P1 -> true P1)
<- ({h1} trans-equivX Ta (D1 h1) Sa (E1 h1))
<- identity P2 (D2 : hyp P2 -> true P2)
<- ({h2} trans-equivX Tb (D2 h2) Sb (E2 h2))
<- cut (P1 + P2) D (+L ([h1] +R1 (E1 h1)) ([h2] +R2 (E2 h2))) E.
- : trans-equivX (t-imp Ta Tb) D (t-imp Sa Sb) (-oR E)
<- identity P2 (D1 : hyp P2 -> true P2)
<- ({h1} trans-equiv Sa (D1 h1) Ta (E1 h1))
<- inv-oR D (D2 : hyp P1 -> true N1)
<- ({h1} trans-equivX Tb (D2 h1) Sb (E2 h1))
<- ({h2} cut P1 (E1 h2) ([h1] E2 h1) (E h2: true N2)).
- : trans-equivX (t+not T) D (t+not S) (-oR E)
<- identity P2 (D1: hyp P2 -> true P2)
<- ({h1} trans-equiv S (D1 h1) T (E1 h1))
<- inv-oR D (D2 : hyp P1 -> true (up 0))
<- ({h2} cut P1 (E1 h2) ([h1] D2 h1) (E h2: true (up 0))).
- : trans-equivX (t+circ T) (D: true (circ P)) (t+circ S) (circR F)
<- invcircR D (D1 : lax P)
<- identity P (D2 : hyp P -> true P)
<- ({h1} trans-equivX T (D2 h1) S (E h1: true B))
<- 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  and  and , then  (trans-sound)

Proved by induction on the target logic derivation .

```trans-sound : conc C -> trans-conc Mt C' C -> conc' Mc C' -> type.
%mode trans-sound +C +T -C'.```

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 Twelf'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  in the target logic using the rule upR, which gives us a subderivation , and we are translating into a contradiction  in the target logic (let  be the translated ).

By the induction hypothesis we have , which we have defined to be . We need to prove, however, . 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.



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.

```trans-init : trans Mt A' S (atom Q) -> hyp' A' -> hyp' (atom' Q) -> type.
- : trans-init tatom H H.
%mode trans-init +T +H -H'.
%worlds (bl_atmpos | bl_atmneg | bl_trans-soundhyp)  (trans-init _ _ _).
%total [] (trans-init _ _ _).

- : trans-sound (init+ H) (tc tatom) (id' H'')
<- trans-soundhyp H T H'
<- trans-init T H' H''.
- : trans-sound (init- H) (tc tatom) (id' H'')
<- trans-soundhyp H T H'
<- trans-init T H' H''.
- : trans-sound (laxR D) (tclax T) (circR' E)
<- trans-sound D (tc T) E.
- : trans-sound (upR D) (tc (t+- T)) E
<- trans-sound D (tc T) E.
- : trans-sound (upR D) tc# (cut' E ([h] notL' trueR' h))
<- trans-sound D (tc t+false) E.
- : trans-sound (upL D H) T (E H')
<- trans-soundhyp H (t+- Th) H'
<- ({h}{h'} trans-soundhyp h Th h'
-> trans-sound (D h) T (E h' : conc' M C)).
- : trans-sound (downR D) (tc (t-+ T)) E
<- trans-sound D (tc T) E.
- : trans-sound (downL D H) T (E H')
<- trans-soundhyp H (t-+ Th) H'
<- ({h}{h'} trans-soundhyp h Th h'
-> trans-sound (D h) T (E h' : conc' M C)).
- : trans-sound topR (tc t-true) trueR'.
- : trans-sound 1R (tc t+true) trueR'.
- : trans-sound (0L H) _ (notL' trueR' H')
<- trans-soundhyp H t+false H'.
- : trans-sound (0L H) _ (weakR' (notL' trueR' H'))
<- trans-soundhyp H t+false H'.
- : 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.
- : trans-sound (*L D H) T (/\L' ([h1][h2] E h1 h2) H')
<- trans-soundhyp H (t+and Th1 Th2) H'
<- ({h1}{h1'} trans-soundhyp h1 Th1 h1'
-> {h2}{h2'} trans-soundhyp h2 Th2 h2'
-> trans-sound (D h1 h2) T (E h1' h2')).
- : 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.
- : trans-sound (&L1 D H) T (/\L' ([h1][h2] E h1) H')
<- trans-soundhyp H (t-and Th _) H'
<- ({h}{h'} trans-soundhyp h Th h'
-> trans-sound (D h) T (E h')).
- : trans-sound (&L2 D H) T (/\L' ([h1][h2] E h2) H')
<- trans-soundhyp H (t-and _ Th) H'
<- ({h}{h'} trans-soundhyp h Th h'
-> trans-sound (D h) T (E h')).
- : trans-sound (+R1 D) (tc (t+or T _)) (\/R1' E)
<- trans-sound D (tc T) E.
- : trans-sound (+R2 D) (tc (t+or _ T)) (\/R2' E)
<- trans-sound D (tc T) E.
- : trans-sound (+L D1 D2 H) T (\/L' E1 E2 H')
<- trans-soundhyp H (t+or Th1 Th2) H'
<- ({h1}{h1'} trans-soundhyp h1 Th1 h1'
-> trans-sound (D1 h1) T (E1 h1'))
<- ({h2}{h2'} trans-soundhyp h2 Th2 h2'
-> trans-sound (D2 h2) T (E2 h2')).
- : trans-sound (-oR D) (tc (t-imp T1 T2)) (=>R' E)
<- ({h}{h'} trans-soundhyp h T1 h'
-> trans-sound (D h) (tc T2) (E h')).
- : trans-sound (-oR D) (tc (t+not T)) (notR' E)
<- ({h: hyp A}{h': hyp' A'} trans-soundhyp h T h'
-> trans-sound (D h) tc# (E h')).

trans-imp : {D: conc C}
idconc D (-oL (D1: true A1) (D2: hyp A2 -> conc C) H)
-> trans-conc Mt C' C
-> trans Mh A' neg (A1 -o A2)
-> hyp' A'
-> conc' Md C'
-> type.
%mode trans-imp +D +Id +T +Th +H -F.
- : 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'} trans-soundhyp h Th2 h'
-> trans-sound (D2 h) T (E2 h')).
- : trans-imp (-oL D1 D2 H) idconc/refl T (t+not Th) (H': hyp' (not' A'))
(weakR' (notL' E1 H'))
<- trans-sound D1 (tc Th) (E1: true' Md A').
- : trans-imp (-oL D1 D2 H) idconc/refl tc# (t+not Th) (H': hyp' (not' A'))
(notL' E1 H')
<- trans-sound D1 (tc Th) (E1: true' Md A').

- : 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.
- : trans-sound (circR D) (tc (t+circ T)) E
<- trans-sound D (tclax T) E.
- : trans-sound (circL D H) (tclax T) (circL' E H')
<- trans-soundhyp H (t+circ Th) H'
<- ({h}{h'} 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  and  and , then .

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.

```trans-compl : {Td}{Tt}
conc' Td D -> trans-conc Tt D J -> conc J -> type.
%mode trans-compl +Td +Tt +D +T -E.

%abbrev trans-compl'
= [d: conc' Td D][t: trans-conc Tt D J][e: conc J]
trans-compl Td Tt d t e.```

#### Shifts

```- : trans-compl' D (tc (t+- T)) (upR E)
<- trans-compl' D (tc T) E.

- : trans-compl' D (tc (t-+ T)) (downR E)
<- trans-compl' D (tc T) E.```

#### Truth

```- : trans-compl' trueR' (tc t+true) 1R.
- : trans-compl' trueR' (tc t-true) topR.```

#### Conjunction

```- : 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.

- : 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.

trans-andL : {TD}{Th} id TD (x Td)
-> (hyp' M1 -> hyp' M2 -> conc' Td D)
-> trans-conc Tt D J
-> trans Th (M1 /\ M2) S A
-> (hyp A -> conc J) -> type.
%mode trans-andL +TD +Th +Id +D +T +Th -E.
- : trans-andL _ _ id/refl (D : hyp' M1 -> hyp' M2 -> conc' Td D')
(T: trans-conc Tt D' J) (t-and T1 T2)
([h] (&L1 ([h1] &L2 ([h2] E h1 h2) h) h))
<- ({h1'}{h1} trans-complhyp h1' T1 h1
-> {h2'}{h2} trans-complhyp h2' T2 h2
-> trans-compl' (D h1' h2') T (E h1 h2)).
- : trans-andL _ _ id/refl (D: hyp' M1 -> hyp' M2 -> conc' Td D')
(T: trans-conc Tt D' J) (t+and T1 T2)
([h] (*L ([h1][h2] E h1 h2) h))
<- ({h1'}{h1} trans-complhyp h1' T1 h1
-> {h2'}{h2} trans-complhyp h2' T2 h2
-> trans-compl' (D h1' h2') T (E h1 h2)).
- : trans-andL _ _ Id D T (t+- Th) (upL E)
<- trans-andL _ _ Id D T Th E.
- : trans-andL _ _ Id D T (t-+ Th) (downL E)
<- trans-andL _ _ Id D T Th E.

- : trans-compl' (/\L' D H') T (E H)
<- trans-complhyp H' Th (H: hyp A)
<- trans-andL _ _ id/refl D T Th (E: hyp A -> conc D').```

#### Disjunction

```- : trans-compl' (\/R1' (D: true' Tt M1)) (tc (t+or T1 _)) (+R1 E)
<- trans-compl' D (tc T1) E.
- : trans-compl' (\/R2' (D: true' Tt M2)) (tc (t+or _ T2)) (+R2 E)
<- trans-compl' D (tc T2) E.

trans-orL : {TD}{Th} id (TD) (Td1 | Td2)
-> (hyp' M1 -> conc' Td1 D')
-> (hyp' M2 -> conc' Td2 D')
-> trans-conc Tt D' J
-> trans Th (M1 \/ M2) S A
-> (hyp A -> conc J) -> type.
%mode trans-orL +TD +Th +Id +D1 +D2 +T +Th -E.
- : trans-orL _ _ id/refl D1 D2 T (t+or Th1 Th2) (+L ([h1] E1 h1) ([h2] E2 h2))
<- ({h1': hyp' M1}{h1: hyp P1} trans-complhyp h1' Th1 h1
-> trans-compl' (D1 h1') T (E1 h1: conc J))
<- ({h2': hyp' M2}{h2: hyp P2} trans-complhyp h2' Th2 h2
-> trans-compl' (D2 h2') T (E2 h2: conc J)).
- : trans-orL _ _ id/refl D1 D2 T (t+- Th) (upL E)
<- trans-orL _ _ id/refl D1 D2 T Th E.
- : trans-orL _ _ id/refl D1 D2 T (t-+ Th) (downL E)
<- trans-orL _ _ id/refl D1 D2 T Th E.

- : trans-compl' (\/L' D1 D2 H') T (E H)
<- trans-complhyp H' Th H
<- trans-orL _ _ id/refl D1 D2 T Th E.```

#### Implication

```- : trans-compl' (=>R' (D: hyp' M1 -> true' Tt M2)) (tc (t-imp T1 T2)) (-oR E)
<- ({h'}{h} trans-complhyp h' T1 h
-> trans-compl' (D h') (tc T2) (E h)).

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

- : trans-compl' (=>L' D1 D2 (H': hyp' (M1 => M2))) T (E H)
<- trans-complhyp H' Th (H: hyp A)
<- trans-impL _ _ id/refl D1 D2 T Th E.```

#### Negation

```- : trans-compl' (notR' (D: hyp' tt' -> # _)) (tc t+false) G
<- ({h'}{h} trans-complhyp h' t+true h
-> trans-compl' (D h') tc# (E h))
<- cut 1 1R ([h] E h) F
<- invupR F G.

- : trans-compl' (notR' (D: hyp' M -> # _)) (tc (t+not T)) (-oR ([h] (E h)))
<- ({h'}{h} trans-complhyp h' T h
-> trans-compl' (D h') tc# (E h)).

trans-notL : {TD}{Tt} id TD (x Td)
-> true' Td M
-> trans Tt (not' M) S A
-> (hyp A -> true (up 0)) -> type.
%mode trans-notL +TD +Tt +Id +D +Th -E.
- : trans-notL _ _ id/refl (D: true' Td M) (t+not T) (-oL E (upL 0L))
<- trans-compl' D (tc T) (E: true P).
- : trans-notL _ _ id/refl D t+false 0L.
- : trans-notL _ _ Id D (t+- T) (upL E)
<- trans-notL _ _ Id D T E.
- : trans-notL _ _ Id D (t-+ T) (downL E)
<- trans-notL _ _ Id D T E.

- : trans-compl' (notL' (D: true' Td M) (H': hyp' (not' M))) tc# (E H)
<- trans-complhyp H' Th (H: hyp A)
<- trans-notL _ _ id/refl D Th E.```

#### Lax modality

```- : trans-compl' (circR' D) (tc (t+circ T)) (circR (laxR E))
<- trans-compl' D (tc T) E.
- : trans-compl' (circR' D) (tclax T) (laxR E)
<- trans-compl' D (tc T) E.

trans-circL : {TD}{Th} id TD (x Td)
-> (hyp' M -> true' Td (circ' D'))
-> trans Tt D' S C
-> trans Th (circ' M) Sh A
-> (hyp A -> lax C) -> type.
%mode trans-circL +TD +Tt +Id +D +T +Th -E.
- : 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) (E h : lax C)).
- : trans-circL _ _ Id D T (t+- Th) (upL F)
<- trans-circL _ _ Id D T Th F.
- : trans-circL _ _ Id D T (t-+ Th) (downL F)
<- trans-circL _ _ Id D T Th F.

- : trans-compl' (circL' (D: hyp' M -> true' Td (circ' D')) H')
(tc (t+circ (T: trans Tt D' pos J))) (circR (E H))
<- trans-complhyp H' Th (H: hyp A)
<- trans-circL _ _ id/refl D T Th E.

- : trans-compl' (circL' (D: hyp' M -> true' Td (circ' D')) H')
(tclax (T: trans Tt D' S J)) (E H)
<- trans-complhyp H' Th (H: hyp A)
<- 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.

```- : trans-compl' (cut' (Da: true' _ M) Dc) T F
<- can-trans M (TRa: trans _ M S A)
<- trans-compl' Da (tc TRa) (Ea: true A)
<- ({h'}{h} 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  and need to show , where .

Identity is a terminal rule, so we will not use induction here. We know because  is a hypothesis that there is a hypothesis  such that , and so by the identity principle we can prove ; then, trans-equiv allows us to prove , which is what we actually need.

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

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  but the best we can get is  or . However, we can use inversion lemmas (and lax cut, in the second case) to get what we need.

```- : trans-compl' (id' (H': hyp' (circ' M))) (tclax (T: trans _ M pos Pm)) F
<- trans-complhyp H' Th (H: hyp P)
<- identity P (D2: hyp P -> true P)
<- trans-equiv Th (D2 H) (t+circ T) (E: true (circ Pm))
<- invcircR E (F: lax Pm).
- : trans-compl' (id' (H': hyp' (circ' M))) (tclax (T: trans _ M neg Nm)) G
<- trans-complhyp H' Th (H: hyp N)
<- identity N (D2: hyp N -> true N)
<- trans-equiv Th (D2 H) (t+circ (t-+ T)) (E: true (circ (down Nm)))
<- invcircR E (F: lax (down Nm))
<- identity _ (Id: hyp Nm -> true Nm)
<- lcut _ F ([h] laxR (downL ([h'] Id h') h)) (G: lax Nm).

- : 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 _ _ _ _ _).```