Summary of the trip

Tomorrow I leave Vienna and head back to Amsterdam, and thus I thought it would be useful to put a brief recap of the important results of the last month:

• Jesse and I finished up our extended paper on N, "A Curious Dialogical Logic and Its Composition Problem", and sent it off.
• Significant new features have been added to the dialogues website, including the long-awaited ability to compute strategies interactively and the possibility of selecting arbitrary rulesets (from a pre-defined set of rules).
• Our goal with Chris was to find out general conditions under which it can be proved that E is redundant; we have not gotten as far as we like, but the results of my various pokings and proddings on the subject are contained in "Some Remarks on the E rule in Dialogical Logic".

This research visit was funded by a grant from the European Science Foundation EUROCORES Short-Term Visit scheme within the framework of the ESF EUROCORES Programme entitled 'Modelling Intelligent Interaction', which we gratefully acknowledge.

Inside Arguments, Coimbra, Portugal

On Saturday, March 26, Jesse and I presented our paper "Lorenzen dialogues as logical semantics" at the International Colloquium Inside Arguments; our slides are available here. In this paper, we argue against an argumentation-theoretic understanding of dialogue games. While it may be the case that Lorenzen's original motivation for dialogical semantics came from a desire to connect intuitionistic theoremhood with real principles of dialogue, interaction, and debate, it is unclear to what extent this philosophical foundations can be carried through to the extensions of the approach to classical logic, modal logic, etc. We give three arguments against any strong connection between actual argumentative practice and dialogical semantics:

• The lack of disagreement on the proper set of structural rules for intuitionistic logic (cf. the wildly different approaches of, e.g., Felscher and Rahman).
• The problem, illustrated by N, of the interplays that arise in sets of independently plausible structural rules.
• Difficulties in identifying acceptable criteria which allow us to rule out particle rules for connectives like tonk, but which do not force us to rule out, e.g., the particle rules for negation.

Unfortunately we had to leave almost immediately after our talk in order to get the train back to Lisbon, so there was not much time for discussion, but judging from the reactions of the audience during the presentation, the reaction was favorable.

Announcement: Two new papers

Last night we submitted two papers produced during the four-week research project on Dialogical Logic in the University of Amsterdam's Master of Logic programme:

• "Dialogue Games for Classical Logic". In this paper we introduce a class of dialogue games for classical logic, building on both Felscher 1985 and Fermüller 2003, and give a rigorous proof of the correspondence between the two.
• A Tableau System for the Dialogical Logic N". In this paper we define a tableau system for the logic N, and prove that it is sound and complete with respect to the logic. The proofs go via a reduction to canonical tableaux and algorithms for converting closed tableaux into winning strategies and vice versa.

Both papers are joint work by Jesse Alama, Aleks Knoks, and Sara L. Uckelman.

Characterizing N-validities

One of the key theorems of our first paper on N was the theorem characterizing valid implications:

Theorem 3: Every N-valid implication φ->ψ satisfies one of the following three conditions:

1. φ is atomic.
2. φ is negated.
3. ψ is N-valid.

Last week I spent some time trying to come up with similar characterizations of validities of other types, that is, characterizations of N-valid atoms, negations, disjunctions, and conjunctions. Three of the four are easy:

• No atom is N-valid [Lemma 2].
• The only N-valid negations are double negations of validities [Theorem 4].
• A conjunct is N-valid iff each conjunct is N-valid [obvious].

So, can we characterize disjunctions? Suppose φVψ is N-valid. There are three cases:

1. Either φ is N-valid or ψ is N-valid.
2. Neither disjunct is N-valid, and neither contains any implication.
3. Neither disjunct is N-valid, but at least one contains an implication.

In the first case, nothing more is needed. For the other two, I have a

Conjecture: (2) At least one atom occurs at least twice in the formula, once with an odd number of negations and once with an even number of negations. NOTE: I do not mean occurs "within the scope of an odd/even number of negations" (as you would find in classical logic) but that attached to the atom itself are an odd or even number (0, of course, being an even number). (3) At least one atom occurs both in the antecedent of a conditional and in either the consequent of a conditional or as a stand alone atomic subformula. (If we wanted a more felicitous phrasing, we could say that an atom is the consequent of a trivial conditional, and then say: "at least one atom occurs in both the antecedent and the consequent of a conditional". But Jesse found this problematic.)

Now we have the following open problem: Prove the conjecture, or find a counterexample.

Live, from Indonesia

Tuesday afternoon, Jesse and I released N into the wild. He gave a talk introducing the website (look for significant improvements to it soon!) and then I spoke about N and the challenges of developing a proof theory for it. I think we rather perplexed the audience, as there was only one person in it that had ever heard of dialogical logic before, and we only had 20 minutes between the two of us. A substantive blog post will come soon; I've got a couple of topics that have been rattling around in my mind.

N goes to India

Jesse and I will be traveling to the 4th Indian Conference on Logic and its Applications to present our paper "A curious dialogical logic and its composition problem".

Handling assumptions

I still have a half-written blog post from when I was in Lisbon last week, but I think it will have to wait, as now I'm thinking about something else, namely, how to handle assumptions in dialogical logic. While preparing a short note on the sound proof rules of N, I noticed that none of them have anything on the left-hand side of the turnstile; that is, none of the rules model anything like reasoning from assumptions. At this point, I have no idea if this is something specific to N, because we don't know enough about N, and how much of this is specific to the dialogical approach, which doesn't, on the face of it, allow for any type of reasoning from assumptions. Now what about IL and CL? They have dialogical characterizations and allow reasoning from assumptions, both in their ordinary semantics and in their proof theory. So why is it that they can be dialogically characterized, if ordinary structural/particle rules don't allow for assumptions? My suspicion is that it's because both logics satisfy a deduction theorem -- $\Gamma\vdash\phi$ iff $\vdash\Gamma\rightarrow\phi$, and hence you can "do away" with assumptions. Now, the fact that the proof rule from $\vdash\phi\rightarrow\psi$ infer $\vdash(\gamma\rightarrow\phi)\rightarrow(\gamma\rightarrow\psi)$ is not sound in N shows that N cannot have an ordinary deduction theorem, and so it is important to find a way to handle reasoning from assumptions in N in a dialogical way. Here is a naive approach, which I will ask Jesse to implement so I can test it via the website: - Fix a set of formulas $\Gamma$ such that Proponent can assert $\phi\in\Gamma$ at any time, as either an attack or as a defense. Essentially then $\Gamma\vDash\psi$ says "if you (Opponent) grant me (Proponent) the info in $\Gamma$, I can prove $\psi$ to you. Being that this is a naive approach, I do not know how well it will work. Luckily, since we know how reasoning from assumptions should work in IL and CL, we can use them as test cases for this approach.

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.