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.