In this paper we examine various requirements on the formalisation choices under which self-reference can be adequately formalised in arithmetic. In particular, we study self-referential numberings, which immediately provide a strong notion of self-reference even for expressively weak languages. The results of this paper suggest that the question whether truly self-referential reasoning can be formalised in arithmetic is more sensitive to the underlying coding apparatus than usually believed. As a case study, we show how this sensitivity affects the formal study (...) of certain principles of self-referential truth. (shrink)

There has been a recent interest in hierarchical generalizations of classic incompleteness results. This paper provides evidence that such generalizations are readily obtainable from suitably formulated hierarchical versions of the principles used in the original proofs. By collecting such principles, we prove hierarchical versions of Mostowski’s theorem on independent formulae, Kripke’s theorem on flexible formulae, Woodin’s theorem on the universal algorithm, and a few related results. As a corollary, we obtain the expected result that the formula expressing “$\mathrm {T}$is$\Sigma _n$-ill” (...) is a canonical example of a$\Sigma _{n+1}$formula that is$\Pi _{n+1}$-conservative over$\mathrm {T}$. (shrink)

We study the first-order consequences of Ramsey’s Theorem fork-colourings ofn-tuples, for fixed$n, k \ge 2$, over the relatively weak second-order arithmetic theory$\mathrm {RCA}^*_0$. Using the Chong–Mourad coding lemma, we show that in a model of$\mathrm {RCA}^*_0$that does not satisfy$\Sigma ^0_1$induction,$\mathrm {RT}^n_k$is equivalent to its relativization to any proper$\Sigma ^0_1$-definable cut, so its truth value remains unchanged in all extensions of the model with the same first-order universe.We give a complete axiomatization of the first-order consequences of$\mathrm {RCA}^*_0 + \mathrm {RT}^n_k$for$n \ge (...) 3$. We show that they form a non-finitely axiomatizable subtheory of$\mathrm {PA}$whose$\Pi _3$fragment coincides with$\mathrm {B} \Sigma _1 + \exp $and whose$\Pi _{\ell +3}$fragment for$\ell \ge 1$lies between$\mathrm {I} \Sigma _\ell \Rightarrow \mathrm {B} \Sigma _{\ell +1}$and$\mathrm {B} \Sigma _{\ell +1}$. We also give a complete axiomatization of the first-order consequences of$\mathrm {RCA}^*_0 + \mathrm {RT}^2_k + \neg \mathrm {I} \Sigma _1$. In general, we show that the first-order consequences of$\mathrm {RCA}^*_0 + \mathrm {RT}^2_k$form a subtheory of$\mathrm {I} \Sigma _2$whose$\Pi _3$fragment coincides with$\mathrm {B} \Sigma _1 + \exp $and whose$\Pi _4$fragment is strictly weaker than$\mathrm {B} \Sigma _2$but not contained in$\mathrm {I} \Sigma _1$.Additionally, we consider a principle$\Delta ^0_2$-$\mathrm {RT}^2_2$which is defined like$\mathrm {RT}^2_2$but with both the$2$-colourings and the solutions allowed to be$\Delta ^0_2$-sets rather than just sets. We show that the behaviour of$\Delta ^0_2$-$\mathrm {RT}^2_2$over$\mathrm {RCA}_0 + \mathrm {B}\Sigma ^0_2$is in many ways analogous to that of$\mathrm {RT}^2_2$over$\mathrm {RCA}^*_0$, and that$\mathrm {RCA}_0 + \mathrm {B} \Sigma ^0_2 + \Delta ^0_2$-$\mathrm {RT}^2_2$is$\Pi _4$- but not$\Pi _5$-conservative over$\mathrm {B} \Sigma _2$. However, the statement we use to witness failure of$\Pi _5$-conservativity is not provable in$\mathrm {RCA}_0 +\mathrm {RT}^2_2$. (shrink)

