We formulate a Π1 sentence τ which is a version of the Tableau consistency of GlΔ0. The sentence τ is true and is provable in GlΔ0 + exp. We construct a model M of GlΔ0+Ω1+τ+BGs1 which has no proper end-extension to a model of GlΔ0+Ω1+τ. Also we prove that GlΔ0+Ω1+τ is not Π1 conservative over GlΔ0+τ.

This paper contains a careful derivation of principles of Interpretability Logic valid in extensions of I0+1.

Let PLω be the provability logic of IΔ0 + ω1. We prove some containments of the form L ⊆ PLω < Th(C) where L is the provability logic of PA and Th(C) is a suitable class of Kripke frames.

For any countable nonstandard modelM of a sufficiently strong fragment of arithmeticT, and any nonstandard numbersa, c εM, M⊨c≦a, there is a modelK ofT which agrees withM up toa and such that inK there is a proof of contradiction inT with Gödel number $ \leqq 2^{a^c } $.

It is shown that for arithmetical interpretations that may include free variables it is not the Guaspari-Solovay system R that is arithmetically complete, but their system R –. This result is then applied to obtain the nonvalidity of some rules under arithmetical interpretations including free variables, and to show that some principles concerning Rosser orderings with free variables cannot be decided, even if one restricts oneself to usual proof predicates.

Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof be replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic (the so-called Rosser logic of Gauspari-Solovay, 1979) so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in (...) particular I0+EXP. The method is adapted to obtain a similar completeness result for the Rosser logic. (shrink)

To the standard propositional modal system of provability logic constants are added to account for the arithmetical fixed points introduced by Bernardi-Montagna in [5]. With that interpretation in mind, a system LR of modal propositional logic is axiomatized, a modal completeness theorem is established for LR and, after that, a uniform arithmetical (Solovay-type) completeness theorem with respect to PA is obtained for LR.

The modal completeness proofs of Guaspari and Solovay (1979) for their systems R and R – are improved and the relationship between R and R – is clarified.

It is shown that for arithmetical interpretations that may include free variables it is not the Guaspari-Solovay system R that is arithmetically complete, but their system R⁻. This result is then applied to obtain the nonvalidity of some rules under arithmetical interpretations including free variables, and to show that some principles concerning Rosser orderings with free variables cannot be decided, even if one restricts onself to "usual" proof predicates.

Solovay's 1976 completeness result for modal provability logic employs the recursion theorem in its proof. It is shown that the uses of the recursion theorem can in this proof replaced by the diagonalization lemma for arithmetic and that, in effect, the proof neatly fits the framework of another, enriched, system of modal logic so that any arithmetical system for which this logic is sound is strong enough to carry out the proof, in particular $\text{I}\Delta _{0}+\text{EXP}$ . The method is adapted (...) to obtain a similar completeness result for the Rosser logic. (shrink)

To the standard propositional modal system of provability logic constants are added to account for the arithmetical fixed points introduced by Bernardi-Montagna in [5]. With that interpretation in mind, a system LR of modal propositional logic is axiomatized, a modal completeness theorem is established for LR and, after that, a uniform arithmetical completeness theorem with respect to PA is obtained for LR.

The modal completeness proofs of Guaspari and Solovay for their systems R and R⁻ are improved and the relationship between R and R⁻ is clarified.

This first chapter contains an introduction to modal logic. In section 1.1 the syntactic side of the matter is discussed, and in section 1.2 the subject is approached from a semantic point of view.