Unlike this blog post, which I wrote in 15 minutes while tired, Bernardo and I have worked very, very hard on trying making this report foundational and clear, and I'd definitely appreciate any feedback people have (large and small) since hopefully this won't be the last time I talk about constructive provability logic. Even if the feedback is that my jokes are really dumb and don't add anything to the paper (I should mention for Bernardo's sake that all the dumb jokes are my fault).
Principles of Constructive Provability LogicThe topic of the paper is "constructive provability logic" (CPL), a rich vein of logic that we've only just begun exploring.1 The abstract and the introduction point out our primary reason for being interested in this logic: we want to give a general, satisfying, and proof-theoretic account for negation in logic programming. In fact, I've already gone out on a limb and written out the design of a distributed logic programming language based on a variant of CPL that I haven't quite-just-yet gotten around to entirely writing down. But I'm also just starting to implement the logic programming language, so it's not like I'm that far ahead of myself. The classical modal logic (which has about a dozen names but let's call it GL for Gödel-Löb) that we're intuitionisticing2 about with has deep connections to everything from Gödel's incompleteness theorems to the denotational semantics of programming languages (it's the "modal" in the very modal models).
Robert J. Simmons and Bernardo Toninho.
[PDF], [Agda tarball], and [Agda HTML]
Abstract: We present a novel formulation of the modal logic CPL, a constructive logic of provability that is closely connected to the Gödel-Löb logic of provability. Our logical formulation allows modal operators to talk about both provability and non-provability of propositions at reachable worlds. We are interested in the applications of CPL to logic programming; however, this report focuses on the presentation of a minimal fragment (in the sense of minimal logic) of CPL and on the formalization of minimal CPL and its metatheory in the Agda programming language. We present both a natural deduction system and a sequent calculus for minimal CPL and show that the presentations are equivalent.
What's so special about this logic? Well, when you're working in the Kripke semantics of a modal logic, you should think of yourself as standing and a particular world and looking at some other worlds (these worlds are called accessible, and an accessibility relation determines which worlds are accessible). Maybe there aren't any! Maybe there are. Maybe you can see the world you're standing on, like being in a hall of mirrors. Maybe you can see one other world, and then beyond that world you can see back to the world you're standing on, like being in Pac-Man. The situation for GL and CPL is that not only can you not see yourself, you can't see forever - you can look past the accessible worlds to the worlds accessible from those (the "2-accessible" worlds, say) and then to the 3-accessible worlds... but this can't go on forever (jargon: the accessibility relation is "converse well-founded," there are no infinite ascending chains).
If you find yourself in a planetary system with a converse well-founded accessibility relation such as this one, the key is that, if you ever find your spaceship and go to one of those accessible worlds, there's now strictly less to see. Put another way, there's necessarily a little more going on where you're standing than in the places you're looking at. If this leads you to think that the places you can see are kind of an approximation of the place where you are, you're heading towards the approximation ("modal model"-esque) interpretation of GL. If you think "oh, the little more going on could refer to logical consistency," then you're heading towards the "provability" interpretation of GL. Perhaps the provability interpretation will inspire you to send a logician on every world and allow each logician to reason about the logical consistency of all the logicians he can see.3 Sure, you'll never get enough watchers for all the watchmen, but that is an occupational hazard of modern mathematics.
Anyway, I'll stop there: hopefully the details in the tech report are much, much clearer than the discussion in the preceding few paragraphs.
1 I don't know when I started referring to my life as "working in the logic mines," it's really not fair to miners who have a really hard job that often isn't fun, unlike me. Maybe I'm just jealous of Mary's hat
2 Intuitionisticing. v. To experimentally take a classical logic and try to deduce constructive, intuitionistic principles and proof theories out of it: Rowan and Alex were intuitionisticing about with propositional S4, and they both came up with things that seemed internally consistent but that were oddly incompatible.
3 Hey! It's a bad idea to use male pronouns to describe mathematicians! Okay, would you rather me be shooting female logicians into space for no compelling reason? Alright then.
Posts
Hi Rob,
ReplyDeleteThis seems to be really interesting work, in particular, on the possible connections with X10. I should probably read the tech-report, but after a quick look through the L10 example program (with path, noedges, etc), I was wondering whether it would be possible to extract worlds from a logic program. That is, instead of writing the signature with the pairs (predicate name, signature), one could extract this signature from the program. Since programs are stratified, one could use the stratification itself to assign the worlds to the predicate names. Would that be right?
Another thing, can you also capture locally stratified programs?
Best,
Vivek
So it's worth doubly-emphasizing that the L10 design is still ahead of the logic - Bernardo and I have ideas on how to do first-order CPL, but basically we're running so "close to the guardrails" with this that I hesitate to make claims that we haven't at least verified in Agda.
ReplyDeleteStratified negation for the propositional fragment, at least, is something I claim to understand (though it's not in the tech report, the idea behind it was sketched in our previous course project and it's not too hard to work out). And absolutely, in that fragment you could synthesize an accessibility relation for any stratified logic program. The idea behind the preliminary specification is to get all the "type" information written down, and then think about (optionally) synthesizing it.
Locally stratified negation is described in one of the L10 examples. However, the way I currently know how to do this with constructive provability logic seems to involve signatures with countably infinite rules (one for every "locally stratified" world). A satisfying solution would seem to involve a form of *quantification over first-order worlds* that I don't claim to fully understand yet.