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.
I believe I've found a proof that the N rules plus D14 gives us CL and that the E rule is redundant for this ruleset. That is, I believe have proofs for:
ReplyDelete(1) there exists a winning N+D14 strategy for A iff A is a tautology
(2) there exists a winning N+D14+E strategy for A iff there exists a winning N+D14 strategy for A.
The proof of (1) is a modification of the proof that we used for the Ei ruleset in our "Dialogue games for classical logic".
I believe I also have proofs that deal with classical logic in the context of the ruleset N+No-Repetitions, and proofs that E is redundant for this ruleset as well.
Cool. Exactly in line with what we expected.
ReplyDeleteFor (2), how do you prove the N+D14+E -> N+D14 direction?
ReplyDeleteI think I also have a (certainly similar and perhaps equivalent result):
ReplyDeleteLet CL'= {D10 + D3,1,∞ + D4,1,∞}. P has a winning CL'-strategy for φ iff he has a winning CL-strategy for φ.
Proof.
(⇐) E implies D13, which is equivalent to D4,1,∞, and E implies D3,1,∞. Thus, any CL-strategy will also be a CL'-strategy.
(⇒) Proved analogously to the proofs of the bold conjectures for IL.