In this paper, we investigate Rosser provability predicates whose provability logics are normal modal logics. First, we prove that there exists a Rosser provability predicate whose provability logic is exactly the normal modal logic \. Secondly, we introduce a new normal modal logic \ which is a proper extension of \, and prove that there exists a Rosser provability predicate whose provability logic includes \.

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.

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.

In this sequel toSelf-reference in arithmetic Iwe continue our discussion of the question: What does it mean for a sentence of arithmetic to ascribe to itself a property? We investigate how the properties of the supposedly self-referential sentences depend on the chosen coding, the formulae expressing the properties and the way a fixed point for the expressing formulae are obtained. In this second part we look at some further examples. In particular, we study sentences apparently expressing their Rosser-provability, their own${\rm{\Sigma (...) }}_n^0$-truth or their own${\rm{\Pi }}_n^0$-truth. Finally we offer an assessment of the results of both papers. (shrink)

In this paper we explain our pretense account of truth-talk and apply it in a diagnosis and treatment of the Liar Paradox. We begin by assuming that some form of deflationism is the correct approach to the topic of truth. We then briefly motivate the idea that all T-deflationists should endorse a fictionalist view of truth-talk, and, after distinguishing pretense-involving fictionalism (PIF) from error- theoretic fictionalism (ETF), explain the merits of the former over the latter. After presenting the basic framework (...) of our PIF account of truth-talk, we demonstrate a few advantages it offers over T-deflationist accounts that do not explicitly acknowledge pretense at work in the discourse. In turning to the Liar Paradox, we explain how the quasi-anaphoric functioning that our account attributes to truth-talk provides a diagnosis of the Liar Paradox (and other instances of semantic pathology) as having no content—in the sense of not specifying any of what we call M-conditions. At the same time, however, we vindicate the intuition that we can understand liar sentences, thereby avoiding one standard objection to “meaningless strategy” responses to the Liar Paradox. With this diagnosis in place, we then, by way of treatment, introduce a new predicate, ‘semantically defective’, and show how the explanation we give for its application allows for a consistent, yet revenge-immune, (dis)solution of the Liar Paradox, and semantic pathology generally. (shrink)

In this paper we study the interpretations of a weak arithmetic, like Buss’s theory $\mathsf{S}^{1}_{2}$, in a given theory $U$. We call these interpretations the arithmetics of $U$. We develop the basics of the structure of the arithmetics of $U$. We study the provability logic of $U$ from the standpoint of the framework of the arithmetics of $U$. Finally, we provide a deeper study of the arithmetics of a finitely axiomatized sequential theory.

Traces the development of recursive functions from their origins in the late nineteenth century to the mid-1930s, with particular emphasis on the work and influence of Kurt Gödel.

In this paper we prove that the preordering $\lesssim $ of provable implication over any recursively enumerable theory $T$ containing a modicum of arithmetic is uniformly dense. This means that we can find a recursive extensional density function $F$ for $\lesssim $. A recursive function $F$ is a density function if it computes, for $A$ and $B$ with $A\lnsim B$, an element $C$ such that $A\lnsim C\lnsim B$. The function is extensional if it preserves $T$-provable equivalence. Secondly, we prove a (...) general result that implies that, for extensions of elementary arithmetic, the ordering $\lesssim $ restricted to $\Sigma_{n}$-sentences is uniformly dense. In the last section we provide historical notes and background material. (shrink)

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)

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.

In this paper individual proofs are integrated into provability logic. Systems of axioms for a logic with operators “A is provable” and “p is a proof of A” are introduced, provided with Kripke semantics and decision procedure. Completeness theorems with respect to the arithmetical interpretation are proved.

An oversight in Guaspari and Solovay’s “Rosser sentences” [D. Guaspari, R.M. Solovay, Rosser sentences, Annals of Mathematical Logic 16 81–99] is pointed out and emended. It concerns the premisses of their proof that there are standard proof predicates all of whose Rosser sentences are provably equivalent. The result holds up, but the premisses mentioned in the paper have to be strengthened somewhat.

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.

A theory T is trustworthy iff, whenever a theory U is interpretable in T, then it is faithfully interpretable. In this paper we give a characterization of trustworthiness. We provide a simple proof of Friedman’s Theorem that finitely axiomatized, sequential, consistent theories are trustworthy. We provide an example of a theory whose schematic predicate logic is complete Π20.

In a recent paper , Urbaniak and Cieśliński describe an analogue of the Yablo Paradox, in the domain of formal provability. Just as the infinite sequence of Yablo sentences inherit the paradoxical behavior of the liar sentence, an infinite sequence of sentences can be constructed that inherit the distinctive behavior of the Gödel sentence. This phenomenon—the transfer of the properties of self-referential sentences of formal mathematics to their “unwindings” into infinite sequences of sentences—suggests a number of interesting logical questions. The (...) purpose of this paper is to give a precise statement of a conjecture from Cieśliński and Urbaniak regarding the unwinding of the Rosser sentence, and to demonstrate that this precise statement is false. We begin with some preliminary motivation, introduce the conjecture against the background of some related results, and finally, in the last section, move on to the proof, which adapts a method used by Solovay and Guaspari. (shrink)

