Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant

Gödel’s incompleteness theorems [14, 17] are landmark results in mathematical logic. Both theorems refer to consistent logical theories that satisfy some assumptions, notably that of “containing enough arithmetic.” The first incompleteness theorem (\(\mathcal {IT}_ {1}\)) says that there are sentences that the theory cannot decide, i.e., neither prove nor disprove; the second theorem (\(\mathcal {IT}_{2}\)) says that the theory cannot prove an internal formulation of its own consistency. It is generally accepted that \(\mathcal {IT}_ {1}\) and \(\mathcal {IT}_{2}\) have a wide scope (and wider for \(\mathcal {IT}_ {1}\) than for \(\mathcal {IT}_{2}\)), covering many logics and logical theories. However, when it comes to rigorous presentation, typically these results are proved for particular, albeit paradigmatic cases, such as theories of arithmetic or hereditarily finite (HF) sets, within classical first-order logic (FOL); and even in these cases the constructions and proofs tend to be significantly sketchy and incomplete. Hence, the theorems’ scope remains largely unexplored on a rigorous/formal basis.

The emergence of powerful proof assistants (also known as interactive theorem provers) has been slowly changing the rules of the game and, we argue, the expectation. Using proof assistants, we can reliably keep track of all the constructions and their properties. Proof automation (sometimes achieved through the cooperation between proof assistants and automatic theorem provers [25, 41]), makes complete, entirely rigorous proofs feasible. And indeed, researchers have successfully met the challenge of mechanizing \(\mathcal {IT}_ {1}\) [21, 36, 40, 53] and recently \(\mathcal {IT}_{2}\) [40]. Besides reassurance, these verification tours de force have brought superior technical insight into the theorems. But they have taken place within the same solitary confinement of scope as the informal proofs.

This article takes steps towards a fully formal exploration of the incompleteness theorems and their wide scope, by a detailed analysis of their assumptions. We use Isabelle/HOL [34, 35] to establish general conditions under which the theorems apply to a partially specified logic. Our formalization is publicly available in the Archive of Formal Proofs [44,45,46,47,48], but is not necessary for following this article, which is self-contained and does not employ Isabelle jargon (except for the dedicated Appendix A).

After discussing related work (Sect. 2) and guiding principles (Sect. 3), we describe our formal development. The abstract part of this development starts by setting the stage of a partially specified logical system, some partially specified arithmetic components, and representability (Sect. 4), proving the diagonalization lemmas (Sect. 5), and proving several flavors of the end results in this setting: \(\mathcal {IT}_ {1}\) (Sect. 6) and \(\mathcal {IT}_{2}\) (Sect. 7). Some of the abstract results (summarized in Sect. 8) are instantiated to concrete first-order logic theories (Sect. 9). We also discuss proof-engineering aspects (Appendix A) and include an index of our abstract assumptions (Appendix B).

We start with a notion of logic whose terms and formulas are kept abstract (Sect. 4.1). In particular, substitution and free variables are not defined, but axiomatized by some general properties. Provability is also axiomatized (Sect. 4.2). We distinguish between a basic provability relation, capturing minimal theories that are sufficiently expressive for representing concepts via Gödel encodings (e.g., Peano arithmetic or weaker theories), and a (plain) provability relation, capturing consistent or \(\omega \)-consistent extensions of the minimal theories. Thus, basic provability is subsumed by provability. Yet, provability will be represented internally and reasoned about within basic provability.

On top of this logic substratum, we consider an arithmetic substratum, consisting of a set of closed terms called numerals and an order-like relation (Sect. 4.3). Our framework also incorporates encodings of formulas and proofs into numerals, the representability of various functions and relations as formulas (Sect. 4.4), the Hilbert–Bernays–Löb derivability conditions (Sect. 4.5), and standard models (Sect. 4.6).

Overall, our assumptions capture the notion of “containing enough arithmetics” in a general and flexible way. It is general because only few assumptions are made about the exact nature of formulas and numerals. It is flexible because different versions of the incompleteness theorems consider their own “amount of arithmetics” that makes it “enough,” as proper subsets of these assumptions. Indeed, our formalization of the results (the diagonalization lemma in Sect. 5, \(\mathcal {IT}_ {1}\) in Sect. 6, and \(\mathcal {IT}_{2}\) in Sect. 7) proceeds in an austere-buffet style: Every result picks just enough infrastructure needed for it to hold—ranging from diagonalization which requires very little, to Rosser’s version of \(\mathcal {IT}_ {1}\) which is quite demanding. This approach caters for a sharp comparison between different formulations of the theorems, highlighting their tradeoffs: Gödel’s original formulation of \(\mathcal {IT}_ {1}\) versus Rosser’s improvement (Sect. 6.3), proof-theoretic versus semantic versions of \(\mathcal {IT}_ {1}\) (Sect. 6.4), and Gödel’s original formulation of the \(\mathcal {IT}_{2}\) versus Jeroslow’s improvement (Sect. 7.3).

Abstractness is our development’s main strength, but also a potential weakness: Are our hypotheses reasonable? Are they consistent? These questions particularly concern our axiomatization of free variables and substitution—a notoriously error-prone area. As a (partial) remedy, we instantiate part of our framework to Paulson’s semantics-based \(\mathcal {IT}_ {1}\) and \(\mathcal {IT}_{2}\) for hereditarily finite (HF) set theory [40], also upgrading Paulson’s \(\mathcal {IT}_{2}\) to a more general and standard formulation: for consistent (not necessarily sound) theories (Sect. 9).

This article extends our CADE 2019 conference paper [43] with a significantly more fine-grained and self-contained presentation of the results, which includes lemmas and detailed proof sketches. Given the existence of formal proofs in Isabelle, one may question the usefulness of paper proof sketches; however, we believe these are important for reaching out to a wider audience—perhaps interested in following the reasoning behind our fine-grained results discovered with the help of Isabelle, but not willing to read and understand Isabelle scripts. Compared to the conference paper, the results are also established in a more general setting, where we distinguish between basic provability and provability (as explained above). This generalization had been left as future work in the conference paper.

There is a vast amount of literature on the incompleteness theorems and their extensions and ramifications. We only discuss works that are strongly related to the ideas and techniques we tackle in this article. Gödel initially gave a proof of \(\mathcal {IT}_ {1}\) and the rough proof idea of \(\mathcal {IT}_{2}\) [17]. Hilbert and Bernays gave a first detailed proof of \(\mathcal {IT}_{2}\) [22]. Subsequently, a large amount of work was dedicated to the (re)formulation, proof, and analysis of these results [5, 50, 56, 57]. The now canonical line of reasoning goes through the derivability conditions devised by Hilbert and Bernays [22] and simplified by Löb [32]. These conditions have inspired a new branch of modal logic called provability logic [5, 58]. Jeroslow has proved that, contrary to prior belief, one of these conditions is redundant when proving \(\mathcal {IT}_{2}\) [24].

Smullyan [59], Kreisel [28] and Jeroslow [24] were among the first to study abstract conditions on logics under which the incompleteness theorems apply. Feferman [13] gives an essential incompleteness account of \(\mathcal {IT}_{2}\) applicable to extensions of Peano arithmetic in classical FOL. Buldt [7] surveys the state of the art on \(\mathcal {IT}_ {1}\) up to 2014 with a focus on the theorem’s scope, also sketching the applicability to non-standard logics. Our abstract approach, based on generic syntax, provability and truth predicates, resembles the style of institution-independent model theory [12, 18] and our previous work on abstract completeness [4] and completeness of ordered resolution [51]. On distinguishing between two notions of provability, one stronger than the other, we take inspiration from Smorynski’s account [57]. Dimensions of generality that our formalized work does not (yet) explore include quantifier-free logics [24] and arithmetical hierarchy refinements [27]. Our syntax axiomatization is inspired by algebraic theories of the \(\lambda \)-calculi syntax [15, 16, 42].

In the realm of mechanical proofs, the earliest substantial development was due to Sieg [55], who used a prover based on TEM (Theory of Elementary Meta-Mathematics) to formalize parts of the proofs of both \(\mathcal {IT}_ {1}\) and \(\mathcal {IT}_{2}\). Full mechanical proofs of \(\mathcal {IT}_ {1}\) were subsequently achieved by Shankar [52, 53] in the Boyer–Moore prover, O’Connor in Coq [36], and Harrison in HOL Light [21]. Harrison also proved abstract versions of \(\mathcal {IT}_ {1}\) and \(\mathcal {IT}_{2}\) in a simple LCF-style prover implemented in OCaml [19]. \(\mathcal {IT}_{2}\) has only been fully proved recently—by Paulson in Isabelle/HOL [39, 40] (who also proved \(\mathcal {IT}_ {1}\)). All these mechanizations target theories over a fixed language in classical FOL: variants of the language of arithmetic (Harrison and O’Connor) and variants of the language of set theory (Sieg, Shankar, and Paulson, with Shankar also allowing the convenience of new symbols to be defined from the existing ones). The targeted theories are usually (finite) extensions of given standard FOL theories—so the results state the (finitary) essential incompleteness of these theories. Sieg considers the theory Z\(^*\), Shankar finite extensions of the theory Z2, and Paulson finite extensions of HF set theory. Each of Z\(^*\), Z2 and HF set theory are variations of Zermelo–Frankel set theory without the axiom of infinity, and have the same expressive power as Peano arithmetic [10, 61]. O’Connor targets self-representable extensions of the theory NN [23, §7.1], a modification of Robinson arithmetic obtained by replacing the dichotomy axiom (stating that any element is either 0 or a successor) with three axioms regulating the behavior of an additional binary relation symbol for strict order. Harrison targets Robinson arithmetic, and additionally proves a variant of \(\mathcal {IT}_ {1}\) for an abstract class of theories in the FOL language of Robinson arithmetic. On their way to \(\mathcal {IT}_ {1}\), Shankar and O’Connor prove representability of all partial, respectively primitive recursive functions— important standalone results. We will revisit some of these mechanized concrete results in Sect. 9, with the hindsight of our abstract framework.

Outside the realm of holistic interactive proof development, there have been efforts to fully automate parts of the proofs of Gödel’s and related theorems [8, 49, 54].

Our long-term goal is a framework that makes it easy to instantiate the incompleteness theorems and related results to different logics. This is a daunting task, especially for \(\mathcal {IT}_{2}\), where a lot of seemingly logic-specific technicalities are required to even formulate the theorem. The challenge is to push as much as possible of the technical constructions and lemmas to a largely logic-independent layer.

To this end, we strive to make minimal assumptions with regard to structure and properties when inferring the results—we will call this the Economy principle. For example, we do not define, but axiomatize syntax in terms of a minimalistic infrastructure. We assume a generic single-point substitution, then define simultaneous substitution and infer its properties. This is laborious, but worthwhile: Any logic that provides a single-point substitution satisfying our assumptions gets the simultaneous substitution for free.

As another instance of Economy, when faced with two different ways of formulating a theorem’s conclusion we prefer the one that is stronger under fewer assumptions. (And dually, we prefer weakness for a theorem’s assumptions.) For example, we discuss two variants of consistency: (1) “does not prove false” or (2) “there exists no formula such that itself and its negation are provable” (Sect. 7.3). While the statements are equivalent at the meta-level, their representations as object-logic formulas are not necessarily equivalent; in fact, (1) implies (2) under mild assumptions but not vice versa. So in our abstract theorems we prefer (1). Indeed, even if (2) implies (1) in all reasonable instances, why postpone for the instantiation time any fact that we can show abstractly?

Applying the Economy principle not only stocks up generality for instantiations, but also accurately outlines tradeoffs: How much does it cost (in terms of other added assumptions) to improve the conclusion, or to weaken an assumption of a theorem? For example, an Economy-based proof of Rosser’s variant of \(\mathcal {IT}_ {1}\) reveals how much arithmetic we must factor in for weakening the \(\omega \)-consistency assumption into consistency.

Roughly, the incompleteness theorems are considered to hold for logical theories that (1) contain enough arithmetic and (2) can themselves be arithmetized. Our goal is to give a general formulation of these favorable conditions. To this end, we identify some logic and arithmetic substrata consisting of structure and axioms that express the containment of (various degrees of) arithmetic more abstractly and flexibly than relative interpretations [63]. We also identify abstract notions of encodings and representability that have just what it takes for a working arithmetization.

4.1 The Logical Substratum: Syntax

We start with some unspecified sets of variables (\(\mathsf {{Var}}\), ranged over by x, y, z), numerals (\({{\mathsf {Num}}}\), ranged over by m, n), terms (\({{\mathsf {Term}}}\), ranged over by s, t) and formulas (\({{\mathsf {Fmla}}}\), ranged over by \(\varphi ,\psi ,\chi \)). We assume that variables and numerals are particular terms, i.e., \(\mathsf {{Var}}\subseteq {{\mathsf {Term}}}\) and \({{\mathsf {Num}}}\subseteq {{\mathsf {Term}}}\), and that \(\mathsf {{Var}}\) is infinite. Free-variables and substitution operators, \({{\mathsf {FVars}}}\) and \(\_ [\_/\_]\), are assumed for both terms and formulas. We think of \({{\mathsf {FVars}}}(t)\) as the (finite) set of free variables of the term t, and similarly for formulas. We think of s[t/x] as the term obtained from s by the (capture-avoiding) substitution of t for the free occurrences of variable x; and similarly for \(\varphi [t/x]\), where \(\varphi \) is a formula.

In FOL, terms introduce no bindings, so any occurring variable is free. FOL terms fall under our framework, and so do terms with bindings as in \(\lambda \)-calculi and higher-order logic (HOL). To achieve this degree of inclusiveness while also being able to prove interesting results, we work under some well-behavedness assumptions about \({{\mathsf {FVars}}}\) and \(\_ [\_/\_]\):

1. (1)

   Free-variables and substitution act on variable terms as expected:

   • \({{\mathsf {FVars}}}(x) = \{x\}\);

   • \(x [s/x] = s\), and \(y [s/x] = y\) if \(x \not = y\).

2. (2)

   Substitution on terms is vacuous outside the free variables: \(x \notin {{\mathsf {FVars}}}(t)\) implies \(t [s/x] = t\); and similarly for substitution on formulas.

In addition, for the operators on formulas we assume the following:

1. (3)

   Free-variables distribute over substitution: \({{\mathsf {FVars}}}(\varphi [s/x]) = {{\mathsf {FVars}}}(\varphi ) - \{x\} \cup {{\mathsf {FVars}}}(s)\) if \(x \in {{\mathsf {FVars}}}(\varphi )\).

2. (4)

   Substitution of a variable for itself is vacuous: \(\varphi [x/x] = \varphi \).

3. (5)

   Substitution is compositional (under some freshness assumptions):

   • \(\varphi [s_1/x] [s_2/x] = \varphi [(s_1 [s_2/x]) / x]\);

   • \(\varphi [s_1/x_1] [s_2/x_2] = \varphi [(s_1[s_2/x_2]) / x_1]\) if \(x_2 \notin {{\mathsf {FVars}}}(\varphi )\);

   • \(\varphi [s_1/x_1] [s_2/x_2] = \varphi [s_2/x_2] [(s_1[s_2/x_2]) / x_1]\) if \(x_1 \not = x_2\) and \(x_1 \notin {{\mathsf {FVars}}}(s_2)\).

Of the above assumptions, (1) only applies to, and only makes sense for, substitution on terms. By contrast, we assume (2) for both terms and formulas. The last group, (3)–(5) would makes sense for terms too, but is only assumed for formulas; this is in line with our Economy principle, since our results will not need these assumptions for terms. In these assumptions, just like in the rest of this paper, “\(=\)” denotes the usual equality of two mathematical entities (formally represented by the Isabelle/HOL equality), and not some more abstract equality. This means that our assumptions do not hold for “raw” formulas, but for formulas quotiented to alpha-equivalence, i.e., equivalence classes modulo alpha (of the kind provided, e.g., by using de Bruijn indices or the Nominal Isabelle package [64]); likewise, if the terms have bindings, they would need to be quotiented to alpha-equivalence to satisfy our assumptions.

The incompleteness theorems rely heavily on simultaneous substitution, whose properties are tricky to formalize—for example, Paulson’s formalization article dedicates them ample space [40, 6.2]. To address this problem once and for all generically, we define simultaneous substitution, written \(\varphi [t_1/x_1,\ldots ,t_n/x_n]\), from the single-point substitution, \(\varphi [t/x]\). Accordingly, we derive the properties of simultaneous substitution from the single-point substitution axioms. For example, we prove that \({{\mathsf {FVars}}}(\varphi [s_1/x_1,\ldots ,s_n/x_n]) = {{\mathsf {FVars}}}(\varphi ) \mathrel \cup \bigcup \{ {{\mathsf {FVars}}}(s_i) - \{x_i\} \mid i \in \{1,\ldots ,n\} \text { and } x_i \in {{\mathsf {FVars}}}(\varphi ) \}\). The technicalities are delicate: To avoid undesired variable replacements, \(\varphi [s_1/x_1,\ldots ,s_n/x_n]\) must be defined as \(\varphi [y_1/x_1]\ldots [y_n/x_n][s_1/y_1]\ldots [s_n/y_n]\) for some fresh \(y_1,\ldots ,y_n\), the choice of which we must show to be immaterial. This definition’s complexity is reflected in the proofs of its properties. But again, this one-time effort benefits any “customer” logic: In exchange for a well-behaved single-point substitution, it gets back a well-behaved simultaneous substitution.

We call a term with no free variables closed and a formula with no free variables a sentence. \({{\mathsf {Sen}}}\) denotes the set of sentences. We let \(v_1,v_2,\ldots \) be fixed mutually distinct variables. \({{\mathsf {Fmla}}}_k\) denotes the set of formulas whose set of free variables is exactly \(\{v_1,\ldots ,v_k\}\). In particular, \({{\mathsf {Fmla}}}_0 = {{\mathsf {Sen}}}\). Given \(\varphi \in {{\mathsf {Fmla}}}_k\), we write \(\varphi (t_1,\ldots ,t_n)\) instead of \(\varphi [t_1/v_1,\ldots ,t_n/v_n]\).

In addition to free variables and substitution, our theorems will require formulas to be equipped with some of the following: term equality (\(\equiv \)), Boolean connectives (\(\bot \), \(\top \), \(\rightarrow \), \(\lnot \), \(\wedge \), \(\vee \)), universal and existential quantifiers (\(\forall \), \(\exists \)). When we need negation, we define it taking \(\lnot \,\varphi \) to be \(\varphi \rightarrow \bot \). On the other hand, even in the presence of negation, we do not assume that \(\vee \) and \(\exists \) are definable from \(\wedge \) and \(\forall \) or vice versa. This is because, in line with the Economy principle, we will not assume classical logic except in results that need it. For the rest, we will only assume intuitionistic logic, where these operators are not inter-definable.

The above are not assumed to be constructors (syntax builders), but unspecified operators on terms and formulas, e.g., \(\equiv \; : {{\mathsf {Term}}}\rightarrow {{\mathsf {Term}}}\rightarrow {{\mathsf {Fmla}}}\), \(\bot \in {{\mathsf {Fmla}}}\), \(\forall : \mathsf {{Var}}\times {{\mathsf {Fmla}}}\rightarrow {{\mathsf {Fmla}}}\). This caters for logics that do not have them as primitives. For example, HOL defines all connectives and quantifiers from \(\lambda \)-abstraction and either equality or implication.

