This book, written by one of the most distinguished of contemporary philosophers of mathematics, is a fully rewritten and updated successor to the author's earlier The Unprovability of Consistency. Its subject is the relation between provability and modal logic, a branch of logic invented by Aristotle but much disparaged by philosophers and virtually ignored by mathematicians. Here it receives its first scientific application since its invention. Modal logic is concerned with the notions of necessity and possibility. What George Boolos does (...) is to show how the concepts, techniques, and methods of modal logic shed brilliant light on the most important logical discovery of the twentieth century: the incompleteness theorems of Kurt Godel and the 'self-referential' sentences constructed in their proof. The book explores the effects of reinterpreting the notions of necessity and possibility to mean provability and consistency. (shrink)

Solovay proved (Israel J Math 25(3–4):287–304, 1976) that the propositional provability logic of any ∑2-sound recursively enumerable extension of PA is characterized by the propositional modal logic GL. By contrast, Montagna proved in (Notre Dame J Form Log 25(2):179–189, 1984) that predicate provability logics of Peano arithmetic and Bernays–Gödel set theory are different. Moreover, Artemov proved in (Doklady Akademii Nauk SSSR 290(6):1289–1292, 1986) that the predicate provability logic of a theory essentially depends on the choice of a binumeration of the (...) theory which is used to construct the provability predicate. In this paper, we compare predicate provability logics of I∑ n ’s. For a binumeration α(x) of a recursive theory T, let PL α(T) be the predicate provability logic of T defined by α(x). We prove that for any natural numbers i, j such that 0 < i < j, there exists a ∑1 binumeration α(x) of some recursive axiomatization of I∑ i such that ${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsupseteq \bigcap_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$ and ${{\sf PL}_\alpha({\rm I \Sigma}_i) \nsubseteq \bigcup_{\beta(x)}{\sf PL}_\beta({\rm I \Sigma}_j)}$ , where β(x) ranges over all ∑1 binumerations of recursive axiomatizations of I∑ j. (shrink)

Vardanyan's theorem states that the set of PA-valid principles of Quantified Modal Logic, QML, is complete Π0 2. We generalize this result to a wide class of theories. The crucial step in the generalization is avoiding the use of Tennenbaum's Theorem.

Solovay proved the arithmetical completeness theorem for the system GL of propositional modal logic of provability. Montagna proved that this completeness does not hold for a natural extension QGL of GL to the predicate modal logic. Let Th(QGL) be the set of all theorems of QGL, Fr(QGL) be the set of all formulas valid in all transitive and conversely well-founded Kripke frames, and let PL(T) be the set of all predicate modal formulas provable in Tfor any arithmetical interpretation. Montagna’s results (...) are described as Th(QGL) ⊊ (Fr(QGL), PL(PA) ⊈ Fr(QGL), and Th(QGL) ⊊ PL(PA). In this paper, we prove the following three theorems: (1) Fr(QGL) ⊈ PL(T) for any Σ1-sound recursively enumerable extension T of I Σ1, (2) PL(T) ⊈ Fr(QGL) for any recursively enumerable S1755020312000275_inline1 A -theory T extending I Σ1, and (3) Th(QGL) ⊊ Fr(QGL) ∩ PL(T) for any recursively enumerable S1755020312000275_inline2 A -theory T extending I Σ2. To prove these theorems, we use iterated consistency assertions and nonstandard models of arithmetic, and we improve Artemov’s lemma which is used to prove Vardanyan’s theorem on the Π0 2-completeness of PL(T). (shrink)