Some notes on C. Fermüller's “Parallel dialogue games and hypersequents for intermediate logics” II: Dialogue sequents and states of the game

Yesterday's post on Fermüller's paper focused on the differences between his basic setup and Felscher's. Today I want to focus on some of the concepts that are most specific to Fermüller's approach. This is not to say that these concepts are absent from Felscher's paper. In fact, concepts similar to what I'm about to discuss probably do appear, in some form, in Felscher; the concepts are so basic, and in any case Fermüller credits Felscher but says that Felscher's techniques differ from his in some essential ways. The reason why I am not going to stop comparing Fermüller to Felscher at this point is because I've never managed to penetrate Felscher's paper in as much detail as I'm able to do with Fermüller's. One refreshing perspective in Fermüller's paper is the idea of moves in the dialogue acting on states:

Moves can be viewed as state transitions. In any state of the dialogue the (multiset of) formulas, that have been either initially granted or stated by O so far, are called the granted formulas (at this state). The last formula that has been stated by P and that either already has been attacked or must be attacked in O’s next move is called active formula. (Note that the active formula, in general, is not the last formula stated by P; since P may have stated formulas after the active formula, that are not attacked by O.) With each state of a dialogue we thus associate a dialogue sequent Π ⊢ A, where Π denotes the granted formulas and A the active formula.

Let's look at some examples illustrating this point of view of moves-as-transitions and see how the concept of granted formula, active formula, and dialogue sequent arise in some concrete games. In the following dialogue, and in all Fermüller-style dialogues in this post, the state column records what the dialogue state is after the move described in the first five columns in the same row. Thus the first row of the table doesn't record a move, but only displays the initial state of the dialogue.

Example 1: Fermüller-style dialogue for ∅ ⊢ p→p.

Move	Player	Statement	Stance	Reference	State	Notes
					∅ ⊢ p→p	1
0	O	p	Attack	—	p ⊢ p→p	2
1	P	p	Defend	0	p ⊢ p	3
2	O	p	Attack	1	p,p ⊢ p	4

Notes:

1. Initial state.
2. The active formula remains unchanged from the initial state, since P hasn't asserted anything yet.
3. Since there are no other formulas asserted by P at all and O must attack it, the active formula is now p.
4. The granted formulas of the dialogue sequence constitute a multiset. Since p has now been asserted twice by O, we have registered that.

For the sake of comparison, let's look at how a [maximal] dialogue (indeed, the only [maximal] dialogue) for p→p would go à la Felscher:

Example 1′: Felscher-style dialogue for p→p

Move	Player	Statement	Stance	Reference
0	P	p→p	—	—
1	O	p	Attack	0
2	P	p	Defend	1

