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:
- 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.)
- Attacks may be answered at most once.
- 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.