Quantified modal logic and self-reference.
C. Smoryński · Notre Dame Journal of Formal Logic · 1987
Quantified Modal Logic and Self-Reference C. SMORYNSKIThe propositional modal logic of provability, which I denote PrL for Provability Logic, has proven to be a useful tool in studying self-reference in Peano Arithmetic, PA.The three chief results about PrL are: (i) Solovay's Completeness Theorems, (ii) the de Jongh-Sambin Theorem, and (iii) the Uniqueness Theorem.Solovay's First Completeness Theorem asserts that PrL is the modal logic of provability in PA, i.e., it axiomatizes those schemata in the language of D which are provable in PA.Solovay's Second Completeness Theorem tells what schemata are always true assertions when interpreted in the language of arithmetic.These results are not only aesthetically pleasing, but they, particularly the Second Theorem, are extremely useful in establishing incompleteness results-the prototypical applications of self-reference.The de Jongh-Sambin Theorem and the Uniqueness Theorem, although they do not help in establishing the results obtained by self-reference, do tell us something more about self-reference itself: According to the de Jongh-Sambin Theorem, for all reasonable modal formulas A (p), there is a modal formula D not containing p and such that PrL \-D +-> A (D); the Uniqueness Theorem, due independently to Bernardi, de Jongh, and Sambin, asserts that the fixed point to A (p) is unique.Whenever one decides to expand the context of the discussion, the first question one asks is whether or not these three results carry over.Thus, for example, in their analysis of Rosser sentences, Guaspari and Solovay expanded the language of PrL to accommodate the Rosser trick of comparing witnesses to provability assertions, added a few axioms about these comparisons, proved the completeness of their system with respect to arithmetic interpretations, and then applied this result to show the failure of the Uniqueness Theorem and to make a few observations on definability.In studying multimodal logics and their interpretations, one finds the same results: Suppose, e.g., one has two modal operators D and Δ to be interpreted as provability in PA and ZF, respectively.Carlson has proven three completeness theorems for axiomatizing the schemata