Let Con↾x denote the finite consistency statement “there are no proofs of contradiction in T with ≤x symbols.” For a large class of natural theories T, Pudlák has shown that the lengths of the shortest proofs of Con↾n in the theory T itself are bounded by a polynomial in n. At the same time he conjectures that T does not have polynomial proofs of the finite consistency statements Con)↾n. In contrast, we show that Peano arithmetic has polynomial proofs of Con)↾n, (...) where Con∗ is the slow consistency statement for Peano arithmetic, introduced by S.-D. Friedman, Rathjen, and Weiermann. We also obtain a new proof of the result that the usual consistency statement Con is equivalent to ε0 iterations of slow consistency. Our argument is proof-theoretic, whereas previous investigations of slow consistency relied on nonstandard models of arithmetic. (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)

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.