In this paper we will show that for every cutIof any countable nonstandard model$\mathcal {M}$of$\mathrm {I}\Sigma _{1}$, eachI-small$\Sigma _{1}$-elementary submodel of$\mathcal {M}$is of the form of the set of fixed points of some proper initial self-embedding of$\mathcal {M}$iffIis a strong cut of$\mathcal {M}$. Especially, this feature will provide us with some equivalent conditions with the strongness of the standard cut in a given countable model$\mathcal {M}$of$ \mathrm {I}\Sigma _{1} $. In addition, we will find some criteria for extendability of initial (...) self-embeddings of countable nonstandard models of$ \mathrm {I}\Sigma _{1} $to larger models. (shrink)

We systematically study several versions of the disjunction and the existence properties in modal arithmetic. First, we newly introduce three classes $\mathrm {B}$, $\Delta (\mathrm {B})$, and $\Sigma (\mathrm {B})$ of formulas of modal arithmetic and study basic properties of them. Then, we prove several implications between the properties. In particular, among other things, we prove that for any consistent recursively enumerable extension T of $\mathbf {PA}(\mathbf {K})$ with $T \nvdash \Box \bot $, the $\Sigma (\mathrm {B})$ -disjunction property, the (...) $\Sigma (\mathrm {B})$ -existence property, and the $\mathrm {B}$ -existence property are pairwise equivalent. Moreover, we introduce the notion of the $\Sigma (\mathrm {B})$ -soundness of theories and prove that for any consistent recursively enumerable extension of $\mathbf {PA}(\mathbf {K4})$, the modal disjunction property is equivalent to the $\Sigma (\mathrm {B})$ -soundness. (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 current paper studies the formal properties of the Global Reflection Principle, to wit the assertion “All theorems of$\mathrm {Th}$are true,” where$\mathrm {Th}$is a theory in the language of arithmetic and the truth predicate satisfies the usual Tarskian inductive conditions for formulae in the language of arithmetic. We fix the gap in Kotlarski’s proof from [15], showing that the Global Reflection Principle for Peano Arithmetic is provable in the theory of compositional truth with bounded induction only ($\mathrm {CT}_0$). Furthermore, we (...) extend the above result showing that$\Sigma _1$-uniform reflection over a theory of uniform Tarski biconditionals ($\mathrm {UTB}^-$) is provable in$\mathrm {CT}_0$, thus answering the question of Beklemishev and Pakhomov [2]. Finally, we introduce the notion of a prolongable satisfaction class and use it to study the structure of models of$\mathrm {CT}_0$. In particular, we provide a new model-theoretical characterization of theories of finite iterations of uniform reflection and present a new proof characterizing the arithmetical consequences of$\mathrm {CT}_0$. (shrink)

The prevalent interpretation of Gödel’s Second Theorem states that a sufficiently adequate and consistent theory does not prove its consistency. It is however not entirely clear how to justify this informal reading, as the formulation of the underlying mathematical theorem depends on several arbitrary formalisation choices. In this paper I examine the theorem’s dependency regarding Gödel numberings. I introducedeviantnumberings, yielding provability predicates satisfying Löb’s conditions, which result in provable consistency sentences. According to the main result of this paper however, these (...) “counterexamples” do not refute the theorem’s prevalent interpretation, since once a natural class ofadmissiblenumberings is singled out, invariance is maintained. (shrink)

This study examines how the Gödel phenomena are to be treated in core logic. We show in formal detail how one can use core logic in the metalanguage to prove Gödel’s incompleteness theorems for arithmetic even when classical logic is used for logical closure in the object language.

We show that the universally axiomatized, induction-free theory equation image is a sequential theory in the sense of Pudlák's 5, in contrast to the closely related Robinson's arithmetic.

This paper belongs to the research on the limit of the first incompleteness theorem. Effectively inseparable (EI) theories can be viewed as an effective version of essentially undecidable (EU) theories, and EI is stronger than EU. We examine this question: Are there minimal effectively inseparable theories with respect to interpretability? We propose tEI, the theory version of EI. We first prove that there are no minimal tEI theories with respect to interpretability (i.e., for any tEI theory T, we can effectively (...) find a theory which is tEI and strictly weaker than T with respect to interpretability). By a theorem due to Pour-EI, we have that tEI is equivalent with EI. Thus, there are no minimal EI theories with respect to interpretability. Also, we prove that there are no minimal finitely axiomatizable EI theories with respect to interpretability. (shrink)

Kreisel’s conjecture is the statement: if, for all$n\in \mathbb {N}$,$\mathop {\text {PA}} \nolimits \vdash _{k \text { steps}} \varphi (\overline {n})$, then$\mathop {\text {PA}} \nolimits \vdash \forall x.\varphi (x)$. For a theory of arithmeticT, given a recursive functionh,$T \vdash _{\leq h} \varphi $holds if there is a proof of$\varphi $inTwhose code is at most$h(\#\varphi )$. This notion depends on the underlying coding.${P}^h_T(x)$is a predicate for$\vdash _{\leq h}$inT. It is shown that there exist a sentence$\varphi $and a total recursive functionhsuch that$T\vdash (...) _{\leq h}\mathop {\text {Pr}} \nolimits _T(\ulcorner \mathop {\text {Pr}} \nolimits _T(\ulcorner \varphi \urcorner )\rightarrow \varphi \urcorner )$, but, where$\mathop {\text {Pr}} \nolimits _T$stands for the standard provability predicate inT. This statement is related to a conjecture by Montagna. Also variants and weakenings of Kreisel’s conjecture are studied. By the use of reflexion principles, one can obtain a theory$T^h_\Gamma $that extendsTsuch that a version of Kreisel’s conjecture holds: given a recursive functionhand$\varphi (x)$a$\Gamma $-formula (where$\Gamma $is an arbitrarily fixed class of formulas) such that, for all$n\in \mathbb {N}$,$T\vdash _{\leq h} \varphi (\overline {n})$, then$T^h_\Gamma \vdash \forall x.\varphi (x)$. Derivability conditions are studied for a theory to satisfy the following implication: if, then$T\vdash \forall x.\varphi (x)$. This corresponds to an arithmetization of Kreisel’s conjecture. It is shown that, for certain theories, there exists a functionhsuch that$\vdash _{k \text { steps}}\ \subseteq\ \vdash _{\leq h}$. (shrink)

We systematically study conservation theorems on theories of semi-classical arithmetic, which lie in-between classical arithmetic $\mathsf {PA}$ and intuitionistic arithmetic $\mathsf {HA}$. Using a generalized negative translation, we first provide a structured proof of the fact that $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over $\mathsf {HA} + {\Sigma _k}\text {-}\mathrm {LEM}$ where ${\Sigma _k}\text {-}\mathrm {LEM}$ is the axiom scheme of the law-of-excluded-middle restricted to formulas in $\Sigma _k$. In addition, we show that this conservation theorem is optimal in the (...) sense that for any semi-classical arithmetic T, if $\mathsf {PA}$ is $\Pi _{k+2}$ -conservative over T, then ${T}$ proves ${\Sigma _k}\text {-}\mathrm {LEM}$. In the same manner, we also characterize conservation theorems for other well-studied classes of formulas by fragments of classical axioms or rules. This reveals the entire structure of conservation theorems with respect to the arithmetical hierarchy of classical principles. (shrink)

Since in Heyting Arithmetic all atomic formulas are decidable, a Kripke model for HA may be regarded classically as a collection of classical structures for the language of arithmetic, partially ordered by the submodel relation. The obvious question is then: are these classical structures models of Peano Arithmetic ? And dually: if a collection of models of PA, partially ordered by the submodel relation, is regarded as a Kripke model, is it a model of HA? Some partial answers to these (...) questions were obtained in [6], [3], [1] and [2]. Here we present some results in the same direction, announced in [7]. In particular, it is proved that the classical structures at the nodes of a Kripke model of HA must be models of IΔ1 and that the relation between these classical structures must be that of a Δ1-elementary submodel. MSC: 03F30, 03F55. (shrink)

In [20] Krajíček and Pudlák discovered connections between problems in computational complexity and the lengths of first-order proofs of finite consistency statements. Later Pudlák [25] studied more statements that connect provability with computational complexity and conjectured that they are true. All these conjectures are at least as strong as $\mathsf {P}\neq \mathsf {NP}$ [23–25].One of the problems concerning these conjectures is to find out how tightly they are connected with statements about computational complexity classes. Results of this kind had been (...) proved in [20, 22].In this paper, we generalize and strengthen these results. Another question that we address concerns the dependence between these conjectures. We construct two oracles that enable us to answer questions about relativized separations asked in [19, 25] (i.e., for the pairs of conjectures mentioned in the questions, we construct oracles such that one conjecture from the pair is true in the relativized world and the other is false and vice versa). We also show several new connections between the studied conjectures. In particular, we show that the relation between the finite reflection principle and proof systems for existentially quantified Boolean formulas is similar to the one for finite consistency statements and proof systems for non-quantified propositional tautologies. (shrink)

Kristiansen and Murwanashyaka recently proved that Robinson arithmetic, Q, is interpretable in an elementary theory of full binary trees, T. We prove that, conversely, T is interpretable in Q by producing a formal interpretation of T in an elementary concatenation theory QT+, thereby also establishing mutual interpretability of T with several well-known weak essentially undecidable theories of numbers, strings, and sets. We also introduce a “hybrid” elementary theory of strings and trees, WQT*, and establish its mutual interpretability with Robinson’s weak (...) arithmetic R, the weak theory of trees WT of Kristiansen and Murwanashyaka, and the weak concatenation theory WTCε of Higuchi and Horihata. (shrink)

By suitably adapting an argument of Hirschfeld , we show that there is a single Δ1 formula that defeats “bounded collection” for any model of II2 Arithmetic that is either a recursive ultrapower or an existentially complete model. Some related facts are noted. MSC: 03F30, 03C62.

We employ the lens provided by formal truth theory to study axiomatizations of Peano Arithmetic ${\textsf {(PA)}}$. More specifically, let Elementary Arithmetic ${\textsf {(EA)}}$ be the fragment $\mathsf {I}\Delta _0 + \mathsf {Exp}$ of ${\textsf {PA}}$, and let ${\textsf {CT}}^-[{\textsf {EA}}]$ be the extension of ${\textsf {EA}}$ by the commonly studied axioms of compositional truth ${\textsf {CT}}^-$. We investigate both local and global properties of the family of first order theories of the form ${\textsf {CT}}^-[{\textsf {EA}}] +\alpha $, where $\alpha (...) $ is a particular way of expressing “ ${\textsf {PA}}$ is true” (using the truth predicate). Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to ${\textsf {PA}}$ and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of ${\textsf {PA}}$. (shrink)

Vardanyan’s Theorems [36, 37] state that $\mathsf {QPL}(\mathsf {PA})$ —the quantified provability logic of Peano Arithmetic—is $\Pi ^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge [38] generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf (...) {QRC_1}$ was previously introduced by the authors [1] as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf {QRC_1}$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf {QRC_1}$ is the strictly positive fragment of $\mathsf {QGL}$ and a fragment of $\mathsf {QPL}(\mathsf {PA})$. (shrink)

Following the finitist’s rejection of the complete totality of the natural numbers, a finitist language allows only propositional connectives and bounded quantifiers in the formula-construction but not unbounded quantifiers. This is opposed to the currently standard framework, a first-order language. We conduct axiomatic studies on the notion of truth in the framework of finitist arithmetic in which at least smash function $\#$ is available. We propose finitist variants of Tarski ramified truth theories up to rank $\omega $, of Kripke–Feferman truth (...) theory and of Friedman–Sheard truth theory, and show that all of these have the same strength as the finitist arithmetic of one higher level along Grzegorczyk hierarchy. On the other hand, we also show that adding Burgess-style groundedness schema, adjusted to the finitist setting, makes Kripke–Feferman truth theory as strong as primitive recursive arithmetic. Meanwhile, we obtain some basic results on finitist theories of (full and hat) inductive definitions and on the second order axiom of hat inductive definitions for positive operators. (shrink)

We characterize the sets of all Π2 and all equation image theorems of IΠ−1 in terms of restricted exponentiation, and use these characterizations to prove that both sets are not deductively equivalent. We also discuss how these results generalize to n > 0. As an application, we prove that a conservation theorem of Beklemishev stating that IΠ−n + 1 is conservative over IΣ−n with respect to equation image sentences cannot be extended to Πn + 2 sentences. © 2011 WILEY-VCH Verlag (...) GmbH & Co. KGaA, Weinheim. (shrink)

Following our [6], though with somewhat different methods here, further variants of Goodstein sequences are introduced in terms of parameterized Ackermann–Péter functions. Each of the sequences is shown to terminate, and the proof-theoretic strengths of these facts are calibrated by means of ordinal assignments, yielding independence results for a range of theories: PRA, PA,$\Sigma ^1_1$-DC$_0$, ATR$_0$, up to ID$_1$. The key is the so-called “Hardy hierarchy” of proof-theoretic bounding finctions, providing a uniform method for associating Goodstein-type sequences with parameterized normal (...) form representations of positive integers. (shrink)

Logic is traditionally considered to be a purely syntactic discipline, at least in principle. However, prof. David Isles has shown that this ideal is not yet met in traditional logic. Semantic residue is present in the assumption that the domain of a variable should be fixed in advance of a derivation, and also in the notion that a numerical notation must refer to a number rather than be considered a mathematical object in and of itself. Based on his work, the (...) central question of this thesis is what kind of logic, if any, results from removing this semantic residue from traditional logic.We differ from traditional logic in two significant ways. The first is that the assumption that a numerical notation must refer to a number is denied. Numerical notations are considered as mathematical objects in their own right, related to each other by means of rewrite rules. The traditional notion of reference is then replaced by the notion of reduction (by means of the rewrite rules) to a normal form. Two numerical notations that reduce to the same normal form would traditionally be considered identical, as they would refer to the same number, and hence they would be interchangeable salva veritate. In the new system, called Buridan-Volpin (BV), the numerical notations themselves are the elements of the domains of variables, and two numerical notations that reduce to the same normal form need not be interchangeable salva veritate, except when they are syntactically identical (i.e., have the same Gödel number).The second is that we do away with the assumption that the domains of variables need to be fixed in advance of a derivation. Instead we focus on what is needed to guarantee preservation of truth in every step of a derivation. These conditions on the domains of the variables, accumulated in the course of a derivation, are combined in a reference grammar. Whereas traditionally a derivation is considered valid when the conclusion follows from the premisses by way of the derivation rules (and possibly axioms), in the BV system a derivation must meet the extra condition that no inconsistency occurs within the reference grammar. For if the reference grammar were to give rise to inconsistency (i.e., it would be impossible to assign domains to all the variables without breaking at least one of the conditions placed on them in the reference grammar), there is no longer a guarantee that truth has been preserved in every step of the derivation, and hence the truth of the conclusion is not guaranteed by the derivation.In Chapter 2 the BV system is introduced in some formal detail. Chapter 3 gives some examples of derivations, notably totality of addition, multiplication and exponentiation, as well as a lemma needed for the proof of Euclid’s Theorem. These examples, taken from prof. Isles’ First-Order Reasoning and Primitive Recursive Natural Number Notations, show that there is a real proof-theoretical difference between traditional logic and the BV system. Here we also find the first major point of departure between myself and prof. Isles, centered on the notion of inheritance of conditions in the reference grammar by way of lemmata. These different points of view are best illustrated in the sections on the totality of exponentiation and on Euclid’s Lemma: prof. Isles maintains that the proof of totality of exponentiation is not BV valid, while I maintain that it is. But I do agree with him that the traditional proof of Euclid’s Lemma is not BV valid. Chapter 6 also expands the arguments for my choice in this matter.Now that it has been shown that there is a difference between traditional logic and BV, the properties of BV need to be examined. In Chapter 4 we give a proof of Cut-elimination for BV minus induction and the subformula property for BV, which allows us to prove the consistency of BV minus induction. We also expand on the reasons for excluding induction. In Chapter 5 we consider in detail the proof of a finite analog to the Löwenheim–Skolem theorem given by prof. Isles in his article with the same title. He proves that under certain conditions it is always possible, given the existence of a (possibly uncountable) model for a derivation, to give a finite model for this derivation. The system he considers deviates from BV as considered in this thesis in two significant ways: it does not contain the induction rule and the domains contain numbers instead of numerical notations. We then go on to show that it is possible to extend the result to include induction, in the sense that the existence of a possibly uncountable model for a derivation guarantees the existence of a model that is at most countable. We also consider the complications that arise from taking numerical expressions instead of numbers as the elements of domains.Finally, in Chapter 6 we consider the philosophical consequences of the BV system, informed by the formal results from the previous chapters. In particular we discuss the relation between reduction and reference, the status of reference grammars, the notion of induction and its function within BV, and some brief considerations on the consequences of the BV system for the discussion regarding nominalism and realism with regard to mathematical objects. The object of the chapter is twofold. On the one hand applying the formal results to philosophical questions, on the other hand arguing that BV is not just a theoretically acceptable alternative to traditional logic, but is in fact deserving of further development and research into its properties. The latter will probably appeal most to those of a nominalist and/or finitist bent.Abstract prepared by Harrie de Swart and Sven Storms.E-mail:[email protected]:https://research.tilburguniversity.edu/files/6170 1294/Storms_The_Buridan_Volpin_04_05_2022.pdf. (shrink)

We prove a strengthened version of Shavrukov’s result on the non-isomorphism of diagonalizable algebras of two $\Sigma _1$ -sound theories, based on the improvements previously found by Adamsson. We then obtain several corollaries to the strengthened result by applying it to various pairs of theories and obtain new non-isomorphism examples. In particular, we show that there are no surjective homomorphisms from the algebra $(\mathfrak {L}_T, \Box _T\Box _T)$ onto the algebra $(\mathfrak {L}_T, \Box _T)$. The case of bimodal diagonalizable algebras (...) is also considered. We give several examples of pairs of theories with isomorphic diagonalizable algebras but non-isomorphic bimodal diagonalizable algebras. (shrink)

We present a new manifestation of Gödel’s second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert’s program. Specifically, we consider a proper extension of Peano arithmetic ( $\mathbf {PA}$ ) by a mathematically meaningful axiom scheme that consists of $\Sigma ^0_2$ -sentences. These sentences assert that each computably enumerable ( $\Sigma ^0_1$ -definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is (...) relevant for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel’s second incompleteness theorem. In contrast, Gödel’s theorem is not needed for typical examples of $\Pi ^0_2$ -independence (such as the Paris–Harrington principle), since computational strength provides an extensional invariant on the level of $\Pi ^0_2$ -sentences. (shrink)

We consider fragments of uniform reflection for formulas in the analytic hierarchy over theories of second order arithmetic. The main result is that for any second order arithmetic theory $T_0$ extending $\mathsf {RCA}_0$ and axiomatizable by a $\Pi ^1_{k+2}$ sentence, and for any $n\geq k+1$, $$\begin{align*}T_0+ \mathrm{RFN}_{\varPi^1_{n+2}} \ = \ T_0 + \mathrm{TI}_{\varPi^1_n}, \end{align*}$$ $$\begin{align*}T_0+ \mathrm{RFN}_{\varSigma^1_{n+1}} \ = \ T_0+ \mathrm{TI}_{\varPi^1_n}^{-}, \end{align*}$$ where T is $T_0$ augmented with full induction, and $\mathrm {TI}_{\varPi ^1_n}^{-}$ denotes the schema of transfinite induction up (...) to $\varepsilon _0$ for $\varPi ^1_n$ formulas without set parameters. (shrink)