A simpler case

Some amount of thought on the previous post made it clear to me that my example was way more complicated than it needs to be. The following formula should be IL valid and allows Opp to assert a conditional so that Pro can attack it:

(implies (implies (and p p) q) (implies (and p p) q))

Or, in readable fashion:

(((P ∧ P) → Q) → ((P ∧ P) → Q))

I'm hoping that this example is small enough that the dialogues website can compute both the D and E strategies for me.

---

ETA: This is still too complicated a formula for the site, so I calculated the D and E strategies by hand; they do differ, but only by the final two moves in two of the three branches [ETA, 23Jun: This is wrong; I did not finish filling out one of the branches]. I came up with a more interesting example:

(implies (implies (and p p) (implies p q)) (implies (and p p) (implies p q)))

Or, readable:

(((P ∧ P) → (P → Q) → ((P ∧ P) → (P → Q))

Here, not only does the game not immediately end when Pro asserts an atom (he does so in the attack on an implication, which means that Opp still has the possibility to defend), but the D and E strategies differ by the final four moves in two of the branches. If I can think of a way to nicely represent the trees in HTML, I'll try to post all four strategies here.

How do D and E diverge?

In order to understand how to get from D strategies to E strategies, I've been trying to think about cases where they diverge -- that is, dialogues which are D-strategies, but not already additionally E-strategies. Recall that we are in the presence of D11 and D13; by D11, an attack may be defended at most once, and by D13, a P-assertion can be attacked at most once. These put significant constraints on O. In fact, I've come to the conclusion that the only time when O will be faced with a choice is when P has attacked a conditional; then, and only then, O has a choice between defending the conditional and attacking its antecedent (assuming it is non-atomic). In either of these cases, it follows that the conditional was originally asserted by O.

Under what conditions will a conditional be asserted by O? In defense of \wedge_L, \wedge_R, or ?, or as an attack on a negation. The former imply that O has previously asserted a conjunction or a disjunction one of whose conjuncts/disjuncts is a conditional. Take the latter; this means that P has asserted a negated conditional. I have yet to come up with an example where P actually does so, but I'm wondering if it shouldn't be possible to construct one via substitution of such for an atom in a IL-valid formula. Hmmmm...

Well, I've found a formula which should be IL-valid and allows O to assert a conditional:

(implies (not (not (implies (and p p) q))) (not (not (not (not (implies (and p p) q))))))

Or, in more readable format:

(¬¬((P ∧ P) → Q) → ¬¬¬¬((P ∧ P) → Q))

However, at the point where O has a choice of moves, if he doesn't take the option of defending the attack on the conditional, then he loses it; the rest of the dialogue is so full of attacks on negations, which are undefensible and hence always remain open, that D11 will prevent him from going back and re-defending. So, in order for a D strategy to differ from an E strategy, (a) O must assert a conditional, (b) P must attack it, (c) O must defend it immediately.

The role of D11 and D12 in IL

Thinking more on what I wrote about a few days ago, I'm convinced of the redundancy of D12 ("An attack may be answered at most once") in the presence of D11 ("At any round, a player may defend against only the latest open attack made by the other player"). An easy proof:

The proof relies on the fact that once an attack has been defended, it is no longer open. Since D11 requires that every defense be made against an open attack, once an attack has been defended and is closed, no defense will be made against it again. Thus, any attack will be answered at most once.

This shows that D10-D11-D13 is a sufficient ruleset to generate IL. I kind of thought one of the results would be trivial; and this was it. I still think that it may be the case that D10-D12-D13 also characterizes IL, but I haven't had time to work further on that conjecture.

this is what happens when you think too much about dialogues

You start developing gut feelings; and the problem with gut feelings is that they are hard to transfer. It was a gut feeling about how N worked that led me to the characterization of implications in that system; and Jesse didn't believe me until he'd fully worked out a proof. Working with N meant focus on D10 and D13. Today, for reasons I'm not still entirely sure, I found myself back in Felscher's article, looking at D11 and D12, and suddenly I'm not seeing how they aren't redundant w.r.t. each other:

• D11: Only the latest open attack may be defended.
• D12: An attack may be answered at most once.

I got Jesse to set up two new rulesets on the dialogues site, D10-D11-D13, and D10-D12-D13, and after some simple playing around with the latter, I'm beginning to develop another feeling in my gut, namely that one or the other of these is sufficient to characterize IL, even though at this point I haven't a clue which. I would LOVE to find a counterexample to this gut feeling, but I've got a feeling there's no systematic way to go about finding one, and thus I must test it via hit-and-miss potential counterexamples. Hmmm. Or maybe I can find a nice axiomatization of IL and test each axiom in both sets. Would that really be enough?

What we've been up to

• Jesse and I revised our paper from the Inside Arguments Colloquium and submitted it for the proceedings: "What is Dialogical About Dialogical Logic?"
• The two of us along with Aleks Knoks have had a short paper accepted to TABLEAUX 2011 in July: "Dialogue Games for Classical Logic". Either Jesse or Aleks, or both, will be attending the conference.
• Jesse presented the long version of this paper at ProDi in Tübingen, as mentioned in an earlier post; Ole Thomassen Hjortland had some nice things to say about our results.
• Next big thing on the dialogical horizon is our 6-week visit to Vienna to work with Chris Fermüller, Christoph Roschger, and Friedrich Slivovsky.

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.

Presentation on dialogue games for classical logic at ProDi

I presented the result (joint with Sara and Aleks Knoks, whom we snagged to work on dialogues with us) on an extension of what I've been calling Fermüller-style dialogue games to classical logic. Fermüller gave a nice presentation of a dialogue game for intuitionistic logic, and presented a proof of the soundness and completeness of his games in his “Parallel Dialogue Games and Hypersequents for Intermediate Logics” (which was discussed earlier [Part 1], [Part 2], [Part 3], [Part 4]). Chris Fermüller was at the workshop and attended my talk. He didn't much like the name “Fermüller-style dialogues”, the idea being that his dialogues are at most a notational variant of ordinary dialogue games. I defended the choice of term by pointing out that the idea of extending his intuitionistic games to classical logic was more attractive and feasible than it is for other formalisms for dialogues. I think this is a case where a change of notation is significant.

As I expected, there was some pushback at the basic motivation of the paper, which is that our result is worthwhile owing to the extremely small number of explicit proofs in the dialogue literature of the correspondence between classical logic and classical dialogues (in whatever form one likes). We know of only two proofs, one by Fermüller himself, and another by Sørensen and Urzyczyn. Our proof has the advantage that it works with a standard sequent calculus, rather than with hypersequents (Fermüller) or one that is specially tuned for the purpose of establishing the correspondence (Sørensen and Urzyczyn).

It was an honor to present the work to an audience that contained several experts on dialogical logic. Here are the slides. The presentation was rather less than ideal: there were so many talks on dialogues preceding mine (not to mention that Fermüller himself presented his games immediately before me) that the first several slides could have been cut, and other interesting issues from the paper could have been dealt with. The paper on which the slides are based can be found on Sara's homepage or on my homepage.