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