Free variables and substitution are assumed to be well-behaved w.r.t. these operators, e.g., \({{\mathsf {FVars}}}(\forall x.\, \varphi ) = {{\mathsf {FVars}}}(\varphi ) - \{x\}\). Finally, numerals are assumed to be closed terms. Thanks to our substitution axioms, this implies that substitution on numerals is vacuous.

4.2 Logical Substratum: Provability

We fix two unary relations on formulas, \(\vdash \; \subseteq {{\mathsf {Fmla}}}\) and \(\vdash ^{\textsf {b}}\; \subseteq {{\mathsf {Fmla}}}\), called provability and basic provability, respectively. We write \(\vdash \varphi \) instead of \(\varphi \in \; \vdash \), and say the formula \(\varphi \) is provable; similarly, we write \(\vdash ^{\textsf {b}}\varphi \) instead of \(\varphi \in \; \vdash ^{\textsf {b}}\), and say the formula \(\varphi \) is basic-provable. Henceforth, we will assume that on sentences basic provability is included in provability: For all \(\varphi \in {{\mathsf {Sen}}}\), \(\vdash ^{\textsf {b}}\varphi \) implies \(\vdash \varphi \).

Typical instances of these relations will be as follows:

• for \(\vdash ^{\textsf {b}}\), provability in some minimal theory, e.g., Robinson arithmetic or HF set theory

• for \(\vdash \), provability in some recursive extension of such a minimal theory

As we will see, \(\vdash ^{\textsf {b}}\) will be assumed to be sufficiently expressive to reason about \(\vdash \), and sometimes also sound w.r.t. the standard model. Whenever certain formula connectives or quantifiers are needed in our results, we will assume that \(\vdash ^{\textsf {b}}\) and \(\vdash \) are closed under the usual (Hilbert-style) intuitionistic FOL axioms and rules with respect to these connectives and quantifiers. Stronger systems, such as those of classical logic, also satisfy these assumptions.

Consistency of \(\vdash \), denoted Con \(_{\vdash }\), is defined as the impossibility to prove false, namely \(\not \vdash \bot \). Another central concept is \(\omega \)-consistency—we carefully choose a formulation that works intuitionistically, with conclusion reminiscent of Gödel’s negative translation [11]:

• OCon \(_{\vdash }\): For all \(\varphi \in {{\mathsf {Fmla}}}_1\), if \(\vdash \lnot \,\varphi (n)\) for all \(n\in {{\mathsf {Num}}}\) then .

Assuming classical deduction in \(\vdash \), this is equivalent to the standard formulation: For all \(\varphi \in {{\mathsf {Fmla}}}_1\), it is not the case that \(\vdash \varphi (n)\) for all \(n\in {{\mathsf {Num}}}\) and \(\vdash \lnot \,(\ \forall x.\,\varphi (x))\).

Occasionally, we will consider not only provability but also explicit proofs. We fix a set \({{\mathsf {Proof}}}\) of (entities we call) proofs, ranged over by p, q, and a binary relation between proofs p and sentences \(\varphi \), written \(p \mathrel {\Vdash }\varphi \) and read “p is a proof of \(\varphi \).” We assume \(\vdash \) and \(\mathrel {\Vdash }\) to be related as expected, in that provability is the same as the existence of a proof:

• Rel \(_{\vdash } ^{\Vdash }\): For all \(\varphi \in {{\mathsf {Sen}}}\), \(\vdash \varphi \) iff there exists \(p\in {{\mathsf {Proof}}}\) such that \(p \mathrel {\Vdash }\varphi \).

Convention 1

In all shown results we will implicitly assume: (1) the generic syntax (free variable and substitution) axioms, (2) at least \(\rightarrow \) and \(\bot \) plus whatever connectives and quantifiers appear in the statement, (3) the inclusion of \(\vdash ^{\textsf {b}}\) into \(\vdash \) and (4) the closedness of \(\vdash ^{\textsf {b}}\) and \(\vdash \) under intuitionistic deduction rules for the assumed connectives and quantifiers. Other assumptions (e.g., order-like relation axioms, classical logic deduction, standard models, etc.) will be indicated explicitly. The appendix contains an index with the explicit assumptions.

In our proof sketches, arguing “by logic” will mean invoking closedness of \(\vdash ^{\textsf {b}}\) or \(\vdash \) under intuitionistic deduction rules; “by classical logic” will explicitly indicate a step that assumes closedness under classical deduction rules.

We will label local facts in proofs for later reference by parenthesized Arabic or Roman numbers, such as (1), (2), (i), (ii). The first occurrence of a parenthesized number will label a fact by preceding it, as in “we obtain (ii) \(\vdash \varphi \wedge \psi \)”, while later occurrences will mean we refer to it, as in “from (ii) we obtain \(\ldots \)”.

4.3 Arithmetic Substratum

On one occasion, we will assume an order-like binary relation modeled by a formula \(\prec \; \in {{\mathsf {Fmla}}}_2\). We write \(t_1 \prec t_2\) instead of \(\prec (t_1,t_2)\) and \(\forall x \prec n \,.\, \varphi \) instead of \(\forall x \,.\, x \prec n \rightarrow \varphi \). It turns out that at our level of abstraction it does not matter whether \(\prec \) is a strict or a non-strict order. Indeed, we only require the following two properties, where \(x \in M\) denotes \(\bigvee _{m \in M} x \equiv m\) and \(\bigvee \) expresses the disjunction of a finite set of formulas:

• Ord \(_{1}\): For all \(\varphi \in {{\mathsf {Fmla}}}_1\) and \(n\in {{\mathsf {Num}}}\), if  \(\vdash ^{\textsf {b}}\varphi (m)\) for all \(m \in {{\mathsf {Num}}}\), then  \(\vdash \forall x \prec n .~\varphi (x)\).

• Ord \(_{2}\): For all \(n\in {{\mathsf {Num}}}\), there exists a finite set \(M \subseteq {{\mathsf {Num}}}\) such that \(\vdash \forall x\, .\, x \in M \vee n \prec x\).

Ord \(_{1}\) states that if a property \(\varphi \) is basic-provable for all numerals, then its universal quantification bounded by any given numeral n is provable. Having in mind the arithmetic interpretation of numerals, it would also make sense to assume a stronger version of Ord \(_{1}\), replacing “if \(\vdash ^{\textsf {b}}\varphi (m)\) for all \(m \in {{\mathsf {Num}}}\)” by the weaker hypothesis “if \(\vdash ^{\textsf {b}}\varphi (m)\) for all \(m \in {{\mathsf {Num}}}\) such that \(\vdash m \prec n\)”. But this stronger version will not be needed. Also, note that we formulate Ord \(_{1}\) in the weakest possible way w.r.t. the choice of provability relations: with a hypothesis about \(\vdash ^{\textsf {b}}\) and a conclusion about \(\vdash \). Ord \(_{2}\) states that, for any numeral n, any element x in the domain of discourse is provably either greater than n or equal to one of a finite set M of numerals.

If we instantiate our syntax to that of first-order arithmetic and take \(\vdash ^{\textsf {b}}\) to be intuitionistic Robinson arithmetic (and \(\vdash \) any larger relation), then both Ord \(_{1}\) and Ord \(_{2}\) hold when taking \(\prec \) as either < or \(\le \). In the presence of a numeral-restricted form of anti-symmetry of the relation (which would include < but exclude \(\le \)), the second condition is stronger:

Lemma 2

Assume \(\vdash \forall x.\,x \prec n \rightarrow \lnot \, n \prec x\). Then Ord \(_{2}\) implies Ord \(_{1}\).

Proof

Let \(\varphi \in {{\mathsf {Fmla}}}_1\) and \(n\in {{\mathsf {Num}}}\). Assume \({\vdash ^{\textsf {b}}}\,\varphi (m)\), in particular, \({\vdash } \varphi (m)\), for all \(m \in {{\mathsf {Num}}}\) and let M be as in Ord \(_{2}\). We must prove \(\vdash \forall x \prec n \,.\, \varphi (x)\). Working inside the formal proof system \(\vdash \), we fix x such that \(x \prec n\). Thanks to the antisymmetry assumption, we obtain \(\lnot \, n \prec x\), which implies by Ord \(_{2}\) that x equals some \(m \in M\); this means that \(\varphi (x)\) holds, as desired.\(\square \)

4.4 Encodings and Representability

Central in the incompleteness theorems are functions that encode formulas and proofs as numerals, \(\langle \_\rangle : {{\mathsf {Fmla}}}\rightarrow {{\mathsf {Num}}}\) and \(\langle \_\rangle : {{\mathsf {Proof}}}\rightarrow {{\mathsf {Num}}}\). For our abstract results, the encodings are not required to be injective or surjective. Various concepts will be assumed to be representable (via these encodings) inside our object logic, via the basic provability relation \(\vdash ^{\textsf {b}}\). We will consistently employ \(\vdash ^{\textsf {b}}\), and not \(\vdash \), to represent concepts. On the other hand, \(\vdash \) and its associated proof-of relation \(\mathrel {\Vdash }\) will be among the concepts we will want to represent.

Let \(A_1,\ldots ,A_m\) be sets, and let, for each of them, \(\langle \_\rangle : A_i \rightarrow {{\mathsf {Num}}}\) be an “encoding” function to numerals. Then, an m-ary relation \(R \subseteq A_1 \times \ldots \times A_m\) is said to be represented by a formula if the following hold for all \((a_1,\ldots ,a_m) \in A_1 \times \ldots \times A_m\):

• \((a_1,\ldots ,a_m) \in R\) implies

• \((a_1,\ldots ,a_m) \notin R\) implies

R is said to be weakly represented by if, for all \((a_1,\ldots ,a_m) \in A_1 \times \ldots \times A_m\), it holds that \((a_1,\ldots ,a_m) \in R\) if and only if . Occasionally, we will use the alternative formulation “ (weakly) represents R.”

Let A be another set with \(\langle \_\rangle : A \rightarrow {{\mathsf {Num}}}\). An m-ary function \(f : A_1 \times \ldots A_{m} \rightarrow A\) is said to be represented by a formula if for all \((a_1,\ldots ,a_{m}) \in A_1 \times \ldots \times A_{m}\):

A function f as above is term-represented by an operator if for all \((a_1,\ldots ,a_{m}) \in A_1 \times \ldots \times A_{m}\).

When the formula by which a relation/function P is represented or term-represented is irrelevant, we call P representable or term-representable.

The terms “representability” and “weak representability” are fairly standard [50]. We refer to Raatikainen [50, §2.2] and Smith [56, §5.6] for an account of different terminologies used in the literature for (variations of) these concepts. In contrast, “term-representability” is a notion that we have introduced ourselves (and so is “cleanness”, defined below).

It is immediate that, assuming \(\vdash ^{\textsf {b}}\) consistent, if a relation R is weakly represented by a formula then it is also represented by that formula. Moreover, if we assume deductive injectivity of the encoding, i.e., \(\vdash ^{\textsf {b}}\langle a_1\rangle \equiv \langle a_2\rangle \) implies \(a_1 = a_2\) for all \(a_1,a_2 \in A\), then the following holds: If a function f is represented by a formula, then its graph \({{\mathsf {Gr}}}(f)\) is represented (as a relation) by the same formula, in particular, representability of f implies representability of \({{\mathsf {Gr}}}(f)\). The converse, i.e., representability of \({{\mathsf {Gr}}}(f)\) implying representability of f (this time by a modified formula), also holds under some assumptions—essentially saying that there is an order-like relation on A that is represented by a formula \(\prec \) as in Sect. 4.3. We do not elaborate on these aspects since they are not used in our end results. Smith works them out in detail in his monograph [56, §16]; he does it for the particular case of Robinson arithmetic, but in such a way that the more general assumptions under which the results hold can be depicted from his proofs. (Smith uses the following terminology: A relation or a function being “captured” means it is represented, and a function being “weakly captured” means its graph is represented as a relation.)

We will also need an enhancement of relation representability: Given \(i < m\), we call the representation of an m-ary relation R by i-clean if for all numbers \(n_1,\ldots ,n_m\) such that \(n_i\) (the i’th number among them) is outside the image of \(\langle \_\rangle \) (i.e., there is no \(a\in A_i\) with \(n_i = \langle a\rangle \)). Cleanness would be trivially satisfied if the encodings were surjective. However, surjectivity is not a reasonable assumption. For example, most of the numeric encodings used in the literature are injective but not surjective.

The key property of cleanness is that it makes a representation behave well with respect to universal quantification of negative statements. We illustrate this for the binary case:

Lemma 3

Assume \(R\subseteq A \times B\) is represented by , and this representation is 1-clean. Then the following are equivalent:

1. (1)

   \((a,b) \not \in R\) for all \(a\in A\)

2. (2)

   for all \(n \in {{\mathsf {Num}}}\)

Proof

By representability, (1) is equivalent to for all \(a \in A\). This, in turn, is equivalent to (2) by 1-cleanness, which lets us exclude numerals outside \(\langle \_\rangle \)’s image. \(\square \)

We let \({{\mathsf {S}}}: {{\mathsf {Fmla}}}_1 \rightarrow {{\mathsf {Sen}}}\) be the self-substitution function, which sends any \(\varphi \in {{\mathsf {Fmla}}}_1\) to \(\varphi (\langle \varphi \rangle )\), i.e., to the sentence obtained from \(\varphi \) by substituting the encoding of \(\varphi \) for the unique variable of \(\varphi \). An alternative to the above “hard” version of \({{\mathsf {S}}}\) is the following “soft” version, which sends any \(\varphi \in {{\mathsf {Fmla}}}_1\) to \(\exists v_1.\;v_1 \,{\equiv }\, \langle \varphi \rangle \,{\wedge }\, \varphi \), where \(v_1\) is the single free variable of \(\varphi \). The soft version yields provably equivalent formulas and has the advantage that it is easier to represent inside the logic, since it does not require formalizing the complexities of capture-avoiding substitution. All our results involving \({{\mathsf {S}}}\) have been proved for both versions.

We will consider the properties Repr \(_\lnot \) , Repr \(_{{\mathsf {S}}}\), and Repr \(_{\Vdash }\) , stating the representability of the functions \(\lnot \) and \({{\mathsf {S}}}\), and of the relation \(\mathrel {\Vdash }\). In addition, Clean \(_{\Vdash }\) will state that the considered representation of \(\mathrel {\Vdash }\) is 1-clean, i.e., it is clean on the proof component. For the representing formulas of the above relations and functions we will use their circled names, , , etc.; for example, Repr \(_{\Vdash }\) means that (1) \(p \mathrel {\Vdash }\varphi \) implies and (2) \(p \mathrel {\not \Vdash }\varphi \) implies for all \(p\in {{\mathsf {Proof}}}\) and \(\varphi \in {{\mathsf {Sen}}}\).

4.5 Derivability Conditions

For several relations R, we will assume representability by formulas . However, the case of the provability relation \(\vdash \) is special. It will have an associated formula , but we will assume for it conditions weaker than representability, and also additional conditions. The following are known as the Hilbert–Bernays–Löb derivability conditions [22, 32]:

• HBL \(_{1}\): \(\vdash \varphi \) implies for all \(\varphi \in {{\mathsf {Sen}}}\).

• HBL \(_{2}\): for all \(\varphi ,\psi \in {{\mathsf {Sen}}}\).

• HBL \(_{3}\): for all \(\varphi \in {{\mathsf {Sen}}}\).

Above and elsewhere, we omit parentheses when instantiating one-variable formulas with encodings of formulas to lighten notation—e.g., writing instead of .

HBL \(_{1}\) states that, if a sentence is provable, then its encoding is basic-provable inside the representation. We would obtain a weaker version of HBL \(_{1}\) if we replaced \(\vdash ^{\textsf {b}}\) with \(\vdash \) in the conclusion, namely asking that \(\vdash \varphi \) implies . HBL \(_{3}\) is, roughly speaking, a formulation of this weaker version of HBL \(_{1}\) “one level up,” inside the proof system \(\vdash ^{\textsf {b}}\). Finally, note that the provability relation is closed under modus ponens, in that \(\vdash \varphi \) and \(\vdash \varphi \rightarrow \psi \) implies \(\vdash \psi \) for all \(\varphi ,\psi \in {{\mathsf {Sen}}}\). Thus, HBL \(_{2}\) roughly states the same property inside the proof system. In short, the derivability conditions state that the representation of provability acts partly similarly to the provability relation. (The above internalizations are “rough” in that they use meta-level quantification instead of object-level quantification—we will come back to this in Sect. 7.2, in the context of \(\mathcal {IT}_{2}\) where these conditions are being used.)

We will also be interested in the converse of HBL \(_{1}\):

• HBL \(^{\Leftarrow }_{1}\): implies \(\vdash \varphi \) for all \(\varphi \in {{\mathsf {Sen}}}\).

The weak representability of \(\vdash \) (as defined in Sect. 4.4) is the conjunction of HBL \(_{1}\) and HBL \(^{\Leftarrow }_{1}\). Moreover, \(\mathrel {\Vdash }\)’s representability implies HBL \(_{1}\) for defined to be :

Lemma 4

Rel \(_{\vdash } ^{\Vdash }\) and Repr \(_{\Vdash }\) imply HBL \(_{1}\).

Proof

Assume \(\vdash \varphi \). Then there exists \(p \in {{\mathsf {Proof}}}\) such that \(p \mathrel {\Vdash }\varphi \). By Repr \(_{\Vdash }\) , we have , hence , as desired. (Note that we did not need the whole Repr \(_{\Vdash }\) ; one implication in the representability condition of \(\mathrel {\Vdash }\) would have sufficed.) \(\square \)

Convention 5

Whenever we assume explicit proofs and representability of proof-of, the formula will be defined from as shown above.

4.6 Standard Models

We fix a unary relation \(\models \; \subseteq {{\mathsf {Sen}}}\), representing truth of a sentence in the standard model. We write \(\models \varphi \) instead of \(\varphi \in \;\models \), and read it as “\(\varphi \) is true.” We consider the assumptions:

• LCQ \(_{\models }\): Logical connectives and quantifiers handle truth as expected:

  1. (1)

     \(\not \models \bot \);

  2. (2)

     for all \(\varphi ,\psi \in {{\mathsf {Sen}}}\), \(\models \varphi \) and \(\models \varphi \rightarrow \psi \) imply \(\models \psi \);

  3. (3)

     for all \(\varphi \in {{\mathsf {Fmla}}}_1\), if \(\models \varphi (n)\) for all \(n\in {{\mathsf {Num}}}\) then \(\models \forall x\!\,\cdot \, \varphi (x)\);

  4. (4)

     for all \(\varphi \in {{\mathsf {Fmla}}}_1\), if \(\models \exists x\,.\,\varphi (x)\) then \(\models \varphi (n)\) for some \(n\in {{\mathsf {Num}}}\);

  5. (5)

     for all \(\varphi \in {{\mathsf {Sen}}}\), \(\models \varphi \) or \(\models \lnot \, \varphi \).

• Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) (basic provability is sound w.r.t. truth): \(\vdash ^{\textsf {b}}\varphi \) implies \(\models \varphi \) for all \(\varphi \in {{\mathsf {Sen}}}\).

