Friday, February 25, 2011
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.
First, structural rules which are wholly player neutral will result in the inconsistent logic: Proponent has a winning strategy for every atom p, so at least some asymmetry/nonneutrality in the rules is required.I am curious to see if he addresses this problem in the remainder of the talk; if he doesn't, I intend to ask him about it. Curiously, at least one version of particle rules for FDE-negation that he introduces is not player neutral. --- I asked my question; I don't think I was able to express myself clearly, because his answer was "of course you have to have some asymmetry" in order to build a logic. So I'm not sure what his motivation for arguing for player neutrality is, nor how he gets the required asymmetry from his symmetric particle rules.
Tuesday, February 8, 2011
- "Dialogue Games for Classical Logic". In this paper we introduce a class of dialogue games for classical logic, building on both Felscher 1985 and Fermüller 2003, and give a rigorous proof of the correspondence between the two.
- A Tableau System for the Dialogical Logic N". In this paper we define a tableau system for the logic N, and prove that it is sound and complete with respect to the logic. The proofs go via a reduction to canonical tableaux and algorithms for converting closed tableaux into winning strategies and vice versa.