\(\newcommand{\interp}[1]{[\negthinspace[#1]\negthinspace]}\)

This post was written while I was attending VSL from July 12 – July 17 2014.

This week I am in Vienna — the capital of Austria — attending the Vienna Summer of Logic (VSL). It has been a blast! The feeling I get when attending a conference is pure unadulterated motivation, creativity, and excitement. I just love this atmosphere. So many great researchers giving great talks about interesting work.

So what do I do with this excitement you might ask? I start to reflect on my own research quite deeply, and ponder if what I am doing is the best I can do, and if the answer is no, then I begin fixing it so that it is. Now, by “the best I can do” I do not mean “will get into the best conference/journal” or “will make me famous”, but rather only that it meets my personal standards, basically I want to be able to be proud that my work is my work and anything less is a waste. An example of this was when I attended a three week summer school in Eugene Organ called the Organ Programming Languages Summer School. There was the first time I got this feeling, and I ended up reworking how proofs of normalization using hereditary substitution worked from the ground up.

So what am I thinking about now that I have this feeling again? My research focused on understanding bi-intuitionistic simple type theory with a non-trivial categorical model. The work I have done so far — in collaboration with Aaron Stump and Ryan McCleeary — can be found here and was presented at The 5th International Workshop on Classical Logic and Computation (CL&C) 2014 on Sunday July 13.

Currently, Dualized Type Theory (DTT) has a sequent that looks like \(G;x_1 : p_1 A_1@n_1,\ldots,x_j : p_j A_j@n_j \vdash t : p B @ n \). There each \(x_i\) and \(t\) are terms while \(G\) is a graph — defined as a list of ordered pairs — and each \(n_i\) and \(n\) are nodes in \(G\), finally each \(p_i\) and \(p\) are polarities — either \(+\) or \(-\). So what is the deal with the graph and node labels on types?

Tristan Crolard was the first to study bi-intuitionistic logic and type theory in the context of computer science. He proposed a multi-succedent sequent calculus called Subtractive Logic, but this sequent calculus has a defect. It requires the Dragalin restriction. This restriction requires that the premise of the right implication inference rule have only one formula on the right side of the sequent. Just as linear logicians observed this breaks cut-elimination! Luis Pinto and Tarmo Uustalu proposed a means of fixing this issue by first starting with LK+subtraction, and then adding a labeling system using graphs that semantically correspond to constraints on the set of Kripke models. This system they called labeled BINT. DTT can be seen as a simple type theory of a simplified version of labeled BINT called Dualized Intuitionistic Logic (DILL).

At this point I should quickly explain — intuitively — what BINT is, but I am not going to go into to much detail. See the references I have been linking to. My slogan is “BINT is intuitionistic logic with perfect duality.” Now “perfect” may be to strong of a word, but it gets my point across. BINT is a logic where for every logical connective of the logic its dual is also a logical connective of the logic. That is, BINT consists of true and false, conjunction and disjunction, and implication and its dual called subtraction or exclusion. Cecylia Rauszer was the first person to study BINT where she proposed an extended version of the Kripke Semantics for intuitionistic logic.

Lets consider the extended Kripke Semantics proposed by Cecylia. It may help with understanding subtraction. The interpretation of implication into a Kripke Model is defined as follows:

\( \interp{A \to B}_w = \forall w’.wRw’ \Rightarrow \interp{A}_{w’} \Rightarrow \interp{B}_{w’}\)

This states that \(A \to B\) holds in an arbitrary Kripke Model at world \(w\) if for any future world \(w’\), reachable from \(w\), and assuming \(A\) holds in the model at the future world \(w’\), and we can show that \(B\) holds at world \(w’\). The key observation to make regarding this interpretation is that it is modal, and talks about all

**future**worlds. This modal aspect is what connects the semantics of modal logic S4 to Kripke semantics. Now to obtain the interpretation of subtraction in Kripke semantics is by simply taking the dual of the above definition:

\( \interp{A – B}_w = \exists w’.w’Rw \land \interp{A}_{w’} \land \lnot\interp{B}_{w’}\)

This shows that we move from talking about all future worlds to talking about the existence of a past world!

It is well-known that the simply-typed \(\lambda\)-calculus can be interpreted in cartesian-closed categories (CCC). Tristan Crolard showed that if one extends a CCC with co-products (which corresponds to disjunction) and co-exponentials or the left adjoint of the co-product (which corresponds to subtraction) then one obtains what he named a bi-[CCC], but even worse every bi-[CCC] is equivalent — up to isomorphism — to a preorder. That is, there is at most one morphism between any two objects of the bi-[CCC]. Therefore, this does not provide for a very good proof theory of BINT!

So I pose the question, does there actually exist a non-trivial proof theory for BINT? The answer may very well be no, but I have some ideas to explore before making that bold claim. That’s the topic of my next post. If the answer is indeed no, then that implies that we must move away from trying to come up with a satisfactory proof theory of bi-intuitionistic logic in the sense of a bi-[CCC]. Instead we must insist that bi-intuitionistic logic be split into two fragments: a positive fragment (or as Paul-Andrea Millies calls it the prover) and a negative fragment (denier). We can also consider the positive fragment being intuitionistic logic, and the negative fragment co-intuitionistic logic — actually this will be slightly different, because we cannot have an isomorphism between both sides. However, before going to that extreme there are a few ideas I want to explore first.

The first idea I explored was moving to linear logic and combining the idea of Crolard’s bi-[CCC]‘s with the idea of Nick Benton’s mixed linear non-linear models of linear logic. I thought that by doing this we could obtain a non-trivial categorical model of bi-intuitionistic linear logic (linear BINT), and by the use of Girard’s translation a categorical model of BINT. However, this does not fix the problem, the embedding of BINT into linear BINT is degenerate by the same argument as Crolard’s. Let’s consider a diagram that may help situate our minds on this idea:

The diagram shows that we can view the model of linear BINT as the union of a symmetric monoidal closed category and its opposite. Then using Girard’s embedding we can obtain an adjunction between a bi-[CCC] (full BINT) and the previous union.

To use Crolard’s argument all we have to show is that by way of Girard’s translation that the co-Kleisli category is cartesian closed and the Kleisli category is co-cartesian co-closed. The former follows from Seely’s theorem in Gavin Bierman’s thesis (Proposition 17 on p. 156), and the latter follows by duality. We briefly show how to obtain the fact that intuitionistic implication is modeled by the right adjoint to the product functor:

\(

\begin{array}{lll}

\mathcal{C}_!(A \times B, C) & \cong & \mathcal{C}_!(!(A \times B), C) & (\text{Def.})\\

& \cong & \mathcal{C}_!(!A \times !B, C) & (\text{Seely’s axiom}\,n)\\

& \cong & \mathcal{C}_!(!A, !B -\negthinspace\negthinspace *\, C) & (\text{Closure.})\\

& \cong & \mathcal{C}_!(A, !B -\negthinspace\negthinspace * \,C) & (\text{Def.})\\

\end{array}

\)

Note that the symbol \(-\negthinspace\negthinspace *\) is linear implication. I could not get the CMLL latex library to work with MathJax yet.

Now by duality we have the following result.

Therefore, any categorical model of linear BINT with linear exponentials is degenerate just as Crolard established.

We could either remove the \(!\)-exponential (of-course) or the \(?\)-exponential (why-not) to obtain a model that looks like one of these:

We could also take the union of a CCC and a SMcC which would mean that the majority of the logic is non-linear, but subtraction is left linear. Now this is less appealing, because it is not as elegant as the other linear logic formulations (previous two diagrams) and it is no more expressive than the previous two diagrams especially the first of the two.

All of the approaches I have been discussing so far have been trying to keep the model — and also the logic — to be as collapsed as possible. I mentioned above that we could also separate the postive fragment from the negative fragment, and then relate them using a weak equivalence — an adjunction. Paul-Andrea Millies calls this a chirality. The term comes from chemistry and means something to the effect of “mirror symmetry.”

This is all I want to say in this post. I now conclude with some final remarks. My reflecting I think has paid off, as it usually does, and I believe I now have a novel idea for two different, but related non-trivial categories models of DIL and DTT. These models will indeed be collapsed, but constrained by an external structure. I will leave the reader with a hint about my latest idea. DIL and DTT may have a categorical model where the external structure is a coalgebra. Exciting I know!