• TIP \(_{\models }^{{\vdash }}\) (truth implies provability): implies \(\vdash \varphi \) for all \(\varphi \in {{\mathsf {Sen}}}\).

Note that Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) refers to \(\vdash ^{\textsf {b}}\), not \(\vdash \). Not having to assume that \(\vdash \) is sound will allow us to capture, for example, consistent or \(\omega \)-consistent extensions of Robinson arithmetic that are not sound in the standard natural numbers model.

LCQ \(_{\models }\)(1–4) form a partial description of the connectives’ and quantifiers’ behavior w.r.t. truth: corresponding to elimination rules for \(\bot \), \(\rightarrow \) and \(\exists \) and introduction rule for \(\forall \). This partial description suffices for our results. Note that LCQ \(_{\models }\)(4) is a strong form of existential elimination, saying that (the interpretations of) numerals are a complete set of witnesses for existential formulas valid in the standard model; in particular, this holds for the case when the standard model is built of numerals only. LCQ \(_{\models }\)(5) states that the standard model decides every sentence. TIP \(_{\models }^{{\vdash }}\) is a form of completeness: It states that \(\vdash \) can prove whatever the standard model “agrees” that can be proved by \(\vdash \).

The above axiomatization of standard models will be used to obtain semantic versions of \(\mathcal {IT}_ {1}\). At the heart of these results there will be the connection between the representability of \(\mathrel {\Vdash }\) and HBL \(^{\Leftarrow }_{1}\) in the presence of standard models. Recall that, by Convention 5, whenever we assume \(\mathrel {\Vdash }\) representable, we also assume that \(\vdash \)’s representation is naturally defined from \(\mathrel {\Vdash }\)’s representation (matching the definition of \(\vdash \) from \(\mathrel {\Vdash }\)). This is crucial for \(\mathcal {IT}_{2}\), where the internal definitions must faithfully capture the external ones [1], but not for \(\mathcal {IT}_ {1}\), where we only care about producing, no matter how, an undecided (and true) sentence. In fact, for recursively enumerable extensions of the Robinson arithmetic and related FOL theories, it is possible to produce an artificial provability formula that enjoys better properties than the above natural choice: While the latter satisfies HBL \(_{1}\) but not necessarily HBL \(^{\Leftarrow }_{1}\), the former is guaranteed to satisfy both HBL \(_{1}\) and HBL \(^{\Leftarrow }_{1}\) (i.e., to weakly represent provability). This is why, for example, in his abstract account, Buldt takes the liberty to assume not only HBL \(_{1}\) but also HBL \(^{\Leftarrow }_{1}\) in his most general formulation of \(\mathcal {IT}_ {1}\) [7, Theorem 3.1]. We will not attempt to model such “artificial” versions of in our framework, but will focus on the “natural” one, which works for both \(\mathcal {IT}_ {1}\) and \(\mathcal {IT}_{2}\).

On his way to formalizing \(\mathcal {IT}_{2}\) for extensions of HF set theory (and thus having in mind the “natural” ), after proving HBL \(_{1}\) Paulson notes [40, p. 21]: “The reverse implication [namely HBL \(^{\Leftarrow }_{1}\)], despite its usefulness, is not always proved.” However, for the “natural” , HBL \(^{\Leftarrow }_{1}\) does not come cheaply: It seems to require the soundness of \(\vdash ^{\textsf {b}}\) w.r.t. truth in the standard model (which Paulson assumes), or at least the \(\omega \)-consistency of \(\vdash \). We can depict the situation abstractly, without knowing what standard models look like:

Lemma 6

1. (1)

   Assume Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\), Clean \(_{\Vdash }\) and OCon \(_{\vdash }\). Then HBL \(^{\Leftarrow }_{1}\) holds.

2. (2)

   Assume Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and TIP \(_{\models }^{{\vdash }}\). Then HBL \(^{\Leftarrow }_{1}\) holds.

3. (3)

   Assume Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\), Clean \(_{\Vdash }\), Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and LCQ \(_{\models }\)(1,2,4). Then TIP \(_{\models }^{{\vdash }}\) holds. (In particular, HBL \(^{\Leftarrow }_{1}\) holds.)

Proof

1. (1):

   Assume \(\vdash \langle \varphi \rangle \).

• Hence . (Recall Convention 5.)

• By logic, we obtain .

• With OCon \(_{\vdash }\), we obtain \(n\in {{\mathsf {Num}}}\) such that , in particular .

• With Clean \(_{\Vdash }\) , we obtain \(p \in {{\mathsf {Proof}}}\) such that \(n = \langle p\rangle \). Hence .

• Since, by Repr \(_{\Vdash }\) , we have that \(p \mathrel {\not \Vdash }\varphi \) implies , we obtain \(p \mathrel {\Vdash }\varphi \).

• With Rel \(_{\vdash } ^{\Vdash }\) , we obtain \(\vdash \varphi \), as desired.

1. (2):

   To prove HBL \(^{\Leftarrow }_{1}\), let \(\varphi \in {{\mathsf {Sen}}}\) and assume .

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain .

• With TIP \(_{\models }^{{\vdash }}\), we obtain \(\vdash \varphi \), as desired.

1. (3):

   To prove TIP \(_{\models }^{{\vdash }}\), assume .

• Then .

• With LCQ \(_{\models }\)(4), we obtain \(n\in {{\mathsf {Num}}}\) such that (i) .

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and LCQ \(_{\models }\)(1,2), we obtain .

• Now the proof of \(\vdash \varphi \) proceeds just like at point (1): using Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\) and Clean \(_{\Vdash }\).\(\square \)

Lemma 6 shows that, in the presence of standard models with reasonable properties and the soundness of \(\vdash ^{\textsf {b}}\), clean representability of the proof-of relation implies HBL \(^{\Leftarrow }_{1}\); and recall from Lemma 4 that it also implies HBL \(_{1}\). Interestingly, a converse of these implications also holds. To state it, we initially assume there is no “outer” notion of proof (i.e., no set \({{\mathsf {Proof}}}\) and no relation \(\mathrel {\Vdash }\)), but only an “inner” one, given by a formula \({\mathsf {Pf}}\in {{\mathsf {Fmla}}}_2\) such that:

• for all \(\varphi \in {{\mathsf {Sen}}}\).

• \(\models {\mathsf {Pf}}(n,\langle \varphi \rangle )\) implies \(\vdash ^{\textsf {b}}{\mathsf {Pf}}(n,\langle \varphi \rangle )\) for all \(n \in {{\mathsf {Num}}}\) and \(\varphi \in {{\mathsf {Sen}}}\).

• implies for all \(n \in {{\mathsf {Num}}}\) and \(\varphi \in {{\mathsf {Sen}}}\).

is the inner version of Rel \(_{\vdash } ^{\Vdash }\) : It expresses that, inside the representation, proofs and provability are connected as expected. and state that provability is complete on \({\mathsf {Pf}}\) statements about formula encodings, as well as on their negations; in traditional settings, this is true thanks to \({\mathsf {Pf}}\) being a \(\varDelta _1\)-formula. Now the converse result states that, thanks to standard models, HBL \(_{1}\) and HBL \(^{\Leftarrow }_{1}\), we can define an outer notion of proof that is represented by the inner notion \({\mathsf {Pf}}\):

Lemma 7

Assume , , , Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), LCQ \(_{\models }\)(4,5), HBL \(_{1}\), HBL \(^{\Leftarrow }_{1}\). Take \({{\mathsf {Proof}}}= {{\mathsf {Num}}}\) and define \(\mathrel {\Vdash }\) by \(n \mathrel {\Vdash }\varphi \) iff . Then Rel \(_{\vdash } ^{\Vdash }\), Repr \(_{\Vdash }\) and Clean \(_{\Vdash }\) hold, with \(\mathrel {\Vdash }\) being represented by \({\mathsf {Pf}}\) (i.e., being \({\mathsf {Pf}}\)).

Proof

To show Rel \(_{\vdash } ^{\Vdash }\) in this context (that is, for this particular definitions of \({{\mathsf {Proof}}}\) and relation \(\mathrel {\Vdash }\)), we must show the equivalence between (i) \(\vdash \varphi \) and (ii) the existence of \(n\in {{\mathsf {Num}}}\) such that \(\vdash ^{\textsf {b}}{\mathsf {Pf}}(n,\langle \varphi \rangle )\).

First assume (i).

• With HBL \(_{1}\), we obtain .

• With , we obtain \(\vdash ^{\textsf {b}}\exists x.\, {\mathsf {Pf}}(x,\langle \varphi \rangle )\).

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain \(\models \exists x.\, {\mathsf {Pf}}(x,\langle \varphi \rangle )\).

• With LCQ \(_{\models }\)(4), we obtain \(n\in {{\mathsf {Num}}}\) such that \(\models {\mathsf {Pf}}(n,\langle \varphi \rangle )\).

• With , we obtain (ii), as desired.

Now assume (ii).

• By logic, we obtain \(\vdash ^{\textsf {b}}\exists x.\, {\mathsf {Pf}}(x,\langle \varphi \rangle )\).

• With , we obtain .

• With HBL \(^{\Leftarrow }_{1}\), we obtain (i), as desired.

Showing half of Repr \(_{\Vdash }\) in this context is trivial, as it amounts to showing that \(\vdash ^{\textsf {b}}{\mathsf {Pf}}(n,\langle \varphi \rangle )\) implies \(\vdash ^{\textsf {b}}{\mathsf {Pf}}(n,\langle \varphi \rangle )\). For the other half, assume \({\not \vdash }^{\textsf {b}}\,{\mathsf {Pf}}(n,\langle \varphi \rangle )\).

• With , we obtain \(\not \models {\mathsf {Pf}}(n,\langle \varphi \rangle )\).

• With LCQ \(_{\models }\)(5), we obtain \(\models \lnot \, {\mathsf {Pf}}(n,\langle \varphi \rangle )\).

• With , we obtain \(\vdash ^{\textsf {b}}\lnot \, {\mathsf {Pf}}(n,\langle \varphi \rangle )\), as desired.

Finally Clean \(_{\Vdash }\) is trivial in this context, since the encoding of proofs is the identity. \(\square \)

The property TIP \(_{\models }^{{\vdash }}\) will be pivotal in the proofs of our semantic versions of \(\mathcal {IT}_ {1}\). As Lemma 6(3) shows, TIP \(_{\models }^{{\vdash }}\) follows from the soundness of \(\vdash ^{\textsf {b}}\), reasonable properties of \(\models \) (namely LCQ \(_{\models }\)(1,2,4)), and the Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\), Clean \(_{\Vdash }\) trio; and the last trio follows by Lemma 7 from the other assumptions if we assume an additional reasonable property of \(\models \) (namely LCQ \(_{\models }\)(5)), together with , , , and the weak representability of \(\vdash \) (i.e., HBL \(_{1}\) and HBL \(^{\Leftarrow }_{1}\)). One disadvantage of this indirect route for obtaining TIP \(_{\models }^{{\vdash }}\) is the need to have both and —which are very tedious to prove for concrete logics, especially . However, it turns out that we can directly prove TIP \(_{\models }^{{\vdash }}\) from a subset of the above assumptions, not including :

Lemma 8

Assume , , Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), and LCQ \(_{\models }\)(2,4). Define \({{\mathsf {Proof}}}\) and \(\mathrel {\Vdash }\) as in Lemma 7.

1. (1)

   Then implies for all \(\varphi \in {{\mathsf {Sen}}}\).

2. (2)

   If in addition we assume HBL \(^{\Leftarrow }_{1}\), then TIP \(_{\models }^{{\vdash }}\) holds.

Proof

(1): Assume (i) .

• From and Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain .

• With (i) and LCQ \(_{\models }\)(2), we obtain \(\models \exists x.\,{\mathsf {Pf}}(x,\langle \varphi \rangle )\).

• With LCQ \(_{\models }\)(4), we obtain \(n \in {{\mathsf {Num}}}\) such that \(\models {\mathsf {Pf}}(n,\langle \varphi \rangle )\).

• With , we obtain \(\vdash ^{\textsf {b}}{\mathsf {Pf}}(n,\langle \varphi \rangle )\).

• By logic, from this we obtain \(\vdash ^{\textsf {b}}\exists x.\, {\mathsf {Pf}}(x,\langle \varphi \rangle )\).

• With , by logic we obtain , as desired.

(2): Follows immediately from point (1), given that HBL \(^{\Leftarrow }_{1}\) and imply \(\vdash \varphi \). \(\square \)

Note that point (1) of the above lemma states that basic provability is complete for sentences of the form . For Robinson arithmetic and related theories, this follows from the completeness of provability for \(\varSigma _1\)-sentences (\(\varSigma _1\)-completeness).

The formula diagonalization technique (due to Gödel and Carnap [9]) yields “self-referential” sentences. All we need for it to work is (logic plus) the representability of substitution.

Proposition 9

Assuming Repr \(_{{\mathsf {S}}}\), for all \(\psi \in {{\mathsf {Fmla}}}_1\) there exists \(\varphi \in {{\mathsf {Sen}}}\) with \(\vdash ^{\textsf {b}}\varphi \!\mathrel {\;\leftarrow \rightarrow \;}\! \psi \langle \varphi \rangle \).

Proof

Assume Repr \(_{{\mathsf {S}}}\), where \({{\mathsf {S}}}\) is the “hard” self-substitution function. Let \(\chi \in {{\mathsf {Fmla}}}_1\) be . We take \(\varphi \) to be \(\chi \langle \chi \rangle \) and must prove (1) \(\vdash ^{\textsf {b}}\varphi \!\mathrel {\;\leftarrow \rightarrow \;}\! \psi \langle \varphi \rangle \).

• From the fact that \({{\mathsf {S}}}\) is represented by we obtain (provably in the formal system \(\vdash ^{\textsf {b}}\)) that \(\langle \varphi \rangle \) is the unique y for which holds.

• By logic, this implies .

• By the definition of \(\chi \), the above means exactly (1). A similar argument works for soft self-substitution. \(\square \)

A sentence \(\varphi \in {{\mathsf {Sen}}}\) is called:

• a Gödel sentence if ,

• a basic Gödel sentence ,

• a Rosser sentence if ,

• a basic Rosser sentence if .

