Where in the world is NCL?

When you have no intuitions about a logic, trying to determine any of its properties or prove anything about it is like fumbling around in the dark. Working with NCL, I've developed a few intuitions, which Jesse is working on proving (one intuition is strong enough that I have bet him dinner and a bottle of Sangiovese that he won't find a counterexample), but while I can make some predictions about how the actors will act, I still have no sense of what is going on behind the curtain. All I know by now is that "NCL" is really a misnomer, since this isn't "nearly" anything, much less classical logic. Is it a logic? This depends on how "logic" is defined. Chagrov & Zakharyaschev, Modal Logic, p. 109 defines a superintuitionistic-logic (in language $\mathcal{L}$) as any set $L$ of $\mathcal{L}$-formulas such that: - $\mathbf{IL}\subseteq L$; - $L$ is closed under modus ponens; - $L$ is closed under uniform substitution. Now, this definition does not suit our purposes as it stands; first, NCL, if it is a logic, is not an si-logic, so we must drop the first condition. Second, as we noted in a previous post, NCL is not closed under uniform substitution, so we must drop the third condition (as there are sets of formulas out there which are not closed under uniform substitution, but only restrictions thereof, which are accepted as logics, we needn't worry too much about this). So we are left with this definition of a logic: \begin{dfn}A \emph{logic} (in language $\mathcal{L}$) is any set $L$ of $\mathcal{L}$-formulas such that $L$ is closed under modus ponens.\end{dfn} This definition of a logic also has the advantage that it highlights the importance of the composition problem. Solving the composition problem for a given set $L$ is a prerequisite for declaring $L$ a logic. Let us assume, for the time being, that we have solved the composition problem for NCL, and that it is a logic. The burning question is, what kind of logic is it? Where does it fit in the scheme of things? We've known from day 1, the day that the dialogical rules for NCL split off from those for CL and they were baptised NCL, that NCL is below CL; it validates, e.g., LEM and WEM but not Peirce. However, it is something of a surprise that NCL is not an extension of IL either, as NCL-validity is not preserved by the Gödel-Gentzen translation. This means that NCL is orthogonal to both IL and CL. The most familiar class of propositional logics that lie orthogonal to IL and CL are connexive logics, which briefly looked promising but quickly collapsed, as NCL does not validate any of the usual connexive theses ($\neg (p\rightarrow \neg p$, $\neg(\neg p\rightarrow p)$, $(p\rightarrow q)\rightarrow\neg(p\rightarrow\neg q)$, $(p\rightarrow q)\rightarrow\neg(\neg p\rightarrow q)$), and validates what we've called the "anti-connexive thesis" ($((p\rightarrow\neg p)\vee(\neg p\rightarrow p))$, which is just a substitution instance of Dummett's formula, an NCL-validity. (In passing, I note that I no longer have any idea why we called this formula the "anti-connexive thesis". Scarily, googling for that phrase returns precisely one hit, http://dialogical-logic.info/). So what is NCL like? - It is like paraconsistent logic in that (some forms of) ex falso are not valid; in particular, conjunctive ex falso fails. (Implicational and negated disjunctive ex falso are valid, however, even at the atomic level.) - It is like relevance logic in that uniform substitution is restricted (cf.\ Rückert 2007, pp.\ 28, 79), though it is restricted in a very different way. - It is like linear logic in that it is "resource sensitive" -- duplicating atoms is not validity preserving. It also appears to be "information sensitive", in that it doesn't appear possible to string validities together to get new ones (more about this later, maybe). - It is like substructural logics more generally, in that the order and the number of the premises matters. What we'd love to find is some $L$-validities where $L$ is not an si-logic which are not CL-validities that we could test in NCL. So far, every NCL-validity we've found is a CL-validity.