One difference is, of course, the absence from the Felscher-style dialogue of a state and its associated dialogue sequent. (Again, I am not claiming that Felscher does not employ this concept in his proof of the soundness and completeness of dialogue games for intuitionistic logic; I'm saying only that I haven't come across the concept in my failed attempts to read his paper.) Nonetheless, it should be plausible that a Felscher-style dialogue can be converted to a Fermüller-style dialogue: if the initial formula is φ then the initial state of the game is ∅ ⊢ φ, and we can make the game end in the Fermüller-style dialogue by making O attack some atom asserted by P that has already been conceded by O (which makes sense in light of Felscher's rule D10). And it should be plausible that one can map Fermüller-style dialogues to Felscher-style dialogues when the set Γ of granted formulas is empty, and these transformations are inverses of one another. The devil is in the details, obviously, and my suggested transformations may break when one seriously considers the differences in the rules employed by Fermüller and Felscher. But it seems natural enough to me that Fermüller's approach is just a syntactic variation of Felscher's; I'm confident that Fermüller is not trying to diverge conceptually from Felscher, but he employs different notation to ease his proofs. To get a better sense of granted formulas, let's look at a second example of a Fermüller-style game.

Example 2: Fermüller-style dialogue for p ⊢ p

Move	Player	Statement	Stance	Reference	State	Notes
					p ⊢ p	1
0	O	p	Attack	—	p,p ⊢ p	2

Notes:

1. Initial state.
2. p is granted and copied to the left-hand side of the dialogue sequent from the previous state.

The game ends with a win for P because O has attacked a formula that has been granted. (In fact, the attacked granted formula is one of the initially granted formulas.) There is no Felscher-style analogue of this Fermüller-style dialogue because for the former there is no notion of formulas granted by O before the beginning of the game. Of course, the notion of non-initial granted formula makes sense for Felscher-style games: these are simply the formulas asserted by O during the course of the dialogue. To explore the concept of initially granted formulas, let's consider a further example:

Example 3: Fermüller-style dialogue for p∧p ⊢ p

Move	Player	Statement	Stance	Reference	State	Notes
					p∧p ⊢ p	1
0	O	?	Attack	—	p,p∧p ⊢ p	2
1	P	?L	Attack	p∧p	p,p∧p ⊢ p	3
2	O	p	Defend	1	p,p,p∧p ⊢ p	4

Notes:

1. Initial state.
2. The active formula is unchanged, since P hasn't asserted anything yet. p is now granted.
3. I'm assuming that the game can proceed in this way; I think that P can attack initially granted formulas. This makes sense to me for various reasons:
   • If the game actually ends at step 0 with a win for P, then there is no difference between the game for p ⊢ p and the game for p∧p ⊢ p, nor between p∧p ⊢ p and, say, p∧(p∨q) ⊢ p. Surely the game has to proceed by analyzing the initially granted formula p∧p.
   • If the game does not end at step 0, then P has to either attack or defend. But surely he can't defend, since there's no attack against which to defend.
   For lack of any other notation, I've set the reference sot for this move as the intially granted formula p∧p (there's no number that I could put there, and I don't want to put simply “—”). The active formula remains unchanged, since ?_L isn't a formula.
4. p occurs twice in the multiset of granted formulas because it has been asserted twice now by O. This suggests, to my mind, some inefficiency in the mapping that will eventually be constructed from winning strategies to sequence calculus deductions in intuitionistic logic. These simple examples suggest to me that perhaps not all intuitionistic sequent calculus deductions will arise as the result of mapping winning strategies to derivations, but only those with some extra, redundant assumptions occurring on the left-hand side of ⊢.

This example puzzles me. I'd like to say that P wins this game: obviously p∧p ⊢ p is intuitionistically valid, so P ought to have a winning strategy for it, and the winning strategy ought to be very simple. I'd like to say that the dialogue above (when regarded as a linear dialogue tree) actually is a winning strategy for P. But it feels weird to say that P wins here, because it feels that now P is trapped: he cannot attack p (by Atom). Fermüller does not include any non-repetition rules in his ruleset, so I suppose that P could repeat an earlier move or, say, re-attack the initially granted formula p∧p with ?_R. But what good would that do? I must be missing something about the use of initially granted formulas and the ipse dixisti rule. Or maybe I don't understand one of the winning conditions: does P win here because O has granted a formula (at step 2) that he attacked earlier (at step 0)? Frustratingly, the ipse dixisti rule is not defined by Fermüller; I can only guess that it has something to do with the winning condition for P; the only reference I have at hand that talks about the ipse dixisti rule, Krabbe's “Formal systems of dialogue rules” (Synthese 63, 1985, pp. 295–328) says that the ipse dixisti rule is a a “‘winning remark’ that ends (at least a part of a) dialogue” (p. 300). This is frustrating for me, because I need to know precisely how this game will go if I am to understand Fermüller's proofs. Perhaps from the proofs, though, I'll be able to reconstruct what exactly the force of the ipse dixisti rule is. Let's look at a more complex example: one of the De Morgan formulas. Here's a Fermüller-style dialogue:

Example 4: Fermüller-style dialogue for ∅ ⊢ ¬(p∨q)→(¬p∧¬q)

Move	Player	Statement	Stance	Reference	State	Notes
					∅ ⊢ ¬(p∨q)→(¬p∧¬q)	1
0	O	¬(p∨q)	Attack	—	¬(p∨q) ⊢ ¬(p∨q)→(¬p∧¬q)	2
1	P	¬p∧¬q	Defend	0	¬(p∨q) ⊢ ¬p∧¬q	3
2	O	?L	Attack	1	¬(p∨q),¬p ⊢ ¬p∧¬q	4
3	P	¬p	Defend	2	¬(p∨q) ⊢ ¬p	5
4	O	p	Attack	3	p,¬(p∨q) ⊢ ¬p	6
5	P	p∨q	Attack	0	p,¬(p∨q) ⊢ ¬p	7
6	O	?	Attack	5	p,¬(p∨q) ⊢ ¬p	8
7	P	p	Defend	6	p,¬(p∨q) ⊢ p	9
8	O	p	Attack	7	p, p,¬(p∨q) ⊢ p	10

Notes:

1. Initial state.
2. O grants ¬(p∨q). Active formula is unchanged. (It never changes after O moves.)
3. The active formula is now ¬p∧¬q because O must attack this new statement by P. In general, any time P defends, the next move by O is an attack on whatever P just asserted, thanks to the E rule.
4. ¬p is now granted.
5. The active formula is now ¬p, because P just defended. See note 3.
6. p is now granted.
7. The active formula is unchanged because O does not need to attack this formula, because he could defend against the attack at move 5 by asserting ⊥ (recall that “¬(p∨q)” is actually (p∨q)→⊥). At step 6, O will in fact attack the disjunction asserted by P at step 5; the point is that, when calculating what formula is active, one needs to consider what Omust do.
8. The state after this move is identical to the previous two states!
9. p is now the active formula because P just asserted p as a defense. See note 3.
10. p has now been granted twice. Again we see a bit of redundancy in the assignment of sequents to dialogue states.

The game ends at move 8 with a win for P because O just attacked a formula that he already granted at step 4. The game could have gone differently: at step 6, for example, O could have defended against the attack at move 5 by asserting ⊥, which would have led to a loss for him at that step. And of course O could have asked O to defend the right conjunct rather than the left one at step 2. There are even more ways the game could have gone, but these alternatives need not distract us here. For comparison, here is the Felscher-style game analogous to the one of Example 3:

Example 4&prime: Felscher-style dialogue for ¬(p∨q)→(¬p∧¬q)

Move	Player	Statement	Stance	Reference
0	P	¬(p∨q)→(¬p∧¬q)	—	—
1	0	¬(p∨q)	Attack	0
2	P	¬p∧¬q	Attack	1
3	O	?L	Attack	2
4	P	¬p	Defend	3
5	O	p	Attack	4
6	P	p∨q	Attack	1
7	O	?	Attack	6
8	P	p	Defend	7

The Felscher-style game ends here because there are no more moves availabe for O to make at this point. So much for concrete dialogue games à la Fermüller. One can then see how Felscher-style dialogue trees are, because these are simply derived from treating Fermüller-style dialgues. Of course, all of the examples above of Fermüller-style dialogues can be regarded as extreme cases of Fermüller-style dialogue trees if we simply ignore all possible branching (which does exist whenone considers the De Morgan formula of Example 4, but not in the other dialogue sequents, owing to their simplicity). Next up in this series on Fermüller's paper: a discussion of Fermüller's proof of his Theorem 1, on the soundness of Ei-dialogues for intuitionistic validity (i.e., Proponent has a winning strategy for a formula φ iff φ is intuitionistically valid).