Above, the formula \(\textsf {RosserTwist}(x,y)\) is . Here, \(y'\) represents the negation of y. If negation were represented not by a formula but by a unary function symbol , \(\textsf {RosserTwist}(x,y)\) would be written .

Since \(\vdash ^{\textsf {b}}\) is included in \(\vdash \), any basic Gödel or Rosser sentence is in particular a Gödel or Rosser sentence, respectively. It will turn out that basic Gödel sentences will be needed for the model-theoretic versions of \(\mathcal {IT}_ {1}\), whereas (not necessarily basic) Gödel or Rosser sentences will suffice for the proof-theoretic versions.

Proposition 10

Assuming Repr \(_{{\mathsf {S}}}\), there exist basic Gödel and basic Rosser sentences.

Proof

Follows immediately from Proposition 9, taking \(\psi (x)\) to be and , respectively. \(\square \)

Thus, any (basic) Gödel sentence is (basic-)provably equivalent to the negation of its own provability; in Gödel’s words, it “says about itself that it is not provable” [17]. A Rosser sentence \(\varphi \) asserts its own unprovability in a weaker fashion: Rather than saying “I am not provable” (i.e., “it is not the case that there exists a proof p of me”), it says “it is not the case that there exists a proof p of me such that all smaller q are not proofs of \(\lnot \,\varphi \).” Here, “smaller” refers to the order that the encoding of proofs as numerals imposes.

After last sections’ preparations, we are now ready to discuss different versions of the incompleteness theorems, based on alternative assumptions. This section deals with \(\mathcal {IT}_ {1}\), and the next one with \(\mathcal {IT}_{2}\).

For a consistent or \(\omega \)-consistent theory that is sufficiently expressive (in particular able to express concepts about itself, such as formulas and provability), \(\mathcal {IT}_ {1}\) identifies sentences that are neither provable nor disprovable, and are also true in the standard model —these are usually the Gödel and Rosser sentences discussed in the previous section.

6.1 Informal Account and Roadmap

Before embarking on the formal analysis of \(\mathcal {IT}_ {1}\), it is worth recalling informally the line of reasoning behind some of its variants. (More details can be found, e.g., in Boolos’s [5] and Smith’s [56] monographs.) Gödel’s original formulation referred to a system called P, a form of simple type theory enriched with the Dedekind–Peano axioms for natural numbers. However, it was soon recognized that the argument works for much weaker systems, notably Robinson arithmetic and a fortiori Peano arithmetic, as well as for any (\(\omega \)-)consistent recursively axiomatizable FOL theories that extend these.

When reading the informal (but quite detailed) recollection that follows, the reader should feel free to think of any of the above systems as target systems—so the term “provable” will refer to provability in one of these systems. To simplify the discussion, we will assume the availability of classical logic reasoning, but the later formal analysis will refine this by singling out the results that only need intuitionistic logic. Moreover, here we will not distinguish between provability and basic provability, but leave this too for our later formal analysis. Enclosing a statement in double quotes will mean that we refer to its internalization as a sentence in the language of the considered system; for example, the provability of “n is not a proof of \({\textsf {R}}\)” can be written using our formal notations as .

1. (1)

   Let us first consider a purely proof-theoretic \(\mathcal {IT}_ {1}\), which ignores the notion of truth and focuses on undecidability.

   1. (1.1)

      Gödel’s original argument goes as follows, for a Gödel sentence \({\textsf {G}}\).

      1. (1.1.1)

         That \({\textsf {G}}\) is unprovable is argued straightforwardly: The provability of \({\textsf {G}}\) on the one hand, by HBL \(_{1}\), would imply that its provability is provable, and on the other hand, by virtue of \({\textsf {G}}\) being a Gödel sentence, would imply that its unprovability is provable, thus contradicting consistency.

      2. (1.1.2)

         That \(\lnot \,{\textsf {G}}\) is unprovable needs a more subtle argument, which delves into actual proofs and their representation: The provability of \(\lnot \,{\textsf {G}}\) would imply, by consistency, the unprovability of \({\textsf {G}}\), i.e., the nonexistence of any proof of \({\textsf {G}}\), i.e., by proof representability, the provability of “n is not a proof of \({\textsf {G}}\)” for all n, i.e., by \(\omega \)-consistency, the unprovability of “there exists a proof of \({\textsf {G}}\)”, i.e., unprovability of “\({\textsf {G}}\) is provable”, i.e., by virtue of \({\textsf {G}}\) being a Gödel sentence, the unprovability of \(\lnot \,{\textsf {G}}\).

   2. (1.2)

      Rosser’s variant removes the need for \(\omega \)-consistency in Gödel’s argument for \(\lnot \,{\textsf {G}}\). This is done by using Rosser sentences \({\textsf {R}}\) instead of Gödel sentences \({\textsf {G}}\). (Recall form Sect. 5 that Rosser sentences assert about themselves something weaker than their unprovability, namely the nonexistence of any proof of them such that Rosser’s twist holds, i.e., there is no smaller proof of their negation.)

      1. (1.2.1)

         Arguing that \(\lnot \,{\textsf {R}}\) is unprovable goes the same as in Gödel’s case until the point of establishing the provability of “n is not a proof of \({\textsf {R}}\)” for all n, while additionally recording a proof p of \(\lnot \,{\textsf {R}}\) (from the assumption that \(\lnot \,{\textsf {R}}\) is provable), which by proof representability brings the provability of “\(\langle p\rangle \) is a proof of \(\lnot \,{\textsf {R}}\)”. So, taking \(m = \langle p\rangle \), we have the provability of “m is a proof of \(\lnot \,{\textsf {R}}\)” for a fixed m, and also of “n is not a proof of \({\textsf {R}}\)” for all n. Using a bit of Robinson arithmetic, this gives us the provability of “there exists no x such that x is a proof of \({\textsf {R}}\) and Rosser’s twist holds for x.” Hence, by virtue of \({\textsf {R}}\) being a Rosser sentence, we obtain the provability of \({\textsf {R}}\)—which, given our initial assumption that \(\lnot \,{\textsf {R}}\) is provable, contradicts consistency.

      2. (1.2.2)

         On the other hand, due to the aforementioned weaker “self-assertion” in Rosser sentences, Rosser’s argument for the unprovability of \({\textsf {R}}\) is not as immediate as in Gödel’s case, but itself needs to delve into proofs. First, proceeding in the same way as for \(\lnot \,{\textsf {R}}\), we obtain a dual of the situation from there: the provability of “m is a proof of \({\textsf {R}}\)” for a fixed m, and also of “n is not a proof of \(\lnot \,{\textsf {R}}\)” for all n. Again using a bit of Robinson arithmetic (a different bit than before!), we obtain the provability of “Rosser’s twist holds for m”, hence the provability of “there exists x such that x is a proof of \({\textsf {R}}\) and Rosser’s twist holds for x”, hence, by virtue of \({\textsf {R}}\) being a Rosser sentence, the provability of \(\lnot \,{\textsf {R}}\)—which, given our initial assumption that \({\textsf {R}}\) is provable, contradicts consistency.

2. (2)

   Now we move to the argument for why the given undecided sentence is also true in the standard model. In what follows, truth and falsity will implicitly refer to the standard model.

   1. (2.1)

      For a Gödel sentence \({\textsf {G}}\), we know that \({\textsf {G}}\) is not provable, hence there is no proof of \({\textsf {G}}\), hence, by proof representability, it is provable that “n is not a proof of \({\textsf {G}}\)” for all n. In particular, since deduction is sound w.r.t. truth, it is true that “n is not a proof of \({\textsf {G}}\)” for all n, i.e., that “for all x, x is not a proof of \({\textsf {G}}\)”, i.e., that “\({\textsf {G}}\) is not provable”. Hence, by virtue of \({\textsf {G}}\) being a Gödel sentence and deduction being sound, we obtain that \({\textsf {G}}\) is true.

   2. (2.2)

      The truth of a Rosser sentence \({\textsf {R}}\) follows by the same argument as above, noting that we only used that a Gödel sentence is implied by the statement of its own unprovability, which is also true for Rosser sentences.

3. (3)

   As we will show later during the formal discussion, if stated carefully the above arguments do not need the full power of classical logic, but intuitionistic logic suffices. On the other hand, if we assume classical logic (i.e., double negation) and additional properties mentioned below, more direct arguments can be given for some of \(\mathcal {IT}_ {1}\)’s components—more precisely, the arguments for the unprovability of \(\lnot \,{\textsf {G}}\) and the truth of \({\textsf {G}}\) no longer need to delve into proofs, but can stay at the level of provability. Below we only discuss the case of Gödel sentences; Rosser sentences can be treated in exactly the same way.

   1. (3.1)

      To argue that \(\lnot \,{\textsf {G}}\) is unprovable, we assume that it is provable. Hence, by virtue of \({\textsf {G}}\) being a Gödel sentence and making essential use of classical logic, we obtain the provability of “\({\textsf {G}}\) is provable”. At this point, we invoke the converse of HBL \(_{1}\) (i.e., the provability of any \(\varphi \) follows from the provability of \(\varphi \)’s provability) to obtain the provability of \({\textsf {G}}\), which together with our assumption contradicts consistency.

   2. (3.2)

      To argue that \({\textsf {G}}\) is true, we assume otherwise and try to reach a contradiction (thus making essential use of classical negation). Since \({\textsf {G}}\) is false, \(\lnot \,{\textsf {G}}\) must be true, hence by soundness and by virtue of \({\textsf {G}}\) being a Gödel sentence, “not not \({\textsf {G}}\) is provable” must be true, hence “\({\textsf {G}}\) is provable” must be true. At this point, we invoke that the truth of provability implies provability, a property that we called TIP \(_{\models }^{{\vdash }}\) in Sect. 4.6, to reach the desired conclusion, namely that \({\textsf {G}}\) is provable. In turn, TIP \(_{\models }^{{\vdash }}\) can be inferred from \(\varSigma _1\)-completeness (which states that, for all \(\varSigma _1\) sentences, in particular for those asserting provability, their truth implies their provability) and the converse of HBL \(_{1}\).

This concludes our informal recollection, which offers a roadmap for our formal and more abstract development that follows: Sects. 6.2–6.5 tackle the above points (1.1), (1.2), (2) and (3), respectively. We distill the exact assumptions needed in these arguments. This forms a basis for generalizing them to a large variety of logical systems, and also reveals some interesting properties required from the logic and arithmetic infrastructures and from the encodings that are not clearly visible in the concrete setting. In particular, we identify the purely intuitionistic line of reasoning that suffices for (1) and (2), the amount of arithmetic needed in (1.2), the tradeoffs between (1.1) and (1.2), and, in Sect. 6.6, the limits in combining provability with basic provability to widen these arguments’ scope.

6.2 Gödel’s Proof-Theoretic Version

We start with an analysis of Gödel’s original argument for the undecidability of Gödel sentences, which requires consistency for one half and \(\omega \)-consistency for the other half.

Proposition 11

Assume Con \(_{\vdash }\) and HBL \(_{1}\). Then \(\not \vdash {\textsf {G}}\) for all Gödel sentences \({\textsf {G}}\).

Proof

Let \({\textsf {G}}\) be a Gödel sentence. To prove \(\not \vdash {\textsf {G}}\), we assume (1) \(\vdash {\textsf {G}}\) and aim to reach a contradiction.

• From (1) and \({\textsf {G}}\) being a Gödel sentence, we obtain .

• From (1) and HBL \(_{1}\), we obtain , hence .

• The last two facts contradict Con \(_{\vdash }\).\(\square \)

For showing that the Gödel sentences are not disprovable, a standard route is to assume explicit proofs, strengthen the consistency assumption to \(\omega \)-consistency, and strengthen HBL \(_{1}\) to representability of the proof-of relation.

Proposition 12

Assume OCon \(_{\vdash }\), Rel \(_{\vdash } ^{\Vdash }\), Repr \(_{\Vdash }\), Clean \(_{\Vdash }\) . Then \(\not \vdash \lnot \, {\textsf {G}}\) for all Gödel sentences \({\textsf {G}}\).

Proof

Let \({\textsf {G}}\) be a Gödel sentence. To prove \(\not \vdash \lnot \, {\textsf {G}}\), we assume (1) \(\vdash \lnot \, {\textsf {G}}\) and aim to reach a contradiction.

• From OCon \(_{\vdash }\), we obtain Con \(_{\vdash }\).

• With (1), we obtain \(\not \vdash {\textsf {G}}\).

• With Rel \(_{\vdash } ^{\Vdash }\), we obtain \(p \mathrel {\not \Vdash }{\textsf {G}}\) for all \(p\in {{\mathsf {Proof}}}\).

• With Repr \(_{\Vdash }\) and Clean \(_{\Vdash }\), by Lemma 3 we obtain for all \(n \in {{\mathsf {Num}}}\).

• Since \(\vdash ^{\textsf {b}}\) is included in \(\vdash \), we obtain for all \(n \in {{\mathsf {Num}}}\).

• With OCon \(_{\vdash }\), we obtain , i.e., .

• With \({\textsf {G}}\) being a Gödel sentence, we obtain \(\not \vdash \lnot \, {\textsf {G}}\), which contradicts (1).\(\square \)

While the line of reasoning in the above proof is mostly well-known, it contains two subtle points about which the literature is not explicit (due to the usual focus on classical first-order arithmetic and particular choices of encodings).

First, we must assume the representation of the proof-of relation \(\mathrel {\Vdash }\) to be 1-clean, i.e., clean with respect to the proof component. Indeed, the argument crucially relies on converting the statement “\(p \mathrel {\not \Vdash }{\textsf {G}}\) for all \(p\in {{\mathsf {Proof}}}\)” into “ for all \(n \in {{\mathsf {Num}}}\),” which is only possible for 1-clean encodings. This assumption is needed in many of our results. By contrast, cleanness is never required with respect to the sentence component of proof-of or for the provability relation (which only involves sentence encodings). In short, cleanness is only needed for proofs, not for sentences.

Second, to reach the desired contradiction for our intuitionistic proof system \(\vdash \), from “ for all \(n \in {{\mathsf {Num}}}\)” it is not sufficient to employ standard \(\omega \)-consistency, which would only give us , i.e., ; the last together with would be insufficient for obtaining \(\not \vdash \lnot \, {\textsf {G}}\).

However, our stronger version of \(\omega \)-consistency, OCon \(_{\vdash }\), does the job.

\(\mathcal {IT}_ {1}\) now follows by putting together Propositions 10–12:

Theorem 13

(\(\mathcal {IT}_ {1}\)) Assume , Rel \(_{\vdash } ^{\Vdash }\), , , Repr \(_{{\mathsf {S}}}\). Then the following hold:

1. (1)

   There exists a basic Gödel sentence.

2. (2)

   \(\not \vdash {\textsf {G}}\) and \(\not \vdash \lnot \, {\textsf {G}}\) for all Gödel sentences \({\textsf {G}}\).

Proof

1. (1)

   : Immediate from Proposition 10.

2. (2)

   : \(\not \vdash \lnot \, {\textsf {G}}\) follows by applying Proposition 12 to the assumptions, so it remains to show \(\not \vdash {\textsf {G}}\).

   • From OCon \(_{\vdash }\), we obtain Con \(_{\vdash }\).

   • Applying Lemma 4 to Rel \(_{\vdash } ^{\Vdash }\) and Repr \(_{\Vdash }\) , we obtain HBL \(_{1}\).

   • Applying Proposition 11 to the last two facts, we obtain \(\not \vdash {\textsf {G}}\), as desired.\(\square \)

6.3 Rosser’s Version

Rosser’s contribution to \(\mathcal {IT}_ {1}\) was an ingenious trick for weakening the \(\omega \)-consistency assumption into plain consistency—as such, it is usually seen as a strict improvement over Gödel’s version. While this is true for the concrete case of FOL theories extending arithmetic, from an abstract perspective the situation is more nuanced: The improvement is achieved at the cost of asking more from the logic. Our framework makes this tradeoff clearly visible. The idea is to use Rosser sentences instead of Gödel sentences to “repair” the \(\omega \)-consistency assumption of Theorem 13 (inherited from Proposition 12).

Proposition 14

Assume Con \(_{\vdash }\), Ord \(_{2}\), Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\) Repr \(_\lnot \) and Clean \(_{\Vdash }\). Then \(\not \vdash \lnot \, {\textsf {R}}\) for all Rosser sentences \({\textsf {R}}\).

Proof

To prove \(\not \vdash \lnot \, {\textsf {R}}\), we assume (1) \(\vdash \lnot \, {\textsf {R}}\) and aim to reach a contradiction.

• With Rel \(_{\vdash } ^{\Vdash }\) , we obtain \(p \mathrel {\Vdash }\lnot \, {\textsf {R}}\) for some \(p \in {{\mathsf {Proof}}}\).

• With Repr \(_{\Vdash }\) , we obtain , hence (2) .

• From (1) and Con \(_{\vdash }\), we obtain \(\not \vdash {\textsf {R}}\).

• With Rel \(_{\vdash } ^{\Vdash }\) , we obtain \(q \mathrel {\not \Vdash }{\textsf {R}}\) for all \(q \in {{\mathsf {Proof}}}\).

• With Repr \(_{\Vdash }\) , Clean \(_{\Vdash }\) and Lemma 3, we obtain, for all \(n \in {{\mathsf {Num}}}\), , hence (3) .

• By Ord \(_{2}\), we obtain a finite \(M \subseteq {{\mathsf {Num}}}\) such that (4) \(\vdash \forall x. \, (\bigvee _{m \in M} x \equiv m) \vee \langle p\rangle \prec x\)

• We prove (5) . The proof is performed in the intuitionistic proof system of \(\vdash \), but we describe it informally: We fix x, assume , and aim to reach a contradiction. We perform a case distinction according to (4):

  • If x equals some \(m\in M\), then , which together with (3) leads to a contradiction.

  • If \(\langle p\rangle \prec x\), then from \(\textsf {RosserTwist}(x,\langle {\textsf {R}}\rangle )\) and (which holds thanks to Repr \(_\lnot \) and \(\vdash ^{\textsf {b}}\) being included in \(\vdash \)), we obtain , which together with (2) leads to a contradiction.

  • This concludes (our informal description of) the \(\vdash \)-formal proof of (5).

• From (5), by (intuitionistic) logic we obtain .

• Thanks to \({\textsf {R}}\) being a Rosser formula, we obtain \(\vdash {\textsf {R}}\).

• Together with (1), this contradicts Con \(_{\vdash }\).\(\square \)

Thus, \(\omega \)-consistency (assumption OCon \(_{\vdash }\)) has been weakened to consistency (assumption Con \(_{\vdash }\)), but in exchange we needed to additionally assume a special formula \(\prec \) satisfying Ord \(_{2}\). This represents a quite strong commitment to the arithmetical ordering.

Even worse, this fix on the assumptions needed to show the unprovability of the negated formula (\(\lnot \, {\textsf {R}}\)) complicates the proof of the unprovability of the direct formula (\({\textsf {R}}\)), which was trivial in Gödel’s version (Proposition 11). Now we again need a cleanly representable proof-of relation, representable negation, and well-behavedness of the order-like relation \(\prec \):

Proposition 15

Assume Con \(_{\vdash }\), Ord \(_{1}\), Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\) Repr \(_\lnot \) and Clean \(_{\Vdash }\) . Then \(\not \vdash {\textsf {R}}\) for all Rosser sentences \({\textsf {R}}\).

Proof

To prove \(\not \vdash {\textsf {R}}\), we assume (1) \(\vdash {\textsf {R}}\) and aim to reach a contradiction.

• With Rel \(_{\vdash } ^{\Vdash }\) , we obtain \(p \mathrel {\Vdash }{\textsf {R}}\) for some \(p \in {{\mathsf {Proof}}}\).

• With Repr \(_{\Vdash }\) , we obtain , hence (2) .

• From (1) and Con \(_{\vdash }\), we obtain \(\not \vdash \lnot \, {\textsf {R}}\).

• With Rel \(_{\vdash } ^{\Vdash }\) , we obtain \(q \mathrel {\not \Vdash }\lnot \, {\textsf {R}}\) for all \(q \in {{\mathsf {Proof}}}\).

• With Repr \(_{\Vdash }\) , Clean \(_{\Vdash }\) and Lemma 3, we obtain for all \(n \in {{\mathsf {Num}}}\).

• With Ord \(_{1}\), we obtain (3) .

• The following reasoning is performed in the (intuitionistic) proof system of \(\vdash \), but we describe it informally.

  • By Repr \(_\lnot \) and the fact that \(\vdash ^{\textsf {b}}\) is included in \(\vdash \), the only z such that is \(\langle \lnot \, {\textsf {R}}\rangle \).

  • With (3), we obtain \(\vdash \textsf {RosserTwist}(\langle p\rangle ,\langle {\textsf {R}}\rangle )\).

• From \(\vdash \textsf {RosserTwist}(\langle p\rangle ,\langle {\textsf {R}}\rangle )\) and (2), we obtain .

• Since \({\textsf {R}}\) is a Rosser sentence, from (1) we obtain .

• The last two facts contradict consistency.\(\square \)

Theorem 16

(\(\mathcal {IT}_ {1}\) à la Rosser) Assume , , , , Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\) ,Clean \(_{\Vdash }\) , Repr \(_{{\mathsf {S}}}\). Then the following hold:

1. (1)

   There exists a basic Rosser sentence.

2. (2)

   \(\not \vdash {\textsf {R}}\) and \(\not \vdash \lnot \, {\textsf {R}}\) for all Rosser sentences \({\textsf {R}}\).

Proof

1. (1)

   : Immediate from Proposition 10.

2. (2)

   : \(\not \vdash {\textsf {R}}\) follows by applying Proposition 15 to the assumptions, and \(\not \vdash \lnot \, {\textsf {R}}\) follows by applying Proposition 14 to the assumptions. \(\square \)

Highlighted in the statements of Theorems 16 and 13 is the assumption tradeoff between the two versions of \(\mathcal {IT}_ {1}\): Rosser’s weakening of \(\omega \)-consistency into consistency is paid by additionally assuming representability of negation and an order-like relation satisfying Ord \(_{1}\) and Ord \(_{2}\). Certainly, negation representability is not a big price, since for concrete logics this tends to be a lemma that is anyway needed when proving HBL \(_{1}\). On the other hand, the ordering assumptions seem to be a significant generality gap in favor of Gödel’s version.

6.4 Semantic Versions

A semantic version of \(\mathcal {IT}_ {1}\) is one that establishes not only the unprovability of Gödel or Rosser sentences and of their negations, but also the truth of these sentences. To capture this abstractly, we leverage our concept of truth from Sect. 4.6, denoted \(\models \).

Theorem 17

(Semantic \(\mathcal {IT}_ {1}\)) If we enrich the assumptions of Theorem 13 with LCQ \(_{\models }\)(2,3) and Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), then its conclusions can be enriched with the following:

(3) \(\models {\textsf {G}}\) for all basic Gödel sentences \({\textsf {G}}\).

Proof

We know from Theorem 13 that \(\not \vdash {\textsf {G}}\), and \(\not \vdash \lnot \, {\textsf {G}}\). It remains to show \(\models {\textsf {G}}\).

• From \(\not \vdash {\textsf {G}}\) and Rel \(_{\vdash } ^{\Vdash }\) , we obtain that \(p \nVdash {\textsf {G}}\) for all \(p\in {{\mathsf {Proof}}}\).

• With Repr \(_{\Vdash }\) and Clean \(_{\Vdash }\), by Lemma 3 we obtain for all \(n \in {{\mathsf {Num}}}\).

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain for all \(n \in {{\mathsf {Num}}}\).

• With LCQ \(_{\models }\)(3), we obtain (i) .

• By logic we obtain . (Recall Convention 5.)

• With the definition of basic Gödel sentence, by logic we obtain .

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain .

• With LCQ \(_{\models }\)(2) and (i), we obtain \(\models {\textsf {G}}\), as desired.\(\square \)

The next variant of the semantic \(\mathcal {IT}_ {1}\) does not directly assume the existence of proofs and their representations, but “recovers” them using HBL \(^{\Leftarrow }_{1}\) as prescribed in Lemma 7:

Theorem 18

(Semantic \(\mathcal {IT}_ {1}\), second variant) The conclusions of Theorem 17 remain true if we replace its assumptions Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\), Clean \(_{\Vdash }\) with the assumptions , , , HBL \(^{\Leftarrow }_{1}\), LCQ \(_{\models }\)(4,5).

