[FOM] speaking of provability logic

[Craig Smorynski]

In a discussion of the fixed point theorem in provability logic and a new proof by Lisa Reidhaar-Olsen Giovanni Sambin makes a few remarks on its history and suggests Dick de Jongh or I should add something.

It was several decades ago, but I recall that when I was in A'dam working on my chapter for the Handbook of Mathematical Logic, Dick informed me of work he and Martin Hugo Löb had been working on on provability logic. They had proven some basic results, among which included the uniqueness of the fixed points. I suggested that explicit definability had to follow by Beth's Theorem, but he said that no one had proven Beth's Theorem. In a short time I had proven the explicit definability in the case where there were no variables other than the fixed point. I then left for Chicago for Christmas and when I returned Dick informed me that he had given a model theoretic proof of the full result. As a result of my reporting on this stuff in an overblown draft of my Handbook article, we got a flood of papers from Sienna. Claudio Bernardi had proven the uniqueness result and explicit definability in the same case as I had. My proof gave a simple procedure for finding the fixed points in a normal form, which I don't believe his more topological argument did, so I was well pleased with myself.

Soon Dick and Giovanni independently gave syntactic proofs of the full explicit definability result. I gave a little survey talk on this at one of the European ASL meetings, but the paper was too long for inclusion in the proceedings so I substituted a new proof using Beth's Theorem which I had proven via the Joint Consistency Theorem. At the same time Boolos had proven the result via interpolation proof theoretically.

Boolos, of course, also gave a model theoretic proof of the full result in his book. Being lazy and knowing the simple syntactic proof I did not read over his proof too carefully and in describing it in my own book miscalculated the bounds on the sizes of Kripke models one would have to search through to find the fixed point. My memory for details never having been great I cannot specify who or where, but a paper pointing out my error was rejected from some journal despite my positive report.

A few years later Julia Robinson arranged for me to write a survey paper in the Bulletin of the AMS and I invented my fixed point algebras as an expositional device and proved that the uniqueness result held for finite such algebras on simple group theoretic grounds, an old result of Burnside to be exact.

To this I can add that whenever it was that I was in Buffalo Kathy Kessel proved the interpolation theorem for the provability logic of the Mostowski operator declaring provability in one of a list of theories.

And, of course, there are the non-uniqueness results of Dave Guaspari and Robert Solovay for the Rosser sentence.
Craig



-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20120523/91048423/attachment.html>