Provability as Modality

Abstract

Although the idea of provability as modal necessity is hardly novel, the serious study of the modal logic of provability did not get underway until the 1970s. There were early flirtations with the idea, but they never amounted to anything: About the time his Incompleteness Theorems gave him instant fame (among mathematicians and philosophers), Gödel wrote up a short note on an embedding of intuitionistic logic into modal logic. The idea behind the embedding was simple: Intuitionistic truth is defined in terms of proof and provability is necessity. Composition yields the embedding. Gödel never bothered (so far as anyone knew before his death— his Nachlass may, or may not, reveal otherwise) to connect this modal view of provability with his self-referential one.