Next up, Laurent Keiff, "Dialogues and Trivializing Connectives". This should be interesting, as one of the questions he's asking is "What are the limits of the framework?", which is closely related to questions Jesse and I explored last fall.
His definition of dialogue games follows the approach of Fermüller; there is an initial set of assertions by the Opponent, and he indicates positions of games via dialogue sequents. However, he only allows one assertion of Proponent in the initial state, so his dialogues are, at base, intuitionistic.
For Keiff, particle rules must be "anonymous"; this is just player neutrality at the local level. Unfortunately, he doesn't give sufficiently precise definitions of the particle and structural rules to evaluate whether the same worry that I have from Rahman's paper is present here.
Much of his talk is focusing on developing rules for tonk, and tonk-like operators. I have to confess, I'm not entirely sure I understand the fascination the Lille people have with tonk. It seems like it will always be possible to allow, or not allow, tonk rules. This, in and of itself, is not problematic, any more than the fact that classical proof theory allows the introduction of a tonk rules. What's important is that we can block the adoption of tonk, that we're not forced to use it. So, if we're interested in investigating interesting logics that arise from the dialogical tradition, we should avoid adding trivializing connectives like tonk.
No comments:
Post a Comment