We investigate the theory IΔ 0 + Ω 1 and strengthen [Bu86. Theorem 8.6] to the following: if NP ≠ co-NP. then Σ-completeness for witness comparison formulas is not provable in bounded arithmetic. i.e. $I\delta_0 + \Omega_1 + \nvdash \forall b \forall c (\exists a(\operatorname{Prf}(a.c) \wedge \forall = \leq a \neg \operatorname{Prf} (z.b))\\ \rightarrow \operatorname{Prov} (\ulcorner \exists a(\operatorname{Prf}(a. \bar{c}) \wedge \forall z \leq a \neg \operatorname{Prf}(z.\bar{b})) \urcorner)).$ Next we study a "small reflection principle" in bounded arithmetic. We prove that for (...) all sentences φ $I\Delta_0 + \Omega_1 \vdash \forall x \operatorname{Prov}(\ulcorner \forall y \leq \bar{x} (\operatorname{Prf} (y. \overline{\ulcorner \varphi \urcorner}) \rightarrow \varphi)\urcorner).$ The proof hinges on the use of definable cuts and partial satisfaction predicates akin to those introduced by Pudlak in [Pu86]. Finally, we give some applications of the small reflection principle, showing that the principle can sometimes be invoked in order to circumvent the use of provable Σ-completeness for witness comparison formulas. (shrink)

In this note, a fully modal proof is given of some conservation results proved in a previous paper by arithmetic means. The proof is based on the extendability of Kripke models.

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)

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.

We characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ 0 + EXP, PRA); (PRA, IΣ 1 ); (IΣ m , IΣ n ) for $1 \leq m etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.

In this paper, we examine the limit of applicability of Gödel’s first incompleteness theorem. We first define the notion “$\textsf {G1}$ holds for the theory $T$”. This paper is motivated by the following question: can we find a theory with a minimal degree of interpretation for which $\textsf {G1}$ holds. To approach this question, we first examine the following question: is there a theory T such that Robinson’s $\mathbf {R}$ interprets T but T does not interpret $\mathbf {R}$ and $\textsf (...) {G1}$ holds for T? In this paper, we show that there are many such theories based on Jeřábek’s work using some model theory. We prove that for each recursively inseparable pair $\langle A,B\rangle $, we can construct a r.e. theory $U_{\langle A,B\rangle }$ such that $U_{\langle A,B\rangle }$ is weaker than $\mathbf {R}$ w.r.t. interpretation and $\textsf {G1}$ holds for $U_{\langle A,B\rangle }$. As a corollary, we answer a question from Albert Visser. Moreover, we prove that for any Turing degree $\mathbf {0}< \mathbf {d}<\mathbf {0}^{\prime }$, there is a theory T with Turing degree $\mathbf {d}$ such that $\textsf {G1}$ holds for T and T is weaker than $\mathbf {R}$ w.r.t. Turing reducibility. As a corollary, based on Shoenfield’s work using some recursion theory, we show that there is no theory with a minimal degree of Turing reducibility for which $\textsf {G1}$ holds. (shrink)

We give a survey of current research on Gödel’s incompleteness theorems from the following three aspects: classifications of different proofs of Gödel’s incompleteness theorems, the limit of the applicability of Gödel’s first incompleteness theorem, and the limit of the applicability of Gödel’s second incompleteness theorem.

The proofs of Gödel (1931), Rosser (1936), Kleene (first 1936 and second 1950), Chaitin (1970), and Boolos (1989) for the first incompleteness theorem are compared with each other, especially from the viewpoint of the second incompleteness theorem. It is shown that Gödel’s (first incompleteness theorem) and Kleene’s first theorems are equivalent with the second incompleteness theorem, Rosser’s and Kleene’s second theorems do deliver the second incompleteness theorem, and Boolos’ theorem is derived from the second incompleteness theorem in the standard way. (...) It is also shown that none of Rosser’s, Kleene’s second or Boolos’ theorems is equivalent with the second incompleteness theorem, and Chaitin’s incompleteness theorem neither delivers nor is derived from the second incompleteness theorem. We compare (the strength of) these six proofs with one another. (shrink)