Proof

Immediate by Lemma 7 and Theorem 17, noting that, by Lemma 4, HBL \(_{1}\) (which is needed by Lemma 7) is implied by Rel \(_{\vdash } ^{\Vdash }\) and Repr \(_{\Vdash }\). \(\square \)

Similar semantic theorems can be obtained for Rosser-style \(\mathcal {IT}_ {1}\):

Theorem 19

(Semantic \(\mathcal {IT}_ {1}\) à la Rosser) If we enrich the assumptions of Theorem 16 with LCQ \(_{\models }\)(2,3) and Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), then its conclusions can be enriched with the following:

   (3) \(\models {\textsf {R}}\) for all basic Rosser sentences \({\textsf {R}}\).

Proof

Exactly the same as the proof of Theorem 17, but using Rosser sentences and applying Theorem 16 (rather than using Gödel sentences and applying Theorem 13). Note that the last part of the proof of \(\models {\textsf {G}}\) also works for \({\textsf {R}}\), because follows from the definition of Rosser sentence (by logic). \(\square \)

Theorem 20

(Semantic \(\mathcal {IT}_ {1}\) à la Rosser, second variant) The conclusions of Theorem 19 remain true if we replace its assumptions Rel \(_{\vdash } ^{\Vdash }\) , Repr \(_{\Vdash }\), Clean \(_{\Vdash }\) with the assumptions , , , HBL \(^{\Leftarrow }_{1}\), LCQ \(_{\models }\)(4,5).

Proof

The same as Theorem 18’s proof, but using Theorem 19 rather than Theorem 17. \(\square \)

The assumption tradeoff between Theorems 17 and 18 on the one hand and Theorems 19 and 20 on the other hand is the same as that between their proof-theoretic counterparts (discussed in Sect. 6.3): OCon \(_{\vdash }\) on the Gödel side versus Con \(_{\vdash }\), Ord \(_{1}\), Ord \(_{2}\) and Repr \(_\lnot \) on the Rosser side. An interesting phenomenon arises when \(\vdash ^{\textsf {b}}\) and \(\vdash \) are the same relation. Then soundness implies \(\omega \)-consistency under reasonable assumptions:

Lemma 21

Assume \(\vdash ^{\textsf {b}}\;=\; \vdash \), Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and LCQ \(_{\models }\)(1,2,3). Then OCon \(_{\vdash }\) holds.

Proof

Assume \(\vdash \lnot \, \varphi (n)\) for all \(n\in {{\mathsf {Num}}}\).

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and \(\vdash ^{\textsf {b}}\;=\; \vdash \), we obtain \(\models \lnot \, \varphi (n)\) for all \(n\in {{\mathsf {Num}}}\).

• With LCQ \(_{\models }\)(3), we obtain \(\models \forall x. \,\lnot \, \varphi (x)\).

• By logic and Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain \(\models (\forall x.\, \lnot \, \varphi (x)) \rightarrow \lnot \, (\exists x.\, \varphi (x))\).

• From the last two facts and LCQ \(_{\models }\)(2), we obtain \(\models \lnot \, (\exists x.\, \varphi (x))\).

• With LCQ \(_{\models }\)(1,2), we obtain \(\not \models \lnot \lnot \, (\exists x.\, \varphi (x))\).

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and \(\vdash ^{\textsf {b}}\;=\; \vdash \), we obtain \(\not \vdash \lnot \lnot \, (\exists x.\, \varphi (x))\), as desired.\(\square \)

Thus, if \(\vdash ^{\textsf {b}}\;=\; \vdash \) and some reasonable properties hold for \(\models \), then \(\omega \)-consistency comes for free. Hence, in this case Gödel’s versions, Theorems 17 and 18, are strictly more general than Rosser’s versions, Theorems 19 and 20 (if we ignore the difference in the way Gödel and Rosser sentences are actually defined). This further illustrates the idea that Rosser’s trick is not always an improvement.

6.5 Classical Logic Versions

The results so far do not require going beyond intuitionistic logic. But if we commit to classical logic for \(\vdash \) (i.e., assume \(\vdash \lnot \lnot \, \varphi \rightarrow \varphi \)) and also assume HBL \(^{\Leftarrow }_{1}\), there is a well-known more direct argument for showing that Gödel sentences are not disprovable, which immediately proves \(\mathcal {IT}_ {1}\). (This is documented, for example, as Theorem 3.1 in Buldt’s monograph [7].) However, in our generalized setting with two provability relations, this argument does not go through unless we strengthen HBL \(^{\Leftarrow }_{1}\) (which currently refers to \(\vdash ^{\textsf {b}}\)) to refer to \(\vdash \):

• HBL \(^{\Leftarrow }_{1,\vdash }\): implies \(\vdash \varphi \) for all \(\varphi \in {{\mathsf {Sen}}}\).

Theorem 22

(Classical \(\mathcal {IT}_ {1}\)) Assume classical logic for \(\vdash \), Con \(_{\vdash }\), HBL \(_{1}\), HBL \(^{\Leftarrow }_{1,\vdash }\), Repr \(_{{\mathsf {S}}}\). Then the following hold:

1. (1)

   There exists a basic Gödel sentence.

2. (2)

   \(\not \vdash {\textsf {G}}\) and \(\not \vdash \lnot \,{\textsf {G}}\) for all Gödel sentences \({\textsf {G}}\).

Proof

1. (1):

   Immediate from Repr \(_{{\mathsf {S}}}\) by Proposition 10.

2. (2):

   Let \({\textsf {G}}\) be a Gödel sentence.

• From Con \(_{\vdash }\) and HBL \(_{1}\), by Proposition 11 we obtain \(\not \vdash {\textsf {G}}\).

• So we are left to prove \(\not \vdash \lnot \, {\textsf {G}}\). To this end, we assume (i) \(\vdash \lnot \, {\textsf {G}}\) and aim to reach a contradiction.

• Since \({\textsf {G}}\) is a Gödel sentence, by logic we obtain .

• By classical logic, from this we obtain .

• With HBL \(^{\Leftarrow }_{1,\vdash }\), we obtain \(\vdash {\textsf {G}}\).

• With (i), this contradicts Con \(_{\vdash }\).\(\square \)

Point (2) of the above theorem refers to Gödel sentences (defined using \(\vdash \)). Note that weakening the statement to refer to basic Gödel sentences (defined using \(\vdash ^{\textsf {b}}\)) would not help with relaxing the assumption HBL \(^{\Leftarrow }_{1,\vdash }\) to HBL \(^{\Leftarrow }_{1}\); the former would still be needed to finish the proof. Of course, HBL \(^{\Leftarrow }_{1}\) and HBL \(^{\Leftarrow }_{1,\vdash }\) coincide in the important case when \(\vdash ^{\textsf {b}}\; = \; \vdash \).

Two semantic versions are possible for classical \(\mathcal {IT}_ {1}\). The first one additionally assumes some reasonable properties of \(\models \), soundness for \(\vdash ^{\textsf {b}}\), and TIP \(_{\models }^{{\vdash }}\):

Theorem 23

(Classical Semantic \(\mathcal {IT}_ {1}\)) If we enrich the assumptions of Theorem 22 with LCQ \(_{\models }\)(1,2,5), Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), TIP \(_{\models }^{{\vdash }}\), then its conclusions can be enriched with the following: (3) \(\models {\textsf {G}}\) for all basic Gödel sentences \({\textsf {G}}\).

Proof

We know from Theorem 22 that (i) \(\not \vdash {\textsf {G}}\), and \(\not \vdash \lnot \, {\textsf {G}}\). It remains to show \(\models {\textsf {G}}\). To this end, we assume (ii) \(\not \models {\textsf {G}}\) and try to reach a contradiction.

• From (ii), by LCQ \(_{\models }\)(5) we obtain (iii) \(\models \lnot \,{\textsf {G}}\).

• From the basic Gödel sentence definition we obtain .

• With Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\), we obtain .

• With (iii), by LCQ \(_{\models }\)(2) we obtain .

• With LCQ \(_{\models }\)(1,2), we obtain .

• With LCQ \(_{\models }\)(5), we obtain .

• With TIP \(_{\models }^{{\vdash }}\), we obtain \(\vdash {\textsf {G}}\), which contradicts (i). \(\square \)

The second one replaces TIP \(_{\models }^{{\vdash }}\) with some assumptions that, in the presence of the others, ensure TIP \(_{\models }^{{\vdash }}\)—hence is strictly less general than the first one:

Theorem 24

(Classical Semantic \(\mathcal {IT}_ {1}\), second version) The conclusions of Theorem 23 still hold if we replace TIP \(_{\models }^{{\vdash }}\) with the assumptions , and LCQ \(_{\models }\)(4).

Proof

It suffices to show that TIP \(_{\models }^{{\vdash }}\) follows from its replacements and the other assumptions. We do this using Lemma 8(2). To apply this lemma, we need:

• , , LCQ \(_{\models }\)(4), which are assumed above;

• LCQ \(_{\models }\)(2), Sound \(_{\models }^{{\vdash ^{\textsf {b}}}}\) and HBL \(^{\Leftarrow }_{1}\), which are assumptions of Theorem 23.

So from the lemma we infer TIP \(_{\models }^{{\vdash }}\), as desired. \(\square \)

We used Gödel, not Rosser sentences in our classical semantic versions of \(\mathcal {IT}_ {1}\). Unlike for the (intuitionistic) semantic versions in Sect. 6.4, here a Rosser-style improvement would serve no purpose, since we already assume \(\vdash \) to be consistent, not \(\omega \)-consistent.

6.6 Benefits of the Two-Relation Take on Provability

Our framework distinguishes between basic provability (\(\vdash ^{\textsf {b}}\)) and provability (\(\vdash \)). This seems to be a rational design choice when aiming high in terms of generality for the incompleteness theorems. For example, this choice has been made explicitly by Smorynski [57] and more implicitly by Feferman [13] in their general accounts. Let us analyze what are the choice’s benefits to \(\mathcal {IT}_ {1}\) in the context of our development. The main questions are of course whether the scope of these theorems has to gain from the two-relation approach, as opposed to working with only one relation; and, if so, by how much.

In some cases, the gain is undeniable: Our Sect. 6.4’s semantic Theorems 17–20 gain significant generality by assuming soundness for \(\vdash ^{\textsf {b}}\) only, and merely consistency or \(\omega \)-consistency for \(\vdash \). This covers the case of Gödel or Rosser sentences being true for unsound theories as well. And of course the above theorems are based on the proof-theoretic theorems in Sects. 6.2 and 6.3, which means that the latter’s two-relation formulations are also needed.

At the other extreme, in one case, namely the classical-logic-based Theorem 22, there is no gain. Indeed, say we ignore \(\vdash ^{\textsf {b}}\) and modify all this theorem’s assumptions to replace \(\vdash \) for all occurrences of \(\vdash ^{\textsf {b}}\)—which is the same as assuming \(\vdash ^{\textsf {b}}\,{=}\, \vdash \). Then we would lose no generality, because the modified assumptions would be the same or weaker than the original assumptions. In conclusion, Theorem 22 stays equally general if we identify \(\vdash ^{\textsf {b}}\) and \(\vdash \).

The other cases, namely the classical-semantic Theorems 23 and 24, are somewhere in between these two extremes: Their two-relation formulation is more general than a one-relation formulation, but the gain from this is doubtful. Like in Theorems 17–20, they allow an unsound \(\vdash \) as an extension of a sound \(\vdash ^{\textsf {b}}\). On the other hand, their assumptions HBL \(_{1}\) and HBL \(^{\Leftarrow }_{1,\vdash }\) (inherited from Theorem 22) force \(\vdash \) to coincide with \(\vdash ^{\textsf {b}}\) on all sentences of the form ; and it is not clear if one can find interesting classes of unsound relations \(\vdash \) that satisfy this constraint (for standard choices of \(\vdash ^{\textsf {b}}\)).

For a consistent theory that is sufficiently expressive, \(\mathcal {IT}_{2}\) states that this theory cannot prove (the internal formalization of) its own consistency, which in our notations will be written as . Here, “sufficient expressiveness” refers to something similar to the case of \(\mathcal {IT}_ {1}\), namely the theory’s ability to express concepts about itself such as formulas and provability, but is a stronger requirement than for \(\mathcal {IT}_ {1}\): For \(\mathcal {IT}_{2}\), the theory needs to be expressive enough to formalize and prove part of \(\mathcal {IT}_ {1}\). This includes Peano arithmetic and stronger theories but excludes Robinson arithmetic.

\(\mathcal {IT}_{2}\) is of course a perfectly mathematical theorem, just like \(\mathcal {IT}_ {1}\). However, the informal paraphrasing of \(\mathcal {IT}_{2}\)’s conclusion, taking to mean that the theory cannot prove its own consistency, relies on an extra-mathematical assumption of an intensional nature [1] [13, §1]: that adequately expresses the provability relation \(\vdash \). The mathematical property of (weakly) representing \(\vdash \) is only an extensional approximation of this assumption. By contrast, \(\mathcal {IT}_ {1}\) only needs as an auxiliary concept used in its proof; the adequate expression of \(\vdash \) is irrelevant there, and it is only (weak) representability that matters. When discussing variants of \(\mathcal {IT}_{2}\), we will always work under the adequate expression assumption.

7.1 Informal Account and Roadmap

Similarly to the case of \(\mathcal {IT}_ {1}\), we start with an informal account of the argument behind \(\mathcal {IT}_{2}\), where again we use double quotes for sentences that internalize certain statements in the language of the considered system.

(1) Gödel realized that \(\mathcal {IT}_{2}\) follows by internally formalizing the positive half of his (proof-theoretic) \(\mathcal {IT}_ {1}\), henceforth referred to as \(\mathcal {IT}_ {0.5}\). It states the unprovability of a Gödel sentence \({\textsf {G}}\), covered by Sect. 6.1’s point (1.1) and Proposition 11. This leads to the provability of “the theory is consistent implies that \({\textsf {G}}\) is not provable”. Moreover, by virtue of \({\textsf {G}}\) being a Gödel sentence, \(\mathcal {IT}_ {0.5}\) itself implies the unprovability of “\({\textsf {G}}\) is not provable”. From the above together with consistency, we obtain the unprovability of “the theory is consistent”.

The three derivability conditions HBL\(_{1-3}\) recalled in Sect. 4.5 were perfected by Löb [32] based on previous work by Hilbert and Bernays [22] to make the above informal argument fully rigorous without referring to internal formalization details (although such details do need to be worked out to prove the conditions). The way these conditions work together to achieve this goal will be discussed in Sect. 7.2. For now, we should just note that the unqualified requirement of internally formalizing \(\mathcal {IT}_ {0.5}\) is in itself not sufficient. The internalized concepts must exhibit certain similarities to the original concepts from one level up; and this is what the derivability conditions express. For example, the above informal argument had a silent shift from the provability of “the theory is consistent implies that \({\textsf {G}}\) is not provable” (with the whole statement inside quotes) to the provability of “the theory is consistent” implies “\({\textsf {G}}\) is not provable” (where the implication operator is outside the quotes, i.e., is positioned one level up)—which is where HBL \(_{2}\) comes to help.

(2) An alternative line of reasoning due to Jeroslow [24] is often cited [50, 56, 57] as a simplification of the canonical route to prove \(\mathcal {IT}_{2}\): Whereas traditionally \(\mathcal {IT}_{2}\) requires all three derivability conditions, Jeroslow’s version does not make use of HBL \(_{2}\).

Jeroslow’s approach relies on pseudo-terms. These are formulas that satisfy existence and uniqueness properties on one of their free variables, say, x, meaning that x denotes a uniquely identified item depending on any items denoted by the other free variables; in short, pseudo-terms can essentially be treated like terms. In the informal discussion that follows, the reader is free to think of actual terms instead of pseudo-terms.

Jeroslow proved an alternative diagonalization lemma, producing pseudo-term fixpoints instead of formula fixpoints. In particular, one obtains a pseudo-term \(\tau \) that is provably equal to the encoding of the sentence “non-\(\tau \) is provable”. If we let \(\varphi \) denote the latter sentence, we obtain that \(\varphi \) is provably equivalent to “\(\lnot \,\varphi \) is provable”. Let us call any sentence satisfying this fixpoint property a Jeroslow sentence. Such a sentence states about itself something stronger-sounding than a Gödel (or Rosser) sentence: not that it is merely not provable, but that even its negation is provable. (We write “stronger-sounding” rather than “stronger” because it would be actually stronger only assuming the provability of consistency.)

Now, the argument for \(\mathcal {IT}_{2}\) goes as follows. Assume that “the theory is consistent” is provable. Because a Jeroslow sentence \(\varphi \) asserts the provability of something, (a slightly stronger form of) HBL \(_{3}\) applies, so \(\varphi \) provably implies “\(\varphi \) is provable”. On the other hand, by virtue of being a Jeroslow sentence, \(\varphi \) also provably implies “\(\lnot \,\varphi \) is provable”. So \(\varphi \) provably implies “the theory is inconsistent”, which together with our assumption gives the provability of \(\lnot \,\varphi \). With HBL \(_{1}\), we obtain the provability of “\(\lnot \,\varphi \) is provable”, i.e, by virtue of \(\varphi \) being a Jeroslow sentence, the provability of \(\varphi \). So both \(\varphi \) and its negation are provable, which contradicts consistency.

The above argument invokes HBL \(_{1}\) and HBL \(_{3}\) but not HBL \(_{2}\). It is specific to Jeroslow sentences and cannot be achieved with Gödel or Rosser sentences. The argument has several loose ends, which will be addressed in our formal discussion. In light of that, it will become clear that the \(\lnot \) in “\(\lnot \,\varphi \)” and the “non” in “non-\(\tau \)” are different, but related operators: The former is formula negation (applied to \(\varphi \)), while the latter is substitution (with \(\tau \)) in a pseudo-term that represents the operator on numerals corresponding to \(\lnot \) via formula encoding.

This concludes our informal discussion. Next, we engage in formal accounts of the above arguments: point (1) in Sect. 7.2 and point (2) in Sect. 7.3.

7.2 Standard Version

Let us slightly rephrase the statement and proof of \(\mathcal {IT}_ {0.5}\) (Proposition 11) in a way that will make it convenient to highlight its internal formalization within the proof of \(\mathcal {IT}_{2}\):

Proposition

11 (rephrased). Assume HBL \(_{1}\). Let \({\textsf {G}}\) be a Gödel sentence. Then Con \(_{\vdash }\) implies \(\not \vdash {\textsf {G}}\).

Proof

• Step 1. Since \({\textsf {G}}\) is a Gödel sentence, \(\vdash {\textsf {G}}\) implies .

• Step 2. By \(\vdash ^{\textsf {b}}\,{\subseteq }\, \vdash \) and HBL \(_{1}\), \(\vdash {\textsf {G}}\) implies .

• Step 3. By modus ponens (since \(\lnot \,{\textsf {G}}\) is \({\textsf {G}}\rightarrow \bot \)), and implies \(\vdash \bot \).

• Step 4. From the last three facts, \(\vdash {\textsf {G}}\) implies \(\vdash \bot \).

• Step 5. Hence Con \(_{\vdash }\) (i.e., \(\not \vdash \bot \)) implies \(\not \vdash {\textsf {G}}\), as desired.\(\square \)

