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

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 \(\_ [\_/\_]\): In addition, for the operators on formulas we assume the following: 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.

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: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]: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:

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}\) 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:

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\):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:

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}}}\).

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]: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}\):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 :

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: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 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: 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}}\):

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 :

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

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

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.

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.

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:

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

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 \):

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.

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

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:

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

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:

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.

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 \):

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 }}\):

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:

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.

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}}\)).

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.

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}\):

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}\):

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

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.

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: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 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}\).

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:

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:

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.²\(^{,}\)³ 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: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 ofwhich, in the presence of HBL \(_{1}\), is seen to be a weak form of HBL \(_{2}\).⁴ This motivates the name “WHBL \(_2\)”. We are led to the following solution:

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:(In concrete logics, the elements of \({{\mathsf {Ops}}}\) can be constructors or derived operators on terms.)

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}\) has a similar flavor as HBL \(_{2}\), but refers to conjunction rather than implication: It states that conjunction introduction holds inside the proof system.

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

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

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:

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

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: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:The above proof, which is similar to Cohen’s proof sketch,⁶ 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)⁷ 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.⁸ (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.

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.