NCL goes to India?

Despite our initial doubts that we'd be able to say anything of much interest about NCL, Sara and I managed to actually solve its composition problem: we now know that

If φ and φ→ψ are NCL-valid, then so is ψ.

The proof didn't turn out to be hard, but it does involve some rather curious lemmas that hardly resemble anything like what I've seen before in my study of mathematical logic. It really feels like exploring a whole new world. Sara discovered a crucial feature of valid NCL-implications:

If φ→ψ is NCL-valid, then either

• φ is an atom,
• φ is a negation, or
• ψ is already NCL-valid.

I confess that I was skeptical when Sara shared this conjecture with me; it felt too ham-fisted and alien. But the conjecture in fact holds, and it paves the way toward a positive solution of the composition problem. (The other principal lemma in the proof is a characterization of NCL-valid negations.) Just today we submitted a joint paper about all this (“A curious dialogical logic and its composition problem”) to the upcoming Indian Conference on Logic and its Applications, to be held in Delhi in January, 2011. We expect to learn in about a month whether it will be accepted. (In the paper we call NCL simply “N”. The name NCL comes from a more benighted time when we thought, based on a priori reasoning about rulesets, that since NCL is only slightly different from a ruleset that characterizes classical logic, it would correspondingly give rise to a logic that might be different from classical logic but “close” to it.) We were restricted to 12 pages, but we have lots more to say about NCL and couldn't pack it all in. We expect to produce a fuller account in a journal article.

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.

Nearly classical logic

Here's something interesting: The rule set consisting in Felscher's D minus rules D11 and D12 -- which at one point we thought corresponded to classical logic, but then we found out does not because though LEM is valid, Peirce's formula is not, and so which we've since been calling "Nearly Classical Logic" even though we're not sure it's even a logic, much less that it's close to CL -- if it corresponds to a logic corresponds to one that is strangely sensitive to atomic formulas. The validities that it does have (LEM, WEM, Dummett's formula), remain valid under a number of negation-translations: double-negating the whole formula, DNing each subformula, Kuroda's translation, negation of atomic formulas, DN of atomics. However, the translations which replace $p$ with $p\vee p$ or $p\wedge p$ and Gödel-Gentzen both fail to preserve validity. The problem is that as soon as P makes a defendable attack (such as ?R or ?L or ?), O can stall indefinitely by continuously defending the attack. Despite this oddity, we have been unable to come up with a counterexample to the composition problem. Even simple cases such as LEM->LEM^GG fail to be valid, so it's unlikely that we'll find a more complicated counterexample in that realm. What this sensitivity to atomic formulas corresponds to is at this point still utterly opaque to me.

Meta

Having not yet had any time to write a proper blog post, I thought I would take a few minutes to at least write a post about posts I am going to write when said time magically appears. The first question Jesse and I considered, and the one that eventually led him to think of and formulate the composition problem, was one that I thought was relatively simple: Given a classically valid formula $\phi$ and the Gödel-Gentzen translation $\phi^n$ of $\phi$, is there a (uniform) way of translating the winning strategy for $\phi$ in the classical game into a winning strategy for $\phi^n$ in the intuitionistic game? What the composition problem has shown us is that this is not an easy question to answer partly because it is not clear what a "winning strategy in the classical game" is. So answering that question will be a long time off and in the meantime I'm going to be much more modest in my aims, and I've come up with a number of much, much more basic questions that I hope to answer, whose answering I also hope will help me come up with some intuitions about how dialogical proofs work (since currently I have none). These are the issues I hope to explore in future blog posts: - The "solution" to the "weakening" problem: We discussed this in Ponta Delgada and I think convinced ourselves that the weakening problem does indeed have a solution, but for now the scare quotes are necessary because we haven't anything like a proof. - Why DN is so important in differentiating classical logic from intuitionistic logic. - What would particle rules for TONK look like? - Is there anyway to get an inconsistent logic other than dropping the requirement that P cannot assert an atomic formula unless O has already asserted it? - How symmetric can you make the structural rules (so that they treat O and P the same) and still get a logic? Some tantalizing topics for future discussion...

Announcing dialogues version 0.9

Following up on my presentation yesterday at the MathUI 2010 workshop, where I discussed the Dialogical Foundations of Semantics project, Lorenzen dialogue games, and demonstrated the software that I've written, it seems appropriate to me to make a formal release of what I've got. Since the system is web-based, there's no need to download and install anything at all beyond a web browser. Just visit the dialogues site to play dialogue games. This announcement concerns the release of the software that underlies the site. If you don't particularly care to download source code and hack lisp, then this post isn't for you. But if you're interested in looking at what makes the site tick, or if you want to even contribute with its development, then read on. You can download the release from github. This system is tested only with SBCL. The main thing that might not work with other Common Lisps is the web server. Patches accepted. So far, the community of people using this system is extremely small, so bug reports and feature requests are greatly appreciated.

The composition problem for Lorenzen dialogue games

The problem: given a set S of dialogue rules, show that

If Proponent has a winning strategy for the S-dialogue game commencing with φ and a winning strategy for the S-dialogue game commencing with φ→ψ, then Proponent has a winning strategy for the S-dialogue game commencing with ψ.

The composition problem for a set of dialogue rules S asks whether the set of formulas φ for which Proponent has a winning strategy in the S-dialogue game commencing with φ is closed under modus ponens. From a rule of inference R one can introduce a further parameter into the definition of the composition problem:

Is the set of formulas φ for which Proponent has a winning strategy in the S-dialogue game commencing with φ closed under the rule R?

The original composition problem—which depends on a set S of dialogue rules—is evidently just the specialization of the more general two-parameter composition problem where we have plugged in modus ponens for the rule of inference parameter R. From this more general perspective, here are two further compositions problems:

• modus tollens:

  If Proponent has a winning strategy for the S-dialogue game commencing with φ→ψ; and a winning strategy for the S-dialogue game commencing with ¬ψ, then Proponent has a winning strategy for the S-dialogue game commencing with ¬φ.

• “implication weakening”:

  If Proponent has a winning strategy for the S-dialogue game commencing with ψ then Proponent has a winning strategy for the S-dialogue game commencing with φ→ψ.

These variants of the original composition problem may or may not be more tractable than it. Either kind of solution to the composition problem or its variants—positive or negative—would be valuable. Of course, positive and negative solutions (counterexamples) to the general composition problem abound: for any interesting rule of inference at hand, we can simply concoct ad hoc dialogue rules that ensure that a positive or a negative counterexamples. These counterexamples, though, lack interesting logical content. A challenge then is to formulate some minimally contentful dialogue rules that give the discussion at least some semblance of serious logical investigation. There may be many such minimally contentful sets. The composition problem is valuable because it is, for of all, so basic and gets at the very heart of the claim that (strategies for) dialogues (à la Lorenzen) really do give us another view on validity. The problem is tantalizing because we do know, for at least one or two sets of dialogue rules, that there is a positive solution to it. Felscher's so-called equivalence theorem, showing that Proponent has a winning strategy for the dialogue game commencing with φ iff φ is intuitionistically valid, amounts to a positive (though not entirely straightforward) solution in the case of Felscher's dialogue rules. Moreover, there are cases where we expect a positive solution (I have in mind here cases where we drop one or two of Felscher's rules, or add an “innocent” extension of them), but which—to my knowledge at least—are open.