The standard proof of \(\mathcal {IT}_{2}\) uses all three derivability conditions in key places in order to internalize the above proof of \(\mathcal {IT}_ {0.5}\):

Theorem 25

(\(\mathcal {IT}_{2}\)) Assume Con \(_{\vdash }\), HBL \(_{1}\), HBL \(_{2}\), HBL \(_{3}\) and Repr \(_{{\mathsf {S}}}\). Then .

Proof

Let \({\textsf {G}}\) be a Gödel sentence, which exists by Proposition 10 and Repr \(_{{\mathsf {S}}}\).

Internalizing the proof of \(\mathcal {IT}_ {0.5}\):

• Step 1. Since \({\textsf {G}}\) is a Gödel sentence, we obtain . With HBL \(_{1}\) and modus ponens, we obtain . With HBL \(_{2}\), we obtain .

• Step 2. From HBL \(_{3}\), we obtain .

• Step 3. From HBL \(_{2}\), we obtain .

• Step 4. From the last three facts, we obtain .

• Step 5. This implies , hence (1) .

Invoking \(\mathcal {IT}_ {0.5}\):

• From Con \(_{\vdash }\) and HBL \(_{1}\), by Proposition 11 we obtain \(\not \vdash {\textsf {G}}\).

• With the Gödel sentence definition, we obtain (2) .

Putting the two together :

• From (1) and (2), we obtain , as desired.\(\square \)

The above proof of \(\mathcal {IT}_{2}\) starts with an internalization of aspects of the \(\mathcal {IT}_ {0.5}\)’s proof. It does not literally formalize the end-to-end proof, but instead proceeds by plugging in the derivability conditions, which can be thought of as pre-formalized reasoning patterns.

• Step 2 is internalized using HBL \(_{3}\), which asserts the provability of some instances of HBL \(_{1}\), replacing object-level quantification with meta-level quantification. To see this, note that a full formalization of HBL \(_{1}\) would be a sentence of the form , where , , and formalize membership to the set of sentences \({{\mathsf {Sen}}}\), the encoding operator \(\langle \_\rangle \), the formula-instantiation (i.e., substitution of a term for the first variable, \(v_1\)) operator, and the inner representation of provability (one further level inside), respectively. By instantiating the \(\forall \)-quantified x with \(\langle \varphi \rangle \) for any \(\varphi \in {{\mathsf {Sen}}}\), we obtain sentences that can be equivalently written in a more palatable from, , which are exactly the sentences whose provability is asserted by HBL \(_{3}\).

• Similarly, Step 3 is internalized using HBL \(_{2}\), which asserts the provability of some instances of the modus ponens rule, again replacing object-level quantification with meta-level quantification—whereas a full formalization of HBL \(_{1}\) would be a sentence of the form .

• The internalization of Step 1 is more interesting: To formalize the fact that \(\vdash {\textsf {G}}\) implies , one takes advantage of the availability of the stronger and “more formal” property , which is pushed inside the proof system via HBL \(_{1}\), and then its implication is lifted one level up using HBL \(_{2}\).

• Steps 4 and 5 are internalized by mapping meta-implication and meta-negation to the implication and negation operators, \(\rightarrow \) and \(\lnot \), using the latter’s deductive properties.

In summary, a judicious use of the derivability conditions and other ad hoc procedures are used to prove an internalized version of \(\mathcal {IT}_ {0.5}\), while avoiding the need to fully formalize the proof inside the system. (On the other hand, proving the derivability conditions does require a substantial internal formalization effort in the first place.)

Theorem 25’s proof is concluded according to the plan sketched in Sect. 7.1: by combining the formalized and the original \(\mathcal {IT}_ {0.5}\) to obtain the unprovability of consistency.

Finally, let us scrutinize \(\mathcal {IT}_{2}\) with respect to the benefit of the two-relation take on provability (as was done for \(\mathcal {IT}_ {1}\) in Sect. 6.6). We see that for \(\mathcal {IT}_{2}\) there is no benefit from using two relations. The same reason as the one discussed for Theorem 22 applies: Replacing \(\vdash ^{\textsf {b}}\) with \(\vdash \) does not decrease generality. Thus, when discussing \(\mathcal {IT}_{2}\), we can assume \({\vdash ^{\textsf {b}}} = {\vdash }\) without loss of generality. Note also that, even if we used a formula corresponding \(\vdash ^{\textsf {b}}\), no meaningful two-relation strengthening of \(\mathcal {IT}_{2}\) would be in sight; in particular, the consistency of the basic theory \(\vdash ^{\textsf {b}}\) could well be provable in the extended theory \(\vdash \).

Convention 26

For the rest of Sect. 7, we will assume \({\vdash ^{\textsf {b}}} = {\vdash }\) and no longer refer to \(\vdash ^{\textsf {b}}\).

7.3 Jeroslow’s Version

Next we study Jeroslow’s approach to \(\mathcal {IT}_{2}\) [24]. To analyze its features and pitfalls, we need to recall into some notions and notations employed by Jeroslow.

A pseudo-term is a formula \(\varphi \in {{\mathsf {Fmla}}}_{m+1}\) expressing a provably functional relation via “exists unique”:

\(\vdash \forall x_1,\ldots ,x_m\,.\, \;\exists ! y. \varphi (x_1,\ldots ,x_m,y)\).

Note that we have already seen examples of pseudo-terms: Sect. 4.4’s formulas representing functions f.

We let \({{\mathsf {PTerm}}}\), ranged over by \(\sigma ,\tau \), be the set of pseudo-terms. While pseudo-terms are particular formulas, they will be treated as an extension of the notion of term. Indeed, a term t having free variables \(v_1,\ldots ,v_m\) can be regarded as the pseudo-term \(v_{m+1} \equiv t\).

Let \(\sigma \in {{\mathsf {Fmla}}}_{m+1}\) be a pseudo-term. Whereas \({{\mathsf {FVars}}}(\sigma ) = \{v_1,\ldots ,v_{m+1}\}\), the free variables of \(\sigma \) as a pseudo-term, written \({{\mathsf {FVarsP}}}(\sigma )\), will be \(\{v_1,\ldots ,v_{m}\}\); in this case, we will also write \(\sigma \in {{\mathsf {PTerm}}}_m\). A pseudo-term \(\sigma \) is closed if \({{\mathsf {FVarsP}}}(\sigma ) = \emptyset \), i.e., \(\sigma \in {{\mathsf {PTerm}}}_0\).

Pseudo-terms can be composed freely with terms and other pseudo-terms in a term-like fashion, and also substituted in formulas, as indicated in the following notation.

Notation 27

Given \(\sigma \in {{\mathsf {PTerm}}}_1\), \(\tau \in {{\mathsf {PTerm}}}_m\), \(t \in {{\mathsf {Term}}}\), and \(\varphi \in {{\mathsf {Fmla}}}_1\), we write:

1. (1)

   \(\sigma (t)\) instead of \(\sigma (t,v_2)\), assuming \(v_2 \notin {{\mathsf {FVars}}}(t)\) (note that \(\sigma (t)\) is closed if t is closed);

2. (2)

   \(\tau \equiv t\) instead of \(\tau (v_1,\ldots ,v_m,t)\);

3. (3)

   \(\varphi (\tau )\) instead of \(\exists y\,.\, \tau (v_1,\ldots ,v_m,y) \wedge \varphi (y)\), which thanks to the pseudo-term property is provably equivalent to \(\forall y\,.\, \tau (v_1,\ldots ,v_m,y) \rightarrow \varphi (y)\);

4. (4)

   \(\sigma (\tau )\) instead of \(\exists y\,.\, \tau (v_1,\ldots ,v_m,y) \wedge \sigma (y,v_{m+1})\), which again is provably equivalent to \(\forall y\,.\, \tau (v_1,\ldots ,v_m,y) \rightarrow \sigma (y,v_{m+1})\); note that \(\sigma (\tau ) \in {{\mathsf {PTerm}}}_m\).

Above, y is chosen to be distinct from the other occurring variables. It is possible to introduce multi-input extensions of this notation, but we will not need them. The notation smoothly integrates pseudo-terms with terms, as shown in the following example properties:

Example 28

1. (1)

   If \(\vdash \sigma \equiv t\) (employing point (1) of the notation) and \(\vdash \varphi (\sigma )\) (employing point (3)) then \(\vdash \varphi (t)\), where \(\varphi (t)\) is the usual instance of \(\varphi \) with t.

