Live Blogging - ProDi Day 1, part 2

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.

Meta

Having not yet had any time to write a proper blog post, I thought I would take a few minutes to at least write a post about posts I am going to write when said time magically appears. The first question Jesse and I considered, and the one that eventually led him to think of and formulate the composition problem, was one that I thought was relatively simple: Given a classically valid formula $\phi$ and the Gödel-Gentzen translation $\phi^n$ of $\phi$, is there a (uniform) way of translating the winning strategy for $\phi$ in the classical game into a winning strategy for $\phi^n$ in the intuitionistic game? What the composition problem has shown us is that this is not an easy question to answer partly because it is not clear what a "winning strategy in the classical game" is. So answering that question will be a long time off and in the meantime I'm going to be much more modest in my aims, and I've come up with a number of much, much more basic questions that I hope to answer, whose answering I also hope will help me come up with some intuitions about how dialogical proofs work (since currently I have none). These are the issues I hope to explore in future blog posts: - The "solution" to the "weakening" problem: We discussed this in Ponta Delgada and I think convinced ourselves that the weakening problem does indeed have a solution, but for now the scare quotes are necessary because we haven't anything like a proof. - Why DN is so important in differentiating classical logic from intuitionistic logic. - What would particle rules for TONK look like? - Is there anyway to get an inconsistent logic other than dropping the requirement that P cannot assert an atomic formula unless O has already asserted it? - How symmetric can you make the structural rules (so that they treat O and P the same) and still get a logic? Some tantalizing topics for future discussion...