*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 byLet'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 isOso far, are called thegranted formulas(at this state). The last formula that has been stated byPand that either already has been attacked or must be attacked inO’s next move is calledactive formula. (Note that the active formula, in general, isnotthe last formula stated byP; sincePmay have stated formulas after the active formula, that are not attacked byO.) With each state of a dialogue we thus associate adialogue sequentΠ ⊢A, where Π denotes the granted formulas andAthe active formula.

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

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 |

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

*p*→

*p*would go à la Felscher:

Move | Player | Statement | Stance | Reference |
---|---|---|---|---|

0 | P | p→p | — | — |

1 | O | p | Attack | 0 |

2 | P | p | Defend | 1 |

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

Move | Player | Statement | Stance | Reference | State | Notes |
---|---|---|---|---|---|---|

p ⊢ p | 1 | |||||

0 | O | p | Attack | — | p,p ⊢ p | 2 |

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

**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:

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 |

- Initial state.
- The active formula is unchanged, since
**P**hasn't asserted anything yet.*p*is now granted. - 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.

*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. - If the game actually ends at step 0 with a win for
*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 ⊢.

**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:

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 |

- Initial state.
**O**grants ¬(*p*∨*q*). Active formula is unchanged. (It never changes after**O**moves.)- 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. - ¬
*p*is now granted. - The active formula is now ¬
*p*, because**P**just defended. See note 3. *p*is now granted.- 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**O***must*do. - The state after this move is identical to the previous two states!
*p*is now the active formula because**P**just asserted*p*as a defense. See note 3.*p*has now been granted twice. Again we see a bit of redundancy in the assignment of sequents to dialogue states.

**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:

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 |

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

## No comments:

## Post a Comment