2. (2)

   If \(\varphi \in {{\mathsf {Fmla}}}_1\), \(\sigma \in {{\mathsf {PTerm}}}_1\) and \(\tau \in {{\mathsf {PTerm}}}_0\), then \(\vdash \varphi (\sigma )(\tau ) \!\mathrel {\;\leftarrow \rightarrow \;}\! \varphi (\sigma (\tau ))\). Indeed:

   • On the left of \(\mathrel {\;\leftarrow \rightarrow \;}\!\), we use point (3) for \(\varphi \) and \(\sigma \), which expands \(\varphi (\sigma )\) to \(\exists y\,.\, \sigma (v_1,y)\). Then, we use point (3) for \(\varphi (\sigma )\) and \(\tau \), which yields \(\exists y\,.\, \tau (y) \wedge \varphi (\sigma )(y)\). Combining the two, we obtain that \(\varphi (\sigma )(\tau )\) abbreviates \(\exists y\,.\, \tau (y) \wedge (\exists y'\,.\, \sigma (y,y') \wedge \varphi (y'))\).

   • On the right, we use point (4) for \(\sigma \) and \(\tau \), which expands \(\sigma (\tau )\) to \(\exists y\,.\, \tau (y) \wedge \sigma (y,v_1)\). Then we use point (3) for \(\varphi \) and \(\sigma (\tau )\), which yields \(\exists y. \sigma (\tau )(y) \wedge \varphi (y)\). Combining the two, we obtain that \(\varphi (\sigma (\tau ))\) abbreviates \(\exists y\,.\, (\exists y'\,.\, \tau (y') \wedge \sigma (y',y)) \wedge \varphi (y)\).

Jeroslow fixes an abstract class of “computable” m-ary functions, \(\mathcal {F}_m \subseteq {{\mathsf {Num}}}^m \rightarrow {{\mathsf {Num}}}\), for all arities \(m \in \mathbb {N}\), on which he considers the following assumptions:

• Repr \(_{\mathcal {F}}\): Every \(f\in \mathcal {F}_m\) is represented by some pseudo-term under the identity encoding \({{\mathsf {Num}}}\rightarrow {{\mathsf {Num}}}\).

• CapN: Some \(\mathsf {N}\in \mathcal {F}_1\) correctly captures negation: \(\mathsf {N}\langle \varphi \rangle = \langle \lnot \, \varphi \rangle \) for all \(\varphi \in {{\mathsf {Sen}}}\).

• CapSS: Some \({{\mathsf {ssub}}}: {{\mathsf {Fmla}}}_1 \rightarrow \mathcal {F}_1\) correctly captures substituted self-substitution: for all \(\psi \in {{\mathsf {Fmla}}}_1\) and \(f \in \mathcal {F}_1\).^{Footnote 1}

Note that, in CapSS, we take advantage of the introduced notation for pseudo-terms: If we spell out Notation 27(2), the highlighted text denotes . Moreover, employing Notation 27(1), the statement of Repr \(_{\mathcal {F}}\) for some \(f\in \mathcal {F}_1\) and \(n\in {{\mathsf {Num}}}\) would be written as ; and combining CapN with the instance of Repr \(_{\mathcal {F}}\) for \(\mathsf {N}\), we obtain a fact that, using the same notation, can be written as .

When our logical theory is a recursive extension of Robinson arithmetic and \({{\mathsf {Num}}}= \mathbb {N}\), \(\mathcal {F}_m\) could be any sufficiently rich the set of m-ary computable functions, ranging from the primitive recursive functions to all total \(\mu \)-recursive functions. Then, every \(f \in \mathcal {F}_m\) would indeed be represented by a formula . Moreover, assuming a computable and injective encoding of formulas, \(\langle \_\rangle : {{\mathsf {Fmla}}}_1 \rightarrow \mathbb {N}\), we can take \(\mathsf {N}: \mathbb {N}\rightarrow \mathbb {N}\) to be the following computable function: Given input n, it checks if n has the form \(\langle \varphi \rangle \); if so, it returns \(\langle \lnot \,\varphi \rangle \); if not, it returns any value (e.g., 0). And \({{\mathsf {ssub}}}(\psi )\) can be defined similarly, obtaining the desired property for every \(\varphi \in {{\mathsf {Fmla}}}_2\), not necessarily of the form .

In short, Jeroslow’s assumptions cover arithmetic (but also potentially many other systems).

The heart of Jeroslow’s approach lies in his diagonalization lemma, which offers pseudo-term fixpoints, and from them formula fixpoints as well:

Lemma 29

Assume CapSS and Repr \(_{\mathcal {F}}\) and let \(\psi \in {{\mathsf {Fmla}}}_1\). Then there exists a closed pseudo-term \(\tau \) such that \(\vdash \tau \equiv \langle \psi (\tau )\rangle \). Moreover, taking \(\varphi = \psi (\tau )\), we have \(\vdash \varphi \!\mathrel {\;\leftarrow \rightarrow \;}\! \psi \langle \varphi \rangle \).

Proof

Let \(f = {{\mathsf {ssub}}}(\psi )\) and . From CapSS, we obtain .

With Repr \(_{\mathcal {F}}\), we obtain , i.e., \(\vdash \tau \equiv \langle \psi (\tau )\rangle \).

By logic, from this we obtain \(\vdash \psi (\tau ) \!\mathrel {\;\leftarrow \rightarrow \;}\! \psi (\langle \psi (\tau )\rangle ) \), i.e., \(\vdash \varphi \!\mathrel {\;\leftarrow \rightarrow \;}\! \psi \langle \varphi \rangle \). \(\square \)

Lemma 29 can be used to produce Gödel and Rosser sentences, which can be used like in Sect. 6, leading to variants of \(\mathcal {IT}_ {1}\).

However, as discussed in Sect. 7.1, Jeroslow’s main innovation affects \(\mathcal {IT}_{2}\): It removes from the assumptions the second derivability condition, HBL \(_{2}\).

Theorem 30

(\(\mathcal {IT}_{2}\) à la Jeroslow) Assume Con \(_{\vdash }\), HBL \(_{1}\), , Repr \(_{\mathcal {F}}\), CapN, CapSS, SHBL \(_{3}\) denotes the condition: for all closed pseudo-terms \(\tau \).

Then , where \(\textsf {jcon}\) denotes .

As with Rosser’s trick, we analyze this innovation’s tradeoffs from an abstract perspective. A first tradeoff is in the employment of a stronger version of the third condition, SHBL \(_{3}\), holding for all closed pseudo-terms and not only those that encode sentences.

Another tradeoff is in the way consistency is expressed in the logic. Jeroslow does not conclude , but something more elaborate, namely \(\not \vdash \textsf {jcon}\). While the formula internalizes the statement \(\not \vdash \bot \), \(\textsf {jcon}\) internalizes the equivalent statement “for all \(\varphi \), it is not the case that \(\vdash \varphi \) and \(\vdash \lnot \, \varphi \).” But are the internalizations themselves equivalent, i.e., is it the case that iff \(\vdash \textsf {jcon}\)? This surely holds for many concrete logics, but it is only one direction that we can infer logic-independently, under mild assumptions:

Proposition 31

Assume HBL \(_{1}\), Repr \(_{\mathcal {F}}\), CapN. Then \(\vdash \textsf {jcon}\) implies .

Proof

Assume \(\vdash \textsf {jcon}\).

• Instantiating \(\textsf {jcon}\) with \(\langle \bot \rangle \), we obtain

• From Repr \(_{\mathcal {F}}\) and CapN, we obtain .

• From the last two facts, by logic we obtain .

• From \(\vdash \lnot \, \bot \) and HBL \(_{1}\), we obtain .

• From the last two facts, by logic we obtain , as desired.\(\square \)

It seems impossible to infer the other direction without knowing what looks like more concretely. Therefore, , the original \(\mathcal {IT}_{2}\)’s conclusion, is abstractly stronger than, hence preferable to \(\not \vdash \textsf {jcon}\). In short, Jeroslow somewhat weakens the theorem’s conclusion.

Let us now look at (a slight rephrasing of) Jeroslow’s proof:

Proof of Theorem 30

We assume (1) \(\vdash \textsf {jcon}\) and aim to reach a contradiction.

• Applying Lemma 29 to the formula , we obtain a closed pseudo-term \(\tau \) such that \(\vdash \tau \equiv \langle \varphi \rangle \) and (2) , where \(\varphi \) denotes .

• By SHBL \(_{3}\) applied to , we obtain , i.e., (3) .

• From (2) and (3), we obtain .

• On the other hand, (1) instantiated with \(\langle \varphi \rangle \) gives us .

• From the last two facts, we obtain (4) \(\vdash \lnot \, \varphi \).

• With HBL \(_{1}\), we obtain .

• From Repr \(_{\mathcal {F}}\) and CapN, we obtain .

• From the last two facts, by logic we obtain .

• With (2), we obtain \(\vdash \varphi \). Together with (4), this contradicts Con \(_{\vdash }\). \(\square \)

The above proof has a subtle gap, which makes Theorem 30incorrect under its stated assumptions. The problem lies in the highlighted description of the formula \(\varphi \). Strictly speaking (i.e., rigorously employing our Notation 27), the correct form of fact (2) is not but , and the correct \(\varphi \) is not but . So let us write \(\varphi \) for the correct version, , and \(\varphi '\) for . Notice the difference: \(\varphi \) is obtained by first instantiating with and then instantiating the remaining formula with \(\tau \), whereas \(\varphi '\) is obtained by first instantiating with \(\tau \) and then instantiating with the result. Both sentences occur in the proof: \(\varphi \) comes from Lemma 29, while \(\varphi '\) comes from SHBL \(_{3}\). For most purposes in logic, the difference is minor, since (as we note in Example 28(2)) \(\varphi \) and \(\varphi '\) are provably equivalent. However, as we discuss below, shifting between \(\varphi \) and \(\varphi '\) must be done with care, since the proof uses them under the encoding \(\langle \_\rangle \).

A first attempt to fill this gap would be to require \(\langle \varphi \rangle = \langle \varphi '\rangle \), or at least \(\vdash \langle \varphi \rangle \equiv \langle \varphi '\rangle \). The latter would be true under the assumption that the encodings of provably equivalent sentences are provably equal. But assuming this is unreasonable: Usually sentence equivalence is undecidable, so no computable encoding can achieve that.^{Footnote 2}\(^{,}\)^{Footnote 3} A more feasible solution comes from noting that the proof does not need \(\vdash \langle \varphi \rangle \equiv \langle \varphi '\rangle \), but could work with the weaker property . The latter would be true under the following assumption:

• WHBL \(_2\): \(\vdash \varphi \!\mathrel {\;\leftarrow \rightarrow \;}\! \psi \) implies for all \(\varphi ,\psi \in {{\mathsf {Sen}}}\).

Since the \(\rightarrow \) in WHBL \(_2\) can be replaced with \(\mathrel {\;\leftarrow \rightarrow \;}\!\) without changing the meaning, WHBL \(_2\) can be read as: encodings of provably equivalent sentences are provably equiprovable. Also, WHBL \(_2\) is a weakening of

• \(\vdash \varphi \rightarrow \psi \) implies for all \(\varphi ,\psi \in {{\mathsf {Sen}}}\)

which, in the presence of HBL \(_{1}\), is seen to be a weak form of HBL \(_{2}\).^{Footnote 4} This motivates the name “WHBL \(_2\)”. We are led to the following solution:

Correction 1

Theorem 30 becomes correct if we add WHBL \(_2\) as an assumption.

Proof

Indeed, using WHBL \(_2\), we can fill the gap in Theorem 30’s proof as follows:

\(\ldots \) (same as before)

• Applying Lemma 29 to the formula , we obtain a closed pseudo-term \(\tau \) such that \(\vdash \tau \equiv \langle \varphi \rangle \) and , where \(\varphi \) denotes .

• Since by Example 28(2), with the above we obtain (2) .

• By SHBL \(_{3}\) applied to , we obtain , i.e., (3’) , where \(\varphi '\) denotes .

• Since \(\vdash \varphi \!\mathrel {\;\leftarrow \rightarrow \;}\! \varphi '\), by WHBL \(_2\) we obtain .

• From this and (3’), we obtain (3) . \(\ldots \) (same as before)

\(\square \)

In summary, one solution to filling the gap in Jeroslow’s approach, which aimed at removing HBL \(_{2}\), was to (re)introduce a weaker version of HBL \(_{2}\), namely WHBL \(_2\).

An alternative solution is to replace representation by pseudo-terms with actual term-representation (defined in Sect. 4.4). To this end, we amend SHBL \(_{3}\) to quantify over all closed terms t instead of all closed pseudo-terms \(\tau \); moreover, also factoring in the observation that Jeroslow’s proof does not need \(\mathcal {F}_n\) for all n but \(\mathcal {F}_1\) suffices, we change Repr \(_{\mathcal {F}}\) into:

• Repr \(_{\mathcal {F}}\): Every \(f\in \mathcal {F}_1\) is term-represented, under the identity encoding \({{\mathsf {Num}}}\rightarrow {{\mathsf {Num}}}\), by some taken from a set \({{\mathsf {Ops}}}\subseteq ({{\mathsf {Term}}}\rightarrow {{\mathsf {Term}}})\) for which an encoding as numerals \(\langle \_\rangle : {{\mathsf {Ops}}}\rightarrow {{\mathsf {Num}}}\) is given, and such that \({{\mathsf {FVars}}}(g(t)) = {{\mathsf {FVars}}}(t)\) and \((g(t))[s/x]= g(t[s/x])\) for all \(g\in {{\mathsf {Ops}}}\), \(s,t\in {{\mathsf {Term}}}\) and \(x\in \mathsf {{Var}}\).

(In concrete logics, the elements of \({{\mathsf {Ops}}}\) can be constructors or derived operators on terms.)

Correction 2

Theorem 30 becomes correct if we work with terms rather than pseudo-terms and amend SHBL \(_{3}\) and Repr \(_{\mathcal {F}}\) as indicated above.

Proof

Indeed, all the proofs of CapSS, Lemma 29 and Theorem 30 work if we switch from pseudo-terms to terms. \(\square \)

In summary, our second solution requires the following amendment to Jeroslow’s approach: For representing computable functions, we must have available not just pseudo-terms, but actual terms. This usually means that the logic has built-in Skolem symbols and axioms.

Finally, let us see what it takes to alleviate the second tradeoff: from \(\not \vdash \textsf {jcon}\) to the more desirable . We consider the following condition:

• HBL \(_{4}\): for all \(\varphi ,\psi \in {{\mathsf {Sen}}}\).

HBL \(_{4}\) has a similar flavor as HBL \(_{2}\), but refers to conjunction rather than implication: It states that conjunction introduction holds inside the proof system.

Theorem 32

If we modify Theorem 30 by applying Correction 1 (i.e., adding assumption WHBL \(_2\)) and adding assumption HBL \(_{4}\), then its conclusion can be upgraded to .

Proof

The only time when \(\vdash \textsf {jcon}\) is used in the proof is via its specific instance , which by Repr \(_{\mathcal {F}}\) and CapN would follow from (1) . So it suffices to show that the last follows from , WHBL \(_2\) and HBL \(_{4}\):

• From HBL \(_{4}\), we obtain .

• From WHBL \(_2\) and , we obtain .

• From the last two facts, we obtain .

• Hence .

• With , we obtain (1), as desired.\(\square \)

Note that a version of Theorem 32 relying on Correction 2 rather than Correction 1 would be weaker than Theorem 32, since WHBL \(_2\) is necessary in the proof even if we work with terms instead of pseudo-terms.

In summary, Theorem 32 highlights the following assumption tradeoff in Jeroslow’s approach, provided the same strong conclusion as in the standard \(\mathcal {IT}_{2}\) is desired: the removal of HBL \(_{2}\) against the addition of WHBL \(_2\) and HBL \(_{4}\) (and the slight strengthening of HBL \(_{3}\) into SHBL \(_{3}\)). Whether this is a good tradeoff will of course depend on the logic’s specificity, in particular, on its primitive rules of inference.

Jeroslow presented his approach for an abstract logical theory over a FOL language, which is not necessarily a FOL theory—so it found a natural fit in our generic framework. Jeroslow’s account is extremely sketchy and notationally ambiguous. In spite of this account having become part of the \(\mathcal {IT}_{2}\) folklore, very few subsequent authors present it rigorously, and none at its original level of generality. Smith’s monograph gives a rigorous account for arithmetic [56, §33], silently performing Correction 2,^{Footnote 5} but failing to detect the need for SHBL \(_{3}\) instead of HBL \(_{3}\) (which Jeroslow had noticed). A mechanical proof assistant is of invaluable help with detecting such nuances and pitfalls.

We conclude with an anecdote involving our Isabelle formalization and Jeroslow’s notations. Given the relative simplicity of Lemma 29, we were not too surprised that Isabelle’s Sledgehammer [41] was able to prove it automatically. But Sledgehammer went further. It reported to have used the equality-reflexivity rule for \(\vdash \) in the proof. And it had found a term (not a pseudo-term) t for which it had proved not just \(\vdash t \equiv \langle \psi (t)\rangle \), but actual equality, \(t = \langle \psi (t)\rangle \); in particular, the term was a numeral. All this was too good to be true. It took us some time to realize why that happened: Due to one of Jeroslow’s notations, who wrote f instead of (thus identifying a function with its representing pseudo-term), we had at first misstated CapSS, writing instead of ; the former is still a valid expression, since f is a function between numerals which are particular terms. Embarrassingly, it took us even longer to realize why this variation discovered by chance was not an improvement of Jeroslow’s diagonalization lemma: because the assumption CapSS becomes unreasonable. Indeed, no concrete computable function would then be able to act like the intended \({{\mathsf {ssub}}}(\psi )\): Given an input n, (1) decode it into a unique formula \(\varphi \) such that \(n=\langle \varphi \rangle \), (2) decode \(\varphi \) into a unique function f such that and (3) proceed to apply f as part of producing . The second step requires an injective and computable encoding of computable functions into formulas, which is impossible.

Using our generic infrastructure (Sect. 4), we have formally proved Gödel-style and Rosser-style diagonalization lemmas (Sect. 5) and several abstract incompleteness results.

They include several versions of \(\mathcal {IT}_ {1}\):

• Gödel’s original \(\mathcal {IT}_ {1}\) (Theorem 13) and an \(\mathcal {IT}_ {1}\) based on classical logic (Theorem 22) required the formalization of some well-known arguments without change.

• Rosser’s \(\mathcal {IT}_ {1}\) (Theorem 16) involved the generalization of a well-known argument: distilling two abstract conditions, Ord \(_{1}\) and Ord \(_{2}\).

• Novel semantic variants of \(\mathcal {IT}_ {1}\) (Theorems 17–20, 23 and 24) arose from analyzing the interplay between standard models, HBL \(_{1}\)’s “iff” version, and proof representability.

They also include two versions of \(\mathcal {IT}_{2}\):

• The standard \(\mathcal {IT}_{2}\) based on the three derivability conditions (Theorem 25) again only required formalizing a well-known argument.

• The alternative, Jeroslow-style \(\mathcal {IT}_{2}\) (Theorem 30 with its two corrections, and Theorem 32) involved a detailed analysis and correction of an existing abstract result.

All the results presented so far operate abstractly, under certain assumptions—starting with a logic as generic as possible and adding structure and hypotheses as needed, while exploring conditions that enable different formulations of the results with various tradeoffs; concrete encodings and recursiveness are below the abstraction level of these results. By contrast, some of the previous mechanization projects, namely those by Shankar [52, 53], O’Connor [36], Harrison [21] and Paulson [40], focused on the impressive goal of “getting all the work done.” They fully proved the incompleteness theorems in particular settings, which involved defining the concrete Gödel encodings.

These two types of developments are complementary, and they both contribute to formally taming the complex ramifications of the incompleteness theorems.

This section will discuss concrete instances of the abstract results. We start by listing our mechanized instances (Sect. 9.1), and explain how they have been based on Paulson’s prior Isabelle development (Sect. 9.2). When instantiating our abstract assumptions to Paulson’s setting, not only did we recover his results, but were also able to upgrade them. This did require modifying some concrete proofs, but even when doing that we relied on top-down insight from the abstract results; in fact, as we are about to discuss, insight has traveled bottom-up as well. We also revisit major developments in other provers (Sect. 9.3), and finally briefly sketch a wider array of possible instances (Sect. 9.4).

9.1 Our Mechanized Instances

We first validate the assumptions about our abstract logic and arithmetic:

Proposition 33

(1) Any FOL theory that extends Robinson arithmetic or HF set theory satisfies all the axioms in our logical and arithmetic substrata (in Sects. 4.1, 4.2 and 4.3).

(2) If, in addition, the theory is sound, then, together with its corresponding standard model, it also satisfies all our model-theoretic axioms (in Sect. 4.6).

In particular, point (2) shows that our abstract framework for standard models applies equally well to \(\mathbb {N}\) and the datatype of HF sets. In the latter case, \({{\mathsf {Num}}}\) becomes the entire set of closed terms, so that numerals can denote arbitrary HF sets. This illustrates the versatility of our abstract concept of numeral.

We instantiate two of our main theorems in three ways:

Theorem 34

Let T be a FOL theory that extends HF set theory with a finite set of axioms, and let \(\vdash ^{\textsf {b}}\) and \(\vdash \) be the same relation, namely provability from T.

1. (1)

   If T is then the hypotheses of Theorems 24 and 25 are satisfied, i.e., \(\mathcal {IT}_ {1}\) (classical semantic version) and \(\mathcal {IT}_{2}\) hold for T.

2. (2)

   If T is , then the hypotheses of Theorem 25 are satisfied, i.e., \(\mathcal {IT}_{2}\) holds for T.

9.2 Connection to Paulson’s Results

The above instances are heavily based on the lemmas proved by Paulson in his Isabelle/HOL formalization of \(\mathcal {IT}_ {1}\) (covering both the proof-theoretic and the semantic aspect) and \(\mathcal {IT}_{2}\) [39, 40]. Paulson formalized quite faithfully Świerczkowski’s detailed account [61], but he also strengthened and slightly corrected it. Świerczkowski’s work applies to HF set theory [61, 62], a classical FOL theory axiomatizing hereditarily finite sets by means of an induction principle stating that the universe is comprised of such sets only. Paulson extended Świerczkowski’s incompleteness to essential incompleteness with respect to any finite sound extension of HF set theory within the same FOL language.

Our Theorem 34’s point (1) is a restatement of Paulson’s formalized results: theorems Goedel\(\_\)I and Goedel\(\_\)II in [40]. By contrast, point (2) is an upgrade of Paulson’s Goedel\(\_\)II, applicable to any finite consistent, though possibly unsound theory. This stronger version is a more standard form of \(\mathcal {IT}_{2}\), free from any model-theoretic dependencies. Paulson proved both HBL \(_{1}\) and HBL \(^{\Leftarrow }_{1}\) taking advantage of soundness, so to achieve the upgrade we had to discard HBL \(^{\Leftarrow }_{1}\) and re-prove HBL \(_{1}\) by replacing any semantic arguments with proofs within the HF calculus. We also removed all invocations of the \(\varSigma _1\)-completeness lemma, which happened to depend on soundness due to Paulson’s choice of \(\varSigma _1\)-sentence definition.

This instantiation process has offered us important feedback into the abstract results. A formal development such as ours is (largely) immune to reasoning errors, but not to missing out on useful pieces of generality. We experienced this firsthand with our assumptions about substitution. An a priori natural choice was to assume representability of the numeral substitution \({{\mathsf {Sb}}}: {{\mathsf {Fmla}}}_1 \times {{\mathsf {Num}}}\rightarrow {{\mathsf {Sen}}}\) (defined as \({{\mathsf {Sb}}}(\varphi ,n) = \varphi (n)\)), part of which means (1) . Instead, Paulson had proved (2) . Unlike (1), Paulson’s (2) applies the term encoding function \(\langle \_\rangle : {{\mathsf {Term}}}\rightarrow {{\mathsf {Num}}}\) to numerals as well (which are particular terms); and since his \(\langle \_\rangle \) function is injective, it is far from the case that \(\langle n\rangle = n\) for all numerals n. Paulson’s version makes more sense than ours when building the results bottom-up: Representability should not discriminate numerals, but filter them through the encodings like other terms. However, top-down our version also made sense: It yielded the incompleteness theorems under reasonable assumptions, which do hold, by the way, for HF set theory—even though in a bottom-up development one is unlikely to prove them. We resolved this discrepancy through a common denominator: the representability of self-substitution \({{\mathsf {S}}}: {{\mathsf {Fmla}}}_1 \rightarrow {{\mathsf {Sen}}}\) (Sect. 4.4), which made our results more general.

Paulson’s formalization has also inspired our abstract treatment of standard models (Sect. 4.6). Since Paulson proved HBL \(^{\Leftarrow }_{1}\) and used classical logic, an obvious “port of entry” of his \(\mathcal {IT}_{2}\) into our framework is Theorem 22, taking both \(\vdash ^{\textsf {b}}\) and \(\vdash \) to be Paulson’s provability relation (which is classical provability in a finite extension of HF set theory). But this theorem tells us nothing about the Gödel sentences’ truth. Delving deeper into Paulson’s development, we noted that, following Świerczkowski, he (unconventionally) completely avoided Repr \(_{\Vdash }\) , and did not even define \(\mathrel {\Vdash }\). This raised the question of whether HBL \(^{\Leftarrow }_{1}\) and Repr \(_{\Vdash }\) are somehow interchangeable in the presence of Standard Models standard models (on which Paulson relies heavily); and we found that they indeed are, under mild assumptions about truth (as we discuss in Sect. 4.6). This analysis has led to variants of our semantic \(\mathcal {IT}_ {1}\), Theorems 18 and 20, which incidentally do not need classical logic. Although our Theorem 18 seemed like an excellent candidate to instantiate to Paulson’s semantic \(\mathcal {IT}_ {1}\), its instantiation turned out to be difficult. All its assumptions were easy to fulfill based on what Paulson had already proved, except for . Indeed, whereas Paulson proved that his proof-of relation is a \(\varSigma _1\)-formula (which implies by \(\varSigma _1\)-completeness), he did not prove the same for its negation (which would imply ). Instead, we recovered Paulson’s \(\mathcal {IT}_ {1}\) as an instance of our Theorem 24 (which requires classical logic).

There are two further improvements that we could perform to Paulson’s formalization, leveraging our abstract results: (1) replacing the soundness assumption from Paulson’s \(\mathcal {IT}_ {1}\) with consistency, and (2) removing all traces of classical reasoning in the object logic to port Paulson’s \(\mathcal {IT}_ {1}\) and \(\mathcal {IT}_{2}\) to intuitionistic logic. For the first improvement, we must prove the aforementioned missing link between Paulson’s \(\mathcal {IT}_ {1}\) and our Theorem 18, namely showing that holds in Paulson’s setting; we are confident that this is true (any reasonable proof-of relation is a \(\varDelta _1\)-formula, implying that its negation is a \(\varSigma _1\)-formula), but the proof will be very laborious. The second improvement will have a large formal overlap with the first: To remove the uses of the unrestricted Excluded Middle axiom, we must prove that instances of this axiom hold intuitionistically for several formulas expressing decidable predicates, including many predicates that participate in the definition of Paulson’s \({\mathsf {Pf}}\), as well as \({\mathsf {Pf}}\) itself; and, in the presence of , we have that is equivalent to Excluded Middle holding for \({\mathsf {Pf}}(n,\langle \varphi \rangle )\).

9.3 Connection to Results Mechanized in Other Provers

Shankar’s 1986 development. In pioneering work [52, 53], Shankar proved formally the proof-theoretic version of \(\mathcal {IT}_ {1}\) for any finite extension of the FOL theory Z2 [10], i.e., he proved Z2’s finitary essential incompleteness. Z2 is a variation of HF set theory, the difference between the two being that the latter postulates an induction principle for all the HF sets, whereas the former singles out the natural numbers as those transitive HF sets that are totally ordered by membership and postulates induction for numbers only. The underlying object logic considered by Shankar was classical FOL enriched with definitions by the Skolemization of any proved “exists unique” sentences. He worked in Thm, an early version of the Boyer–Moore prover that eventually evolved into Nqthm [6] and then ACL2 [26]. This prover’s logic, i.e., the meta-logic of Shankar’s development, is a quantifier-free FOL enriched with induction and recursion principles for reasoning about total functions expressed in pure Lisp. This is significantly less expressive than HOL, and in fact close to primitive recursive arithmetic (PRA). Formally proving \(\mathcal {IT}_ {1}\) within the constraints of this minimalistic meta-logic was an impressive achievement even by today’s standards.

Shankar’s development follows a similar structure to Cohen’s high-level informal presentation [10, §9] (which Shankar cites). He proved that all partial recursive functions are representable in Z2, a result we will refer to as \(\mathcal {RR}\). Besides being a central result in itself, \(\mathcal {RR}\) is a convenient tool for proving Gödel’s theorems. Some proof developments for \(\mathcal {IT}_ {1}\), including the Świerczkowski-Paulson one, do not prove \(\mathcal {RR}\) in its generality, but prove the representability of needed functions only. On the other hand, the \(\mathcal {RR}\) route is usually the one preferred in textbooks due to its elegance and generality. As Shankar observed, textbook proofs of \(\mathcal {IT}_ {1}\) via \(\mathcal {RR}\) often step from the meta-logic (where the usual informal mathematical discourse takes place) into a meta-meta-logic: The formula- and proof- manipulating functions needed for \(\mathcal {IT}_ {1}\) are defined (as usual) as meta-level functions, then a meta-meta-level argument is being made that they are recursive, in order to conclude that they are representable. In a mechanization, however, such an argument must stay in the meta-logic. Shankar achieves this by formalizing a pure Lisp interpreter that is able to evaluate any recursive function when taking its description as input. His formulation of \(\mathcal {RR}\) refers to this interpreter, stating that the interpreter’s partial-function behavior (in relational form) is representable in Z2. Each function needed in the proof of \(\mathcal {IT}_ {1}\) is proved to be representable by first showing it to be equivalent to its interpreted version. Special care is required to have these definitions and proofs work in the meta-logic, where all functions must terminate—to that end, the interpreter takes an additional numeric argument representing the maximum allowed size of the computation. Using notations close to the ones in this paper and bypassing the indirection through the interpreter, Shankar’s proof of \(\mathcal {IT}_ {1}\) can be summarized as follows. He defined a partial function \({{\mathsf {THM}}}: {{\mathsf {Sen}}}\rightarrow \{0,1\}\) that, upon an input \(\varphi \), enumerates all the possible proofs and:

• terminates and returns 1 if a proof of \(\varphi \) is found;

• terminates and returns 0 if a proof of \(\lnot \,\varphi \) is found.

In particular, \({{\mathsf {THM}}}\) loops (i.e., is undefined) if neither \(\varphi \) nor \(\lnot \,\varphi \) is provable. Also, if both \(\varphi \) and \(\lnot \,\varphi \) are provable (meaning the considered extension of Z2 is inconsistent), then the output of \({{\mathsf {THM}}}\) depends on whose proof comes first in the enumeration. But regardless of that, it holds that \({{\mathsf {THM}}}(\varphi ) = 1\) implies \(\vdash \varphi \), and \({{\mathsf {THM}}}(\varphi ) = 0\) implies \(\vdash \lnot \,\varphi \).

Let \(\psi \in {{\mathsf {Fmla}}}_1\) be the formula that represents the unary relation \(\{\varphi \in {{\mathsf {Sen}}}\mid {{\mathsf {THM}}}(\varphi \langle \varphi \rangle ) = 1\}\); this is obtained by (i) invoking \(\mathcal {RR}\) to produce a formula \(\chi \in {{\mathsf {Fmla}}}_2\) that represents the graph of the partial function \({{\mathsf {THM}}}\circ {{\mathsf {S}}}\) (where \({{\mathsf {S}}}\) is the self-substitution operator), and (ii) substituting \(\langle 1\rangle \) for \(\chi \)’s second variable. Let \(\textsf {CS}\) be the Cohen–Shankar sentence \(\lnot \,\psi \langle \lnot \,\psi \rangle \).

Now, assume that \(\vdash \textsf {CS}\) or \(\vdash \lnot \,\textsf {CS}\), meaning that \({{\mathsf {THM}}}(\textsf {CS})\) terminates and returns 1 or 0. We have two cases, both of which contradict consistency:

• If \({{\mathsf {THM}}}(\textsf {CS}) = 1\) (i.e., \(({{\mathsf {THM}}}\circ {{\mathsf {S}}}) (\lnot \, \psi ) = 1\)), then we have \(\vdash \lnot \,\psi \langle \lnot \,\psi \rangle \) by \({{\mathsf {THM}}}\)’s definition, and also \(\vdash \psi \langle \lnot \,\psi \rangle \) by \(({{\mathsf {THM}}}\circ {{\mathsf {S}}})\)’s representability.

• If \({{\mathsf {THM}}}(\textsf {CS}) = 0\) (hence \(({{\mathsf {THM}}}\circ {{\mathsf {S}}}) (\lnot \, \psi ) \not = 1\)), then we have \(\vdash \lnot \,\lnot \,\psi \langle \lnot \,\psi \rangle \) by \({{\mathsf {THM}}}\)’s definition, and also \(\vdash \lnot \,\psi \langle \lnot \,\psi \rangle \) by \(({{\mathsf {THM}}}\circ {{\mathsf {S}}})\)’s representability.

The above proof, which is similar to Cohen’s proof sketch,^{Footnote 6} does not make explicit reference to HBL \(_{1}\), although this is of course a consequence of \(\mathcal {RR}\) via the representability of the “proof of” relation. In fact, the proof makes use of the representability of \({{\mathsf {THM}}}\circ {{\mathsf {S}}}\), which is a variation of the representability of \(\vdash \) (for particular sentences of the form \(\varphi \langle \varphi \rangle \)) featuring a positive version of the Rosser twist discussed in Sect. 5, but at the meta-level: The considered relation is not just provability, but provability by a proof p such that there is no proof q of the formula’s negation occurring earlier in the enumeration.

The above argument is based on the diagonalization, though at the meta-level not at the object level as in Proposition 9. As Shankar remarked, the sentence \(\textsf {CS}\) says “my negation is provable by a proof that comes in the enumeration before any proof of me”. This is true in the context of the above argument by contradiction, namely under the assumption that \(\textsf {CS}\) is decided (either provable or unprovable). Indeed, from the definitions of \(\psi \) and \({{\mathsf {THM}}}\), we see that \(\textsf {CS}\) says “it is not the case that a proof of \(\textsf {CS}\) comes before a proof of \(\lnot \,\textsf {CS}\)”, which, given the assumption, is equivalent to the above.

Let us refer to such sentence \(\textsf {CS}\) as Cohen-Shankar sentences (without claiming historical accuracy about the ideas behind them, which seem to go back at least as far as Smullyan [59]). They can alternatively be obtained by diagonalization in the object logic, namely using Proposition 9 and Repr \(_\lnot \) to find \(\textsf {CS}\) such that , where < is the representation of the occurrence order in the enumeration of proofs used in \({{\mathsf {THM}}}\)’s definition. While classically a Cohen–Shankar sentence is essentially the negation of a Rosser sentence, intuitionistically this is not the case. However, \(\textsf {CS}\) can replace the Rosser sentence in our proof-theoretic Rosser-style \(\mathcal {IT}_ {1}\), covered by Propositions  14, 15 and Theorem 16. Indeed, a bit of mining reveals that the proofs of these results are sufficiently general to accommodate both types of sentences. Given any \(\varphi _1\) and \(\varphi _2\), let us define the one-variable formula \({\textsf {Twist}}_{\varphi _1,\varphi _2}(x)\) to be . Note that, in the presence of Repr \(_\lnot \) , we have that (i) \(\vdash {\textsf {R}}\mathrel {\;\leftarrow \rightarrow \;}\lnot \, {\textsf {Twist}}_{{\textsf {R}},\lnot \,{\textsf {R}}}\) for all Rosser sentences \({\textsf {R}}\), and (ii) \(\vdash \textsf {CS}\mathrel {\;\leftarrow \rightarrow \;}{\textsf {Twist}}_{\lnot \,\textsf {CS},\textsf {CS}}\) for all Cohen–Shankar sentences \(\textsf {CS}\). Based on this observation, we can amend the proofs of Propositions 14 and 15 by simply replacing \(\lnot \,{\textsf {R}}\) with \(\textsf {CS}\) and \({\textsf {R}}\) with \(\lnot \,\textsf {CS}\), and using (ii) instead of (i). Let us illustrate this on the crucial point (5) in Proposition 14’s proof, establishing that \(\vdash \forall x. \,\lnot \,{\textsf {Twist}}_{{\textsf {R}},\lnot \,{\textsf {R}}}(x)\), which is used to infer \(\vdash \lnot \,(\exists x.\,{\textsf {Twist}}_{{\textsf {R}},\lnot \,{\textsf {R}}}(x))\), hence (by (i)) \(\vdash {\textsf {R}}\), leading to a contradiction with the \(\vdash \lnot \,{\textsf {R}}\) assumption. After the replacement, point (5) establishes that \(\vdash \forall x.\, \lnot \,{\textsf {Twist}}_{\lnot \,\textsf {CS},\textsf {CS}}(x)\), which is used to infer \(\vdash \lnot \,(\exists x. \,{\textsf {Twist}}_{\lnot \,\textsf {CS},\textsf {CS}}(x))\), hence (by (ii)) \(\vdash \lnot \,\textsf {CS}\), leading to a contradiction with the \(\vdash \textsf {CS}\) assumption; and similarly for Proposition 15. Moreover, the proof of our semantic Rosser-style \(\mathcal {IT}_ {1}\) (Theorems 19 and 20) can be straightforwardly adapted to show, under our abstract assumptions, that \(\textsf {CS}\) is false (i.e., \(\lnot \,\textsf {CS}\) is true) in the standard model—a fact also proved by Cohen in his concrete setting. In conclusion, our abstract results can be migrated from Rosser to Cohen–Shankar sentences without requiring classical reasoning in the object logic.

O’Connor’s 2005 development. O’Connor proved formally the proof-theoretic version of \(\mathcal {IT}_ {1}\) [36, 37] for any self-representable extension of a classical FOL theory called NN [23, §7.1], i.e., he proved the essential incompleteness of NN with respect to self-representable extensions. Self-representability of a FOL theory means that its set of axioms is represented by a one-variable formula in that theory. NN is a modification of Robinson arithmetic obtained by replacing the dichotomy axiom ( any element is either 0 or a successor) with three axioms regulating the behavior of an additional binary relation symbol for strict order, namely stating that (i) no element is smaller than 0, (ii) being smaller than the successor of an element implies being smaller than or equal to that element, and (iii) the order is total. NN has a similar (though not comparable) expressiveness to Robinson arithmetic. Like the latter, it is significantly less expressive than Peano arithmetic yet sufficient for \(\mathcal {IT}_ {1}\) (but not for \(\mathcal {IT}_{2}\)).

O’Connor worked in the Coq prover [3], so his meta-logic is Coq’s underlying Calculus of Inductive Constructions [38], an intuitionistic logic based on intensional type theory. Working out \(\mathcal {IT}_ {1}\)’s theorem intuitionistically (though for a classical object logic)^{Footnote 7} was original, and revealed some interesting phenomena.

O’Connor’s development followed the informal presentation from Hodel’s textbook [23], with some notable modifications discussed below. Following Hodel, and similarly to Shankar, he combined a representability theorem for a class of computable functions with proofs that all functions needed for \(\mathcal {IT}_ {1}\) are in this class, hence are representable. However, unlike Hodel and Shankar, O’Connor did not prove representability for all recursive functions (a result we denoted by \(\mathcal {RR}\)), but stopped at the representability of primitive recursive functions—we will refer to this latter result as \(\mathcal {PR}\). This restriction made the proofs that certain functions are in the considered class more difficult—notably, he reported on the difficulty of establishing that substitution is primitive recursive. On the other hand, O’Connor’s formalized representability result is stronger than Shankar’s on the theory expressiveness dimension, since it is proved for the minimalistic theory NN.

O’Connor proved a version of \(\mathcal {IT}_ {1}\) that would classically read as follows: For any consistent self-representable extension of NN, there exists a sentence \(\varphi \) such that neither \(\varphi \) nor \(\lnot \,\varphi \) is provable. Due to the intuitionistic meta-logic, O’Connor preferred the intuitionistically stronger (and classically equivalent) formulation: For any self-representable extension of NN, there exists a sentence \(\varphi \) such that, if \(\varphi \) or \(\lnot \,\varphi \) are provable, then that extension proves everything (i.e., is inconsistent). Another consequence of the intuitionistic meta-logic is the need for an additional assumption: that the given extension’s set of axioms is decidable, i.e., its (meta-level) membership predicate satisfies Excluded Middle.

The above universally quantified \(\varphi \) is witnessed by a Rosser sentence constructed via diagonalizaton, so the result essentially falls under Propositions 9,10 and Theorem 16, where both \(\vdash ^{\textsf {b}}\) and \(\vdash \) are taken to be deduction in a self-representable extension of NN. (Note that all the FOL theories of interest for \(\mathcal {IT}_ {1}\) can already be represented in NN, not only in an extension of NN; and the corresponding (slightly weaker) version of O’Connor’s result assuming NN-representability instead of self-representability is obtained by taking \(\vdash ^{\textsf {b}}\) to be deduction in NN and \(\vdash \) to be deduction in the considered extension.)

Since here the FOL infrastructure is fixed, self-representability is equivalent to representability of the “proof of” relation (which O’Connor proved), hence it implies HBL \(_{1}\) (which he did not mention explicitly but inlined in his proof). Incidentally, O’Connor’s formalization improves on Hodel’s account, who unnecessarily added an axiom to NN for coping with Rosser’s trick [37, §6.4].

O’Connor’s self-representability assumption in \(\mathcal {IT}_ {1}\) is more general than the standard recursive axiomatizability assumption. In informal accounts of essential incompleteness including Hodel’s, this more general result is usually inlined in the proof and only the end result is stated, which assumes not self-representability but recursive axiomatizability; an exception is the account of Feferman, who assumes a generalized form of self-representability (namely representability in a sub-theory) in his statements of \(\mathcal {IT}_ {0.5}\) and \(\mathcal {IT}_{2}\) (Theorems 5.3 and 5.6 in [13]). In a formal account, such more general results are valuable for easier reusability across different instances.

O’Connor did not prove that all recursively axiomatizable extensions of NN are self-representable (which would have followed from \(\mathcal {RR}\)). However, he used his \(\mathcal {PR}\) together with a proof that Peano arithmetic has its axioms primitively recursive to instantiate \(\mathcal {IT}_ {1}\) to Peano arithmetic. He also proved the consistency of this theory (by showing that the natural numbers form a model, via a semantic interpretation function wrapped up in a negative translation to ensure classical validity within the intuitionistic meta-logic). Thus, he obtained the theory’s unconditional incompleteness.

Harrison’s 2009-2010 development. Harrison [21] proved formally versions of \(\mathcal {IT}_ {1}\) for theories in the language of Robinson arithmetic with \(\le \) and < included as primitive predicate symbols. In what follows, we will refer to this language as \(\mathcal {LA}\), and by “Robinson arithmetic” we will mean the definitional extension of Robinson arithmetic as a theory in \(\mathcal {LA}\) (with added axioms that define \(\le \) and <). Harrison worked in HOL Light [20], a proof assistant belonging to the HOL family together with Isabelle/HOL and HOL4.

In his development towards \(\mathcal {IT}_ {1}\), Harrison followed a semantic approach, based on ideas that go back to Gödel’s introduction of his original paper [17]. The approach was promoted by Smullyan [60] for its simplicity and elegance, and Harrison himself further elaborated and improved on it in his textbook [19, §7]. The focus is no longer on the concept of a relation’s representability (for a given theory), but on that of a relation’s definability in the standard model (for a given language). In our notations, definability is obtained by replacing \(\vdash ^{\textsf {b}}\) with \(\models \) in either the representability or the weak representabilty condition.^{Footnote 8} (Harrison formalized an equivalent definition of definability using valuations in the model.) The advantage of definability over representability is that the former is typically much easier to prove for concrete relations, without having to work inside a formal proof system.

\(\mathcal {LA}\) is sufficient to achieve the definability (in the standard model of natural numbers) of the relevant syntactic concepts. These include (soft) self-substitution, which gives a semantic version of diagonalization: Proposition 9 with \(\vdash ^{\textsf {b}}\) replaced by \(\models \). In turn, this leads to the semantic version of Tarski’s theorem on the undefinability of truth, which concludes the non-existence of a one-variable formula \({{\mathsf {T}}}\) such that \(\models \varphi {\mathrel {\;\leftarrow \rightarrow \;}} {{\mathsf {T}}}\langle \varphi \rangle \) for all \(\varphi \). And after showing that provability in Robinson arithmetic is definable, one obtains that provability is distinct from truth; in particular, for sound theories this implies the incompleteness of provability, a first version of the proof-theoretic \(\mathcal {IT}_ {1}\). In fact, Harrison proved something more general: If a theory T in \(\mathcal {LA}\) is definable (in that its set of axioms is definable), then its set of provable sentences is definable, hence different from the set of true sentences. This leads to a form of essential incompleteness: Any sound definable theory in \(\mathcal {LA}\), in particular, any extension of Robinson arithmetic with a sound definable set of axioms, is incomplete.

Harrison also pursued an alternative semantic route to \(\mathcal {IT}_ {1}\), which does not go through Tarski’s theorem, but instead: (1) assumes (for starters) the soundness of the theory, (2) obtains a semantic version of Gödel sentences \({\textsf {G}}\) using the semantic diagonal lemma, and (3) performs (what can be regarded as) a modification of the Gödel’s original argument (the proofs of Propositions 11 and 12), appealing to soundness whenever needed for shifting from provability to truth. The advantage of this last line of reasoning is that it can be sharpened: Noting that soundness is only needed for \({\textsf {G}}\), \(\lnot \,{\textsf {G}}\) and \(\bot \), and using the fact that \({\textsf {G}}\) is a \(\varPi _1\)-sentence (making \(\lnot \,{\textsf {G}}\) a \(\varSigma _1\)-sentence) if the theory is \(\varSigma _1\)-definable (i.e., definable by a \(\varSigma _1\)-formula), Harrison obtained the following stronger, symmetric version of proof-theoretic \(\mathcal {IT}_ {1}\): If a theory in \(\mathcal {LA}\) is \(\varSigma _1\)-definable, then (i) if it also \(\varPi _1\)-sound then \(\not \vdash {\textsf {G}}\) and (ii) if it also \(\varSigma _1\)-sound then \(\not \vdash \lnot \,{\textsf {G}}\) (where \(\vdash \) denotes deduction from this theory, and X-soundness or X-completeness means soundness or completeness for all X-sentences). And from representability and the semantic Gödel-sentence property, under the assumptions of (i), it follows that \(\models {\textsf {G}}\). So he obtained both the proof-theoretic and the semantic component of \(\mathcal {IT}_ {1}\).

In the above statement of \(\mathcal {IT}_ {1}\), the \(\varPi _1\)-soundness assumption can be replaced by consistency plus \(\varSigma _1\)-completeness, since the latter two imply the former. Finally, using the \(\varSigma _1\)-completeness for Robinson arithmetic (and hence for any extension), Harrison formalized an essential incompleteness generalization and strengthening of the original Gödel-style \(\mathcal {IT}_ {1}\): For any consistent \(\varSigma _1\)-definable extension of Robinson arithmetic, we have \(\not \vdash {\textsf {G}}\) and \(\models {\textsf {G}}\); and if the extension is also \(\varSigma _1\)-sound, then \(\not \vdash \lnot \,{\textsf {G}}\). In the presence of \(\varSigma _1\)-completeness, the \(\varSigma _1\)-soundness property (also called 1-consistency) is weaker than the \(\omega \)-consistency property used originally by Gödel, which we assume in our Proposition 12 and Theorem 13.

Currently, refinements of \(\mathcal {IT}_ {1}\) based on arithmetical hierarchy considerations are below the level of abstraction of our general framework. On the other hand, the high-level aspects of the Smullyan–Harrison semantic line of reasoning could be incorporated in this framework, which has infrastructure for both provability and truth. Our Archive of Formal Proofs entry [44] already contains proof-theoretic and semantic versions of Tarski’s theorem.

9.4 Other Potential Instances

Many other logics and logical theories satisfy our theorems’ assumptions. We do not require the logic to be reducible to a single syntactic category of formulas, \({{\mathsf {Fmla}}}\), a single pair of judgments, \(\vdash ^{\textsf {b}}\) and \(\vdash \), etc.; but only that such (well-behaved) formulas, provability relations, etc. are identifiable as part of that logic, e.g., localized to a given type and/or relativised by a given predicate. This allows our framework to capture most variants of higher-order logic and type theory (including the variant underlying Isabelle/HOL itself [29, 30]), and also, we believe, many of the logics surveyed by Buldt [7], including non-classical and fuzzy. But enabling “mass instantiation” that is both formal and painless requires more progress on the agenda we started here: recognizing reusable construction and proof patterns and formalizing them as abstract results.