We present an analogue of Gödel’s second incompleteness theorem for systems of second-order arithmetic. Whereas Gödel showed that sufficiently strong theories that are $\Pi ^0_1$ -sound and $\Sigma ^0_1$ -definable do not prove their own $\Pi ^0_1$ -soundness, we prove that sufficiently strong theories that are $\Pi ^1_1$ -sound and $\Sigma ^1_1$ -definable do not prove their own $\Pi ^1_1$ -soundness. Our proof does not involve the construction of a self-referential sentence but rather relies on ordinal analysis.

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 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 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 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 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.

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)

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)