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)
Subscribe to:
Post Comments (Atom)
Posts
Link's broken! You forgot the http.
ReplyDeleteThe story you tell makes plenty of sense, although I wonder about how smooth you can make the transition to reflecting provability...
Oops! Fixed.
ReplyDeletesaw 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.
ReplyDeleteI'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.
ReplyDeleteMy 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.