In this paper we study proofs of some general forms of the Second Incompleteness Theorem. These forms conform to the Feferman format, where the proof predicate is fixed and the representation of the set of axioms varies. We extend the Feferman framework in one important point: we allow the interpretation of number theory to vary.

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)

We examine recursive monotonic functions on the Lindenbaum algebra of EA. We prove that no such function sends every consistent φ to a sentence with deductive strength strictly between φ and (φ∧Con(φ)). We generalize this result to iterates of consistency into the effective transfinite. We then prove that for any recursive monotonic function f, if there is an iterate of Con that bounds f everywhere, then f must be somewhere equal to an iterate of Con.

We study effectively inseparable (abbreviated as e.i.) prelattices (i.e., structures of the form$L = \langle \omega, \wedge, \vee,0,1,{ \le _L}\rangle$whereωdenotes the set of natural numbers and the following four conditions hold: (1)$\wedge, \vee$are binary computable operations; (2)${ \le _L}$is a computably enumerable preordering relation, with$0{ \le _L}x{ \le _L}1$for everyx; (3) the equivalence relation${ \equiv _L}$originated by${ \le _L}$is a congruence onLsuch that the corresponding quotient structure is a nontrivial bounded lattice; (4) the${ \equiv _L}$-equivalence classes of 0 and 1 (...) form an effectively inseparable pair of sets). Solving a problem in (Montagna & Sorbi, 1985) we show (Theorem 4.2), that ifLis an e.i. prelattice then${ \le _L}$is universal with respect to all c.e. preordering relations, i.e., for every c.e. preordering relationRthere exists a computable functionfreducingRto${ \le _L}$, i.e.,$xRy$if and only if$f\left( x \right){ \le _L}f\left( y \right)$, for all$x,y$. In fact (Corollary 5.3)${ \le _L}$is locally universal, i.e., for every pair$a{ < _L}b$and every c.e. preordering relationRone can find a reducing functionffromRto${ \le _L}$such that the range offis contained in the interval$\left\{ {x:a{ \le _L}x{ \le _L}b} \right\}$. Also (Theorem 5.7)${ \le _L}$is uniformly dense, i.e., there exists a computable functionfsuch that for every$a,b$if$a{ < _L}b$then$a{ < _L}f\left( {a,b} \right){ < _L}b$, and if$a{ \equiv _L}a\prime$and$b{ \equiv _L}b\prime$then$f\left( {a,b} \right){ \equiv _L}f\left( {a\prime,b\prime } \right)$. Some consequences and applications of these results are discussed: in particular (Corollary 7.2) for$n \ge 1$the c.e. preordering relation on${{\rm{\Sigma }}_n}$sentences yielded by the relation of provable implication of any c.e. consistent extension of Robinson’s systemRorQis locally universal and uniformly dense; and (Corollary 7.3) the c.e. preordering relation yielded by provable implication of any c.e. consistent extension of Heyting Arithmetic is locally universal and uniformly dense. (shrink)

Answering a question raised by Shavrukov and Visser :569–582, 2014), we show that the lattice of \-sentences ) over any computable enumerable consistent extension T of \ is uniformly dense. We also show that for every \ and \ refer to the known hierarchies of arithmetical formulas introduced by Burr for intuitionistic arithmetic) the lattices of \-sentences over any c.e. consistent extension T of the intuitionistic version of Robinson Arithmetic \ are uniformly dense. As an immediate consequence of the proof, (...) all these lattices are also locally universal. (shrink)