returning to the role of E

One of the original motivations our work with Chris here in Vienna started with is contexts under which we can show that E is redundant; IL is an obvious case, and hence D10+D11+D13 is as well. D10+D12+D13 was a surprising (to some) countercase. CL is an obvious countercase...or is it?

It appears that the unique redundancy of E in IL noted above is actually closely tied to Felscher's formulation of the rules. If we stray from there (keeping E: "The Opponent must immediately respond to the previous Proponent move") and start formulating rules on our own, can we perhaps come away with sets of rules where the presence or absence of E is irrelevant?

When we talked about this a few days ago, my conjecture was that it's not the immediate-response consequence of E that is so important for CL, but rather the restriction on the number of moves O can make. I propose the following:

• D10: P cannot assert an atom before O does.
• D13: A P-statement can be attacked at most once.
• D14: A P-attack can be defended at most once.

Certainly D10+D13+E implies D10+D13+D14. But D10+D13+D14 does not imply E, since it relaxes the immediate-response constraint.

So one hypothesis for how to go about constructing rules that would allow us to prove the redundancy of E in a particular ruleset is by looking at variants of the bounded rules that Krabbe proposed in his 1985 Synthese article which put constraints on the number of times O can repeat a move.

However, if you are in the context of E, what is it that separates IL from CL? It is the ability of P to go back and essentially "change his mind" about a defense, e.g., in the case of excluded middle. So here, it appears that the important distinction is not how many times O can repeat a move, but how many times P can. The case is not quite the same, though: In IL, there are contexts where P is allowed to repeat a move (same formula/symbolic attack, same stance, same reference), and in CL, it is not that we are allowing P to repeat a move that he's already made, but rather to re-refer to a move of O that he's already referred to. So the cases aren't quite parallel, but it still shows a tantalizing dimension to consider.

Characterizing classical logic dialogically

Here's a simple question:

Do we know how to characterize classical logic (CL) dialogically?

The answer is, thankfully, “yes”. Various proofs are available. Together with a masters student at the ILLC, Aleks Knoks, Sara and I found a correspondence between LK deductions (more precisely, deductions in a proof search-friendly variant of LK) and (what we called) classical dialogues. (Our proof does not literally use Felscher's notation for dialogue games; instead, we extended Fermüller's notation, found in his “Parallel dialogue games and hypersequents for intermediate logics”. It's clear that there's no essential difference between Fermüller-style games and Felscher-style games.

Here's a related question:

How do we characterize CL using Felscher-style dialogues?

The question is motivated by a desire to find some general framework for dialogues in which we can understand how the E-rule above is redundant. The motivating example is the dialogical characterization of intuitionistic logic (IL): it turns out that the E-rule is redundant in the presence of other structural rules. One way to understand the redundance of E is to look at other logics and their dialogical characterizations. Is the E rule redundant for these, too?

Turing to classical logic, the salient structural rules are:

D11

Defenses must be against only the most recent open attack. (An attack is said to be open if there is no defensive move in the game that responds to the attack. Non-open attacks are closed.)

D12

Attacks may be answered at most once.

E

O must react to the immediately preceding statment by P.

Based on the work mentioned before, I'm pretty sure that one way to get CL is to keep E but remove the other two rules. But this is, for the present discussion, a negative example because the E rule, far from being redundant, is crucial. We can't drop all three of these conditions. The result of doing so is the curiosity N; and we have known for some time that N ≠ CL. This leaves open some other questions: what if we keep D11 or D12? Do we find that E is redundant in those cases as well?

Sara's recent slick observation about the redundancy of D12 helps with this, but we still have some work to do.

two more conjectures

The first one is wholly my own, and this one I have a lot less data to base it on than others, and I can't even really say why I think it might be true. However, it's something for me to spend some time (using the nifty new "search for a strategy (interactively)" functionality, which I am loving) investigating, and it doesn't seem prima facie false:

Conjecture: Let s be a winning E-strategy for phi. Extend s to s' by augmenting the tree wherever required so that the result is a winning D-strategy. Claim: The E-violating moves will occur after P has asserted an atom.

Check back often for evidence for or against this conjecture.

The second one is one that Chris proposed, namely whether D10+D12+D13=CL (i.e., we drop E, but add D12). Now, you might recall from a week or two ago that I conjectured that D10+D12+D13=IL, not CL (and I already have an easy proof that D10+D11+D13=IL), so it will be interesting to see how this pans out.

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.

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...