A generalization of the second incompleteness theorem and some exceptions to it (Q2500470)

Generalizing a theorem of Pudlák from 1985, Solovay identified a very modest set of assumptions under which a system formalizing arithmetic cannot prove its Hilbert-style proof consistency. The statement that the successor function is total is one of the assumptions. In the introduction, Willard gives a comprehensive account of Solovays's result together with a detailed discussion of the relevant literature concerning provability of arithmetic statements of the form \(\forall p[\varphi(p)\rightarrow \lnot\text{ Prf}_{\alpha,D}(\lceil 0=1\rceil),p)]\), where \(\alpha\) is a formal system, \(D\) is a proof-system for \(\alpha\) and \(\varphi(x)\) is a formula defining a cut in every model of \(\alpha\). The main question of the paper is whether there are exceptions to Solovay's result for theories which do not prove that \(x+1\) exists for every \(x\). It turns out that, for theories with infinitely many constant symbols, the Second Incompleteness Theorem is sensitive to naming conventions for constants. Willard considers three such conventions: Incremental \(C_i=C_{i-1}+1\); Additive \(C_i=C_{i-1}+C_{i-1}\); and Multiplicative \(C_i=C_{i-1}*C_{i-1}\). Since addition is not assumed total, it takes some effort to formalize these conventions using so-called grounding functions. There are seven grounding functions, including, for example, division with rounding. The grounding functions also serve as primitive terms in the definition of the class of bounded formulas \(\Delta^-_0\) and the rest of the arithmetic hierarchy. There are two main theorems. Let \(A\) be an arbitrary consistent system in the language using the grounding functions, such that \(A\) proves all \(\Pi^-_1\) statements true in the standard model, and there exists a \(\Delta^-_0\) predicate encoding the relation ``\(p\) is a Hilbert-style proof of the theorem \(t\) from axiom system \(A\).'' Theorem 3 says that for every such \(A\) there exists a consistent axiom system, called Introspective Semantics with Continuous Expansion of \(A\) (ISCE(\(A\))), whose constant symbols are defined via the additive naming convention, which proves all \(\Pi^-_0\) theorems of \(A\) as well as the statement declaring non-existence of a Hilbert-style proof of 0=1 from its own set of axioms. In contrast, Theorem 4 declares that no consistent axiom system can prove its Hilbert Consistency when it contains all multiplicative naming convention's axioms, proves all \(\Pi^-_0\) theorems of Peano Arithmetic, and satisfies a certain technical constraint called the ``Concise Encoding'' property.