Wednesday, November 07, 2007

Proofs and provability

Earlier today I had a thought about proof theory. Proof theory is, roughly, a formal investigation of the properties of proof systems. (I sort of dig proof theory.) Provability logic is an interpretation of modal logic. It has its own axiom set distinct from S5 and it was, I believe, originated by Goedel and greatly elaborated by Los and Boolos. It assigns the interpretation "is provable" to the box instead of the normal alethic interpretation. So, '[]p' is read as 'p is provable'. Now, the question I have is: what is the relation between proof theory and provability logic? The contexts in which I've seen provability logic didn't connect it to proof theory and those in which I've studied proof theory didn't connect to provability logic. It seems like a big flaw for at least one of the two if there is no connection. Glancing at the SEP reveals that there is at least one article on this topic: Beklemishev, L.D., “Parameter-free Induction and Provably Total Computable Functions,” Theoretical Computer Science, Vol. 224 (1999): 13-33. I haven't tracked this down yet, but I'm going to venture a guess that it isn't too philosophical. (Of course, I could be wildly wrong on this count.) In any case, at the moment I'm not sure what the relationship between provability logic and proof theory is and I have no idea what it should be.


Kenny said...

I remember learning a little bit of provability logic in Johan van Benthem's modal logic class at Stanford. At any rate, I seem to recall that the characteristic axiom was []([]p->p)->[]p, which they called Loeb's Theorem. There's a proof-theory argument for that.

I think once you've got that axiom though, the argument from Godel's first incompleteness theorem to the second is very quick, and can be written in modal terms. At least, I once was familiar enough with this stuff that I remember writing a proof something like that down on my preliminary exam in logic.

Shawn said...

The bit I learned about provability logic was from van Benthem's modal logic class as well. He did say something along the lines of: the core of the second incompleteness theorem could be stated entirely in the modal language. That is an interesting result, that the proof only uses things reasoning that can be captured in the restricted modal language. I think he did say there were parts of the proof, technical details, that needed the expressive power of first-order languages, but the important parts of the proof were expressible in the modal language. That is an interesting connection, but it seems to me that there should be more of a connection between the two. That might be the way into the connection though.