Sunday, September 12, 2010

Background to constructive provability logic

So after some off-line discussions, while I continue to feel like the natural-deduction based judgmental methodology really maybe isn't the best way to do the work of experimentally developing logics (you really want the sequent calculus version for that - but that's another post), it's an excellent storytelling device. The idea is that it should help you explain a logic that is initially non-intuitive to an audience that you're trying not to scare off.

I'm not even certain how fully I believe that, since I tend to like using sequent calculus presentations for more-or-less everything that isn't a programming language. However, this tech report, by forcing me to work through a lot of things very carefully, has clarified my views on a lot of things - in particular, I think I have a "modern formulation" of the judgmental methodology that neatly generalizes to things like substructural logics without going out of its way, while simultaneously doing a good job of putting on paper all the tricks I learned from Dan about formalizing logics in Agda.

My wildest hope is that this story can motivate to Random J. PLPerson not only what Bernardo and I are doing specifically, but also give the intuition behind a number of things I've learned from Noam Zeilberger and Dan Licata about the philosophy behind both higher-order focusing and behind doing logic in Agda, and without actually requiring any background with focusing or knowledge of Agda to get there. I'd be happy to hear from you whether you think I've succeeded: any criticism would be greatly appreciated. (Draft Technical Report: Constructive Provability Logic)


  1. Link's broken! You forgot the http.

    The story you tell makes plenty of sense, although I wonder about how smooth you can make the transition to reflecting provability...

  2. saw the paper now, and have two thoughts/suggestions: 1. you could try giving a "shallow embedding" in Agda, which would basically be a Kripke semantics---is there a Kripke semantics for constructive provability logic? 2. you could try encoding the proof theory in Twelf, via defunctionalization---I've found that to be very useful for understanding what's going on in these mixed data/computation encodings, because you're forced to be more explicit.

  3. I'm actually very uncertain that there's any straightforward Kripke semantics of this logic because the reflection mechanism is kind of goofily powerful. There's a particular non-proof argument for why the logic with atomic propositions probably isn't axiomatiziable that I need to recall and put in the T.R.

    My current goals basically are to get the proof theory (sequent calculus and natural deduction) story clearly written out for minimal CPL. One thing I've noticed is that the "intermediate" setting in 2.2 is also something that it might be very interesting to study, and I think your suggestions are likely to be more fruitful to consider there.