We show that the modal prepositional logicILM (interpretability logic with Montagna's principle), which has been shown sound and complete as the interpretability logic of Peano arithmetic PA (by Berarducci and Savrukov), is sound and complete as the logic ofπ 1-conservativity over eachbE 1-sound axiomatized theory containingI⌆ 1 (PA with induction restricted tobE 1-formulas). Furthermore, we extend this result to a systemILMR obtained fromILM by adding witness comparisons in the style of Guaspari's and Solovay's logicR (this will be done in a (...) separate continuation of the present paper). (shrink)

-/- Provability logic is a modal logic that is used to investigate what arithmetical theories can express in a restricted language about their provability predicates. The logic has been inspired by developments in meta-mathematics such as Gödel’s incompleteness theorems of 1931 and Löb’s theorem of 1953. As a modal logic, provability logic has been studied since the early seventies, and has had important applications in the foundations of mathematics. -/- From a philosophical point of view, provability logic is interesting because (...) the concept of provability in a fixed theory of arithmetic has a unique and non-problematic meaning, other than concepts like necessity and knowledge studied in modal and epistemic logic. Furthermore, provability logic provides tools to study the notion of self-reference. (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.

We investigate the Friedman–Goldfarb–Harrington theorem from two perspectives. Firstly, in the frameworks of classical and modal propositional logics, we study the forms of sentences whose existence is guaranteed by the FGH theorem. Secondly, we prove some variations of the FGH theorem with respect to Rosser provability predicates.

By using a provability predicate of PA, we define ThmPA(M) as the set of theorems of PA in a modelMof PA. We say a modelMof PA is (1) illusory if ThmPA(M) ⊈ ThmPA(ℕ), (2) heterodox if ThmPA(M) ⊈ TA, (3) sane ifM⊨ ConPA, and insane if it is not sane, (4) maximally sane if it is sane and ThmPA(M) ⊆ ThmPA(N) implies ThmPA(M) = ThmPA(N) for every sane modelNof PA. We firstly show thatMis heterodox if and only if it is (...) illusory, and that ThmPA(M) ∩ TA ≠ ThmPA(ℕ) for any illusory modelM. Then we show that there exists a maximally sane model, every maximally sane model satisfies ¬ConPA+ConPA, and there exists a sane model of ¬ConPA+ConPAwhich is not maximally sane. We define that an insane model is (5) illusory by nature if its every initial segment being a nonstandard model of PA is illusory, and (6) going insane suddenly if its every initial segment being a sane model of PA is not illusory. We show that there exists a model of PA which is illusory by nature, and we prove the existence of a model of PA which is going insane suddenly. (shrink)

It is widely considered that Gödel’s and Rosser’s proofs of the incompleteness theorems are related to the Liar Paradox. Yablo’s paradox, a Liar-like paradox without self-reference, can also be used to prove Gödel’s first and second incompleteness theorems. We show that the situation with the formalization of Yablo’s paradox using Rosser’s provability predicate is different from that of Rosser’s proof. Namely, by using the technique of Guaspari and Solovay, we prove that the undecidability of each instance of Rosser-type formalizations of (...) Yablo’s paradox for each consistent but not Σ1-sound theory is dependent on the choice of a standard proof predicate. (shrink)

A modal theory Z using the Guaspari witness comparison signs $\leq, is developed. The theory Z is similar to, but weaker than, the theory R of Guaspari and Solovay. Nevertheless, Z proves the independence of the Rosser fixed-point. A Kripke semantics for Z is presented and some arithmetical interpretations of Z are investigated. Then Z is enriched to ZI by adding a new modality sign for interpretability and by axioms expressing some facts about interpretability of theories. Two arithmetical interpretations of (...) ZI are presented. The proofs of the validity of the axioms of ZI in arithmetical interpretations use some strengthening of Solovay's result about interpretability in Godel-Bernays set theory. (shrink)

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.

It is argued that an instrumentalist notion of proof such as that represented in Hilbert's viewpoint is not obligated to satisfy the conservation condition that is generally regarded as a constraint on Hilbert's Program. A more reasonable soundness condition is then considered and shown not to be counter-exemplified by Godel's First Theorem. Finally, attention is given to the question of what a theory is; whether it should be seen as a "list" or corpus of beliefs, or as a method for (...) selecting beliefs. The significance of this question for assessing "intensional" results like Godel's Second Theorem, and their bearing on Hilbert's Program are discussed. (shrink)

In Honour of John Crossley’s 85th Birthday.

Guaspari (J Symb Logic 48:777–789, 1983) conjectured that a modal formula is it essentially Σ1 (i.e., it is Σ1 under any arithmetical interpretation), if and only if it is provably equivalent to a disjunction of formulas of the form ${\square{B}}$ . This conjecture was proved first by A. Visser. Then, in (de Jongh and Pianigiani, Logic at Work: In Memory of Helena Rasiowa, Springer-Physica Verlag, Heidelberg-New York, pp. 246–255, 1999), the authors characterized essentially Σ1 formulas of languages including witness comparisons (...) using the interpretability logic ILM. In this note we give a similar characterization for formulas with a binary operator interpreted as interpretability in a finitely axiomatizable extension of IΔ 0 + Supexp and we address a similar problem for IΔ 0 + Exp. (shrink)