2.1 Syntax

Let us work with the basic language of arithmetic $\mathcal {L}$ whose alphabet A consists of non-logical symbols $\{ \mathsf {0}, \mathsf {s}, +, \times \}$ and of logical symbols $\{ \mathsf {v},^{\prime } , \bot , =, \rightarrow , \forall \}$ .Footnote ⁵ The sets of expressions of $\mathcal {L}$ (i.e., the variables, terms, and formulas) are defined inductively over a background universe by an implementation.

The most common background universe is a universe of strings [Reference Avigad1, Reference Boolos, Burgess and Jeffrey6, Reference Enderton17, Reference Gödel25], but other options serve equally well, for example, labelled trees [Reference van Dalen15, Reference Feferman, Ferro, Bonotto, Valentini and Zanardo20], sets [Reference Fitting23, Reference Manin52, Reference Świerczkowski74], numbers [Reference Feferman18, Reference Hájek and Pudlák36], or two-dimensional strings [Reference Halbach and Leigh38]. Before presenting the more general framework, let us define two common examples of implementations on universes of strings. For the Kleene star $A^\ast $ , that is, the set of all finite strings from A, the usual prefix (or Polish) implementation $\textsf {pre}$ on $A^\ast $ defines the set of $\textsf {pre}$ -expressions as follows:

$$ \begin{align*} x & := \mathsf{v} \mid^{\prime}\!\!{x} \\t & := ~ x \mid \mathsf{0} \mid \mathsf{s}\,t \mid +\,t\,t \mid \times\,t\,t \\\varphi & := ~ \bot \mid\, =\!t\,t \mid\, \rightarrow\!\varphi\,\varphi \mid ~\forall x\,\varphi. \end{align*} $$

In this framework, the auxiliary symbols (such as commas or brackets) are part of the background universe. Thus, the standard infix implementation $\textsf {inf}$ defines the set of $\textsf {inf}$ -expressions on the Kleene star on $A \cup \{),(\}$ as follows:

$$ \begin{align*} x & := ~\mathsf{v} \mid^{\prime}{\!\!x} \\ t & := ~x \mid \mathsf{0} \mid \mathsf{s}\,t \mid (t+t) \mid (t\times t) \\ \varphi & := ~ \bot \mid (t=t) \mid (\varphi \rightarrow \varphi) \mid \forall x \, \varphi. \end{align*} $$

More generally, given a background universe U, the sets of $\imath $ -variables, $\imath $ -terms, and $\imath $ -formulas are defined inductively by the following $\imath $ -constructor functions:

$$ \begin{align*} \begin{aligned} \mathsf{v}_\imath \colon & \mathrm{Var}_\imath^0 \to \mathrm{Var}_\imath & {\, }^{\prime}_\imath \colon & \mathrm{Var}_\imath \to \mathrm{Var}_\imath \\ \mathsf{0}_\imath \colon & \mathrm{Ter}_\imath^0 \to \mathrm{Ter}_\imath & \mathsf{s}_\imath \colon & \mathrm{Ter}_\imath \to \mathrm{Ter}_\imath \\ +_\imath \colon & \mathrm{Ter}_\imath^2 \to \mathrm{Ter}_\imath & \times_\imath \colon & \mathrm{Ter}_\imath^2 \to \mathrm{Ter}_\imath \\ \bot_\imath \colon & \mathrm{Fml}_\imath^0 \to \mathrm{Fml}_\imath & =_\imath \colon & \mathrm{Ter}_\imath^2 \to \mathrm{Fml}_\imath \\ \rightarrow_\imath \colon & \mathrm{Fml}_\imath^2 \to \mathrm{Fml}_\imath & \forall_\imath \colon & \mathrm{Var}_\imath \times \mathrm{Fml}_\imath \to \mathrm{Fml}_\imath. \end{aligned} \end{align*} $$

The various $\imath $ -constructor functions are defined by operations on U. For instance, $^{\prime }_{\mathsf {pre}}$ is defined by $x \mapsto ^{\prime }\!\! {{}^\smallfrown } x$ , where ${{}^\smallfrown }$ denotes the operation of concatenation. The set of $\textsf {pre}$ -variables is then the smallest set closed under $\mathsf {v}_{\mathsf {pre}}$ and $^{\prime }_{\mathsf {pre}}$ (see, e.g., [Reference Avigad1, chap. 1] on inductively defined sets). The set of $\imath $ -expressions $\mathrm {Exp}_\imath $ on U is defined as $\mathrm {Var}_\imath \cup \mathrm {Ter}_\imath \cup \mathrm {Fml}_\imath \subseteq U$ . For simplicity, we use an implementation $\imath $ to denote the collection of all $\imath $ -constructor functions, and say that $\mathrm {Exp}_\imath $ is defined by $\imath $ . More details and some motivation are given in §5.2 and Appendix A.

In this article, I consider only implementations $\imath $ that satisfy the following two conditions. First, each variable is a term and no term is a formula; thus, $\mathrm {Var}_\imath \subseteq \mathrm {Ter}_\imath $ and $\mathrm {Ter}_\imath \cap \mathrm {Fml}_\imath = \emptyset $ . Second, the basic syntactic relations (e.g., being free in, being a sentence, etc.) are defined by recursion. This requires recursion theorems for each of the sets $\mathrm {Var}_\imath , \mathrm {Ter}_\imath $ , and $\mathrm {Fml}_\imath $ . Since such theorems hold in general for every inductively and freely generated set, it suffices for our syntactic sets to be inductively and freely generated (see, e.g., [Reference Avigad1, pp. 16–17] or [Reference Humberstone44, sec. 0.24]). This amounts to considering only those implementations $\imath $ for which the $\imath $ -constructor functions are injective and their ranges pairwise disjoint.Footnote ⁶

2.2 Gödel numberings

Over the set of non-negative integers $\omega $ , we define numberings as follows.

We say that $\alpha (b)$ is the $\alpha $ -code of b, and that the range $\alpha (B)$ of $\alpha $ is the set of $\alpha $ -codes. For an implementation $\imath $ , a Gödel numbering on $\imath $ is a numbering of B where each $\imath $ -expression has an $\alpha $ -code, that is, $\mathrm {Exp}_\imath \subseteq B$ . When the context is clear, I simply use ‘numbering’ as shorthand for ‘Gödel numbering on $\imath $ ’.

A tracking function is used to track, at the level of numbers, a given function on an encoded set.

Definition 2 ( $\alpha $ -tracking functions).

For a numbering $\alpha $ of B and any partial k-ary function $f\colon B^k \to B$ , an $\alpha $ -tracking function of f is a partial k-ary function ${f^{\alpha } \colon \omega ^k \to \omega }$ such that

$$\begin{align*}f^\alpha (n_0, \dots , n_{k-1}) = \alpha ( f (\alpha^{-1}(n_0), \dots , \alpha^{-1}(n_{k-1})) ), \end{align*}$$

whenever $f(\alpha ^{-1}(n_0), \dots , \alpha ^{-1}(n_{k-1}))$ is defined.

Let us consider an example of a numbering $\alpha $ on $\mathsf {pre}$ . An $\alpha $ -tracking function of the $\mathsf {pre}$ -constructor function $\rightarrow _{\mathsf {pre}}$ can be defined by $ x,y \mapsto \alpha (\rightarrow _{\mathsf {pre}} \! (\alpha ^{-1}(x),\alpha ^{-1}(y)))$ and then the following diagram commutes:

where $\alpha \! \times \! \alpha \, (x,y) := \langle \alpha (x), \alpha (y) \rangle $ . Thus, we have $\rightarrow ^\alpha _{\mathsf {pre}} \! (\alpha (\varphi ),\alpha (\psi )) = \alpha (\rightarrow \!\varphi \,\psi )$ , which tracks the constructor function $\rightarrow _{\mathsf {pre}}$ at the level of the $\alpha $ -codes.

Finally, to compare numberings, we use a notion of equivalence between numberings. For our purposes, it suffices to define equivalence relative to the class of recursive functions $\mathbb {REC}$ .Footnote ⁷

Roughly, two numberings $\alpha $ and $\beta $ of B are equivalent if, for each $b \in B$ , we can translate (in a computable way) the $\alpha $ -code of b into the $\beta $ -code of b and vice versa.

3.1 Standard numberings

The most common numberings in the literature are the string numberings. These numberings assign a code to each string of $A^\ast $ thanks to some basic code and some coding of finite sequences of positive integers. A basic code of the alphabet A is a function $\# \colon A \to \omega \setminus \{0\}$ . For definiteness, let $\#(\mathsf{v}) = 1, \#(^{\prime }) = 2, \ldots, \#(\forall) = 10$ , and let $s \equiv s_0 {{}^\smallfrown } s_1 {{}^\smallfrown } \ldots {{}^\smallfrown } s_{n-1}$ with $n> 0$ and $s_i \in A$ , where $\equiv$ denotes identity of strings. Different basic codes and sequential codings yield different string numberings (see [Reference Cegielski and Richard11]). Below, two most common numberings are presented.

The first numbering $\mathsf {gn}_1$ was introduced by Gödel [Reference Gödel25] and is still used in many textbooks (e.g., [Reference Manin52, Reference Rautenberg69, Reference Smith72]). Relying on the fundamental theorem of arithmetic, it is defined as follows:

$$\begin{align*}\mathsf{gn}_1 (s) = \pi_0^{\# (s_0)} \cdot \pi_1^{\# (s_1)} \cdot \ldots \cdot \pi_{n-1}^{\# (s_{n-1})} = \prod_{i=0}^{n-1} \pi_{i}^{\# (s_i)}, \end{align*}$$

where $\pi _i$ denotes the $(i+1)$ th prime number. A common variant is to encode n, the length of s, as the first term of the encoded sequence (see, e.g., [Reference Odifreddi61]).

Introduced by Smullyan [Reference Smullyan73], the second numbering $\mathsf {gn}_2$ is commonly used in the study of weak arithmetics (e.g., [Reference Visser80, Reference Wilkie and Paris82]). For some (often prime) number $b \geq \max (\#(A))$ , it employs the base-b representation of numbers:

$$\begin{align*}\mathsf{gn}_2 (s) = \#(s_{0})\cdot b^{0} + \#(s_{1})\cdot b^{1} + \cdots + \#(s_{n-1})\cdot b^{n-1} = \sum_{i=0}^{n-1} \#(s_i) \cdot b^{i}. \end{align*}$$

The length-first lexicographic (or shortlex) numbering is a special case of this numbering, in our case with $b = 10$ .

Another common way to define numberings in the literature does not focus on strings, but on the syntactic expressions and their generation. Introduced by Hilbert and Bernays [Reference Hilbert and Bernays43], such compositional numberings are often preferred when the syntax is not defined on a universe of strings (e.g., [Reference Avigad1, Reference van Dalen15, Reference Feferman18, Reference Kleene47]).

The third numbering $\mathsf {gn}_3$ is defined recursively on $\mathrm {Var}_{\mathsf {pre}}, \mathrm {Ter}_{\mathsf {pre}}$ , and $\mathrm {Fml}_{\mathsf {pre}}$ as follows: For some sequential coding $\langle \cdot \rangle $ and $x \in \mathrm {Var}_{\mathsf {pre}}$ ,

$$\begin{align*}\mathsf{gn}_3 (\mathsf{v}) = \langle \#(\mathsf{v}) \rangle \text{ with } \mathsf{gn}_3(^{\prime} x) = \langle \#(^{\prime}), \mathsf{gn}_3 (x) \rangle, \end{align*}$$

for $s,t \in \mathrm {Ter}_{\mathsf {pre}}$ ,

$$\begin{align*}\mathsf{gn}_3 (\mathsf{0}) = \langle \#(\mathsf{0}) \rangle \text{ with } \mathsf{gn}_3 (\mathsf{s}\,t) = \langle \#(\mathsf{s}), \mathsf{gn}_3 (t) \rangle, \end{align*}$$

$$\begin{align*}\mathsf{gn}_3 (+\,s\,t) = \langle \#(\mathsf{+}), \mathsf{gn}_3 (s), \mathsf{gn}_3 (t) \rangle \text{, and } \mathsf{gn}_3 (\times\,s\,t) = \langle \#(\times), \mathsf{gn}_3 (s), \mathsf{gn}_3 (t) \rangle \end{align*}$$

and similarly for the formulas. Other definitions not using a sequential coding are also available, as it suffices, for all clauses, to take injective functions whose ranges are pairwise disjoint (see, e.g., [Reference Hilbert and Bernays43, pp. 216–218]).Footnote ⁹

It is clear that the standard numberings $\mathsf {gn}_{1,2,3}$ , as well as most numberings found in the literature, are intuitively reasonable. Indeed, it is difficult to see what could go wrong with any of them. However, the reasonableness of a numbering also depends on the choice of base theory. This dependence becomes particularly apparent in weak theories of arithmetic, although it is not limited to such theories.

Consider, for instance, the set of $\mathsf {gn}_1$ -codes of the terms. Such a set can be arithmetised by the standard $\Sigma _1$ -formula $\mathsf {term}(x)$ that mimics a definition of the terms, that is, x is the $\mathsf {gn}_1$ -code of a term iff “there exists a construction sequence for terms which ends with x.” Any theory T extending $\textsf {Q}$ binumerates such a set with $\mathsf {term}(x)$ , however not all of them prove the basic properties of the terms with $\mathsf {term}(x)$ (see, e.g., [Reference Hájek and Pudlák36, p. 312]). For example, $\textsf {I}\Sigma _1$ already proves them with $\mathsf {term}(x)$ using its induction on $\Sigma _1$ -formulas. But what about weaker theories without induction on $\Sigma _1$ -formulas?

The answer depends on whether $\mathsf {term}(x)$ can be proved to be equivalent to a formula of lower complexity, which requires bounding the initial existential quantifier. Under $\mathsf {gn}_1$ , the code of such a construction sequence is bounded by an exponential in x. Thus, the theory $\textsf {EA}$ , whose language has a symbol of exponentiation, can prove basic properties of the terms with existentially bounded $\mathsf {term}(x)$ , making it $\Delta _0(\mathsf {exp})$ . However, the same bounding argument is unavailable in $\mathsf I\Delta _0$ (or even $\textsf {I} \Delta _0 + \Omega _n$ ), which is formulated in the basic language of arithmetic and does not prove the totality of exponentiation. (If the set of $\mathsf {gn}_1$ -codes of terms does not belong to the linear time hierarchy, then $\mathsf I\Delta _0$ does not $\Delta _0$ -binumerate it, see [Reference Cook and Nguyen14, chap. III.4].)

This is a defect of the combination of the choices of numbering and base theory, not of $\textsf {I}\Delta _0$ itself. Indeed, by choosing a more efficient numbering, $\textsf {I}\Delta _0$ can prove the basic properties of the terms [Reference Hájek and Pudlák36, chap. V.3]. (See also [Reference Wilkie and Paris82] on $\mathsf {gn}_2$ and its interaction with $\textsf {I} \Delta _0 + \Omega _n$ .) I return to these issues below. For now, let us turn to more problematic and philosophically significant cases of numberings.

3.2 Characteristic numberings

Another type of numbering is the characteristic numbering which encodes not only its domain but also additional information about that domain—typically, the characteristic function of some subset of its domain. Such numberings are similar in many respects to deviant notations in the philosophy of computation.Footnote ¹⁰

The fourth numbering $\mathsf {gn}_4$ is defined following Grabmayr [Reference Grabmayr29, p. 55]: For $X\subseteq A^\ast $ such that both X and $A^\ast \setminus X$ are infinite, let $(\eta _i)_{i\in \omega }$ and $(\theta _i)_{i\in \omega }$ be, respectively, enumerations without repetitions of X and $A^\ast \setminus X$ . Then, let

$$\begin{align*}\mathsf{gn}_4(s)= \begin{cases} 2i & \text{ if } s \equiv \eta_i \in X \\ 2i + 1 & \text{ if } s \equiv \theta_i \in A^\ast \setminus X. \end{cases} \end{align*}$$

Hence, whether or not s is an element of X depends on whether the $\mathsf {gn}_4$ -code of s is even. This definition also generalises, with some additional coding, to any n-ary relation on $A^\ast $ .

It is then straightforward to construct counterexamples to many metamathematical theorems using such characteristic numberings. To extend our sketch in §1, let X be the set of T-provable sentences. By the standard $\Delta _0$ -binumeration $\mathsf {even}(x)$ of the set of even numbers, T binumerates X and therefore its own provability. It is easy to see that $\mathsf {even}(x)$ fulfils all Löb’s conditions with respect to such a $\mathsf {gn}_4$ , but $T \vdash \neg \mathsf {even}(\overline {\mathsf {gn}_4 (\bot )})$ . Indeed, if T is consistent, then $\bot $ is not provable in T and so, by definition, $\mathsf {gn}_4(\bot )$ is odd. Thus, we obtain a version of $\textsf {G}2$ with Löb’s conditions that fails for T (note that, in this case, the diagonal lemma has to fail [Reference Grabmayr29, p. 55]). Clearly, $\mathsf {gn}_4$ is not a reasonable choice (at least with T).

Nonetheless, not all characteristic numberings appear unreasonable. For instance, allowing X to be the whole (or empty) domain with $(\eta _i)_{i\in \omega }$ (or $(\theta _i)_{i\in \omega }$ ) given by $\mathsf {gn}_1$ , the resulting numberings are essentially just $\mathsf {gn}_1$ . More interesting and difficult cases come with non-trivial choices of X. Let X be the set of terms $\mathrm {Ter}_{\mathsf {pre}}$ and consider its characteristic numbering (with some effective enumerations). Working in $\textsf {PA}$ , we then have a straightforward $\Delta _0$ -binumeration of the terms with $\mathsf {even}(x)$ . However, in $\textsf {PA}$ , this binumeration does not seem to have any substantive advantage over the standard one with $\mathsf {gn}_1$ . A similar phenomenon arises if we take X to be the set of $\textsf {I} \Sigma _1$ -provable sentences and work in $\textsf {PA}$ . Trivially, with such a numbering, $\textsf {PA}$ proves a consistency statement for $\textsf {I}\Sigma _1$ , but also with $\mathsf {gn}_1$ (though with much more work and not with the same statement). Still, these last two $\mathsf {gn}_4$ seem mainly to be mathematical tricks, which happen to have no (obvious) dire consequences.

3.3 Self-referential numberings

The last type of numberings considered here are self-referential numberings. Both Kripke [Reference Kripke48, fn. 6] and Feferman [Reference Feferman19, p. 80] suggested defining numberings in such a way as to obtain a Gödel sentence directly from the numbering. This idea was later generalised to construct numberings with this self-referential property for all formulas with one free variable (see [Reference Halbach and Visser40, Reference Heck41, Reference Kripke49, Reference Visser, Gabbay and Guenthner76], and Reference Grabmayr and Visser34 for an extensive study).

The fifth numbering $\mathsf {gn}_5$ is defined following Visser [Reference Visser, Gabbay and Guenthner76, pp. 159–160]: Let $(\theta _i)_{i\in \omega }$ be an enumeration of the Kleene star on $A \cup \{\mathsf {c}\}$ , where $\mathsf {c}$ is a fresh constant. We define $(\delta _i)_{i\in \omega }$ as an enumeration of $A^\ast $ (without $\mathsf {c}$ ) from $(\theta _i)_{i\in \omega }$ by substituting, the standard numeral of $i, \overline{i}$ , for every occurrence of $\mathsf {c}$ in each $\theta_i$ . Thus, $\delta _i \equiv \theta _i [\mathsf {c}:= \overline {i}]$ and $\mathsf {gn}_5$ is defined as followsFootnote ¹¹ :

$$\begin{align*}\mathsf{gn}_5(s) = \min\{n \mid \delta_n \equiv s\}. \end{align*}$$

Using such self-referential numberings, the diagonal lemma becomes a triviality. Indeed, for any formula $\varphi (x)$ , there is an i such that

$$\begin{align*}\mathsf{gn}_5(\varphi(\overline{i})) = \min\{n \mid \varphi(\overline{i}) \equiv \delta_n \equiv \theta_n [\mathsf{c}:= \overline{i}] \} = i. \end{align*}$$

Trivially, $T \vdash \overline {\mathsf {gn}_5(\varphi (\overline {i}))} = \overline {i}$ (the strong diagonal lemma), from which the diagonal lemma follows.

As with the preceding examples, such self-referential numberings appear to be a more elaborate version of the characteristic numbering, where the diagonalisation takes place in the construction of the numbering rather than in the theory. Again, this mathematical trick seems to have no dire consequences.Footnote ¹²

Should we therefore regard these as reasonable numberings? It is unclear to me whether such self-referential numberings should be considered reasonable. As pointed out by a reviewer, self-referential numberings might play an important role in certain contexts with weak theories of arithmetic (see, e.g., the remarks in [Reference Kurahashi and Visser50, sec. 6.2]). Although this has not yet been carefully studied, it may count in favour of their reasonableness. On the other hand, these numberings directly affect the consistency of some basic untyped truth theories (see [Reference Heck41, sec. 3] and [Reference Schindler71, sec. 2.2]). In particular, such theories become inconsistent when self-referential numberings are used, while remaining consistent with standard numberings, such as $\mathsf {gn}_1$ (see also [Reference Grabmayr and Visser34, sec. 9]). This may seem an unwelcome consequence for the class of reasonable numberings, and therefore favour understanding them as unreasonable.

4.1 Resemblance criterion

The resemblance criterion is a natural and intuitive criterion that is widely, though often tacitly, used in metamathematics. Consider a relation and its usual description in a metalanguage. To arithmetise this relation, that is, define an arithmetical formula that represents it, a natural requirement is to ask for this formula to resemble its description.

• Resemblance criterion. For a relation R and a description of R, a formula $\varphi $ is a reasonable representation of R iff $\varphi $ resembles the description of R, in the relevant way.

This presentation assumes that the relation R comes with a preferred description. Typically, the standard $\textsf {PA}$ -provability predicate $\mathsf {prov_{pa}}(x) := \exists y \, \mathsf {prf_{pa}} (y,x)$ resembles the standard description of the notion of $\textsf {PA}$ -provability. By contrast, the Rosser $\textsf {PA}$ -provability predicate $\mathsf {rprov_{pa}}(x) := \exists y \, ( \mathsf {prf_{pa}} (y,x) \land \forall v\leq y \; \neg \mathsf {prf_{pa}}(v, \mathsf {neg}(x)) )$ does not, as it contains a second conjunct which does not resemble any part of the standard description of $\textsf {PA}$ -provability.Footnote ¹⁴

As in the previous example, the focus is usually on structural resemblance between a formula and a description (see, e.g., [Reference Niebergall and Kahle59, sec. 2.2] or [Reference Halbach and Leigh38, chap. 12.2]). However, many such descriptions (often implicitly) include computable properties that cannot be captured simply by structural resemblance. This suggests that the resemblance criterion should also be concerned with computable resemblance. A natural way to articulate this is, for example, by invoking the Church-Turing thesis and the arithmetical hierarchy. To illustrate, let us consider two examples:

First, the set of terms is usually defined, at least implicitly, in such a way as to be, at least, computable (see, e.g., [Reference Hájek and Pudlák36, pp. 21–23] where this requirement is explicit). Take then a $\Sigma _2$ -formula $\varphi $ that structurally resembles the description of the terms (e.g., $\varphi $ is the usual formula but with one of its relevant universal quantifiers left unbounded). There is a clear sense that such a formula fails to be a reasonable representation of the terms, as it does not have the same complexity as the set of terms. On this analysis, by the Church-Turing thesis and the arithmetical hierarchy, $\varphi $ should be a $\Delta _1$ -formula.

Second, we often restrict our interest to computably enumerable (c.e.) theories T, meaning that there is a c.e. set of axioms for T. It is then common to require the formula representing the axiom set of T to be of the same complexity, that is, to be a $\Sigma _1$ -formula or even $\Delta ^b_1$ if one works with p-time decidable theories (see, e.g., [Reference Niebergall, Baaz, Friedman and Krajícek58, sec. 3.2] and [Reference Visser, Horsten and Welch77, p. 68]). For instance, Feferman's [Reference Feferman18, p. 68] representation of the axiom set of $\textsf {PA}$ fails to resemble the usual description of the axioms of $\textsf {PA}$ (at least) on the grounds that this $\Pi _1$ -formula is not of the right complexity.

Although the previous examples make the resemblance criterion appear intuitive and a good heuristic, this criterion is vague, and it is not obvious how to make it mathematically precise. Indeed, it is far from clear what ‘resemblance’ means and whether it can be formally captured, especially in the case of structural resemblance (see [Reference Halbach and Visser39, p. 677] for further difficulties).

4.2 Conditions criterion

To address the many difficulties posed by the resemblance criterion, logicians have adopted an alternative criterion. Instead of requiring resemblance, they focus on identifying key conditions that any representation of a relation should fulfil. These conditions are to be proved within a theory T for a class of formulas, which are then taken to represent the relation.

• Conditions criterion. For a theory T and a relation R, a formula $\varphi $ is a reasonable representation of R iff T proves the conditions for R with $\varphi $ .

This criterion, unlike the resemblance criterion, is mathematically well-defined once its conditions are specified. And it has been successfully applied throughout metamathematics. Löb’s conditions for the notion of provability are the paradigmatic examples of such a criterion, and are commonly used in the “modal” proof of $\textsf {G}2$ . Other examples of conditions criteria are numerous, for example, with partial truth [Reference Halbach and Visser39, pp. 675–676], terms [Reference Hájek and Pudlák36, chap. V.3(g)], or theorems [Reference Buss and Buss9, p. 116].

The conditions criterion is often glossed and motivated in anthropomorphic terms. When working with representations, we need to ensure that they are reasonable. This usually requires proving certain results about the representation. For instance, with any implementation of the terms, one should prove that some unique readability theorem holds. In metamathematics, the situation is similar, except that such results must be established in the theory. For a theory T to “know” or “understand” a relation amounts for T to prove the conditions criterion for that relation (see, e.g., [Reference Detlefsen16, p. 45]).Footnote ¹⁵

It is extremely difficult to find conditions such that all the formulas that satisfy them in some theory are intuitively reasonable. The main issue with the conditions criterion is that, while it can provide necessary conditions for a formula to be a reasonable representation, it often fails to provide sufficient conditions. For example, any theory T proves Löb’s conditions for the trivial $x=x$ , yet it obviously does not represent provability.

4.3 Complementary criteria

Despite these difficulties, both of these criteria are widely accepted and used throughout the literature. A proper defence and detailed exposition of them would take us too far afield. My aim here is instead to suggest that, contra their usual presentation, these two criteria should not be regarded as opposed. On the contrary, I shall argue that their roles are distinct and that both are required for a complete analysis of indeterminacy in metamathematics.

The conditions criterion is given with respect to a theory T. An obvious issue is that different theories might disagree on which conditions are provable. Typically, $\textsf {PA}$ proves Löb’s conditions with $\mathsf {prov}_{\mathsf {pa}}$ , but $\textsf {Q}$ fails to do so. What should we then conclude from the representation of $\textsf {PA}$ -provability by $\mathsf {prov}_{\mathsf {pa}}$ ? To answer this worry, we could choose a fixed base theory $\textsf {Base}$ that will determine the reasonableness of any representation. This solution is, however, unattractive. Given some fixed base theory $\textsf {Base}$ , this criterion can only distinguish formulas up to $\textsf {Base}$ -provability, which might be too coarse-grained for our purposes. Take, for example, the standard conditions criterion for terms. Any two $\Delta _0$ -formulas satisfying them are equivalent already in $\textsf {I} \Delta _0$ (in this case, some additional assumptions are at play, see [Reference Hájek and Pudlák36, pp. 312–313]). However, it does not follow that all these formulas are equally good representations of the terms. For instance, the representation relying on “counting the brackets” of the terms satisfies these conditions, but one could still argue against its reasonableness. Furthermore, independently of the choice for $\textsf {Base}$ , it is questionable whether a formal theory and its strength should play any role in determining the reasonableness of a representation (see [Reference Visser, Horsten and Welch77, secs. 3.3–3.4] and [Reference Visser81, sec. 2] for further arguments and a detailed discussion).

In contrast, the resemblance criterion, by lacking any reference to a theory, fails to capture the interplay between a representation and the choice of the base theory. For instance, $\mathsf {con}(\mathsf {PA})$ , which is presumably a reasonable representation of the consistency of $\textsf {PA}$ , is unprovable both in $\textsf {PA}$ and $\textsf {Q}$ . Yet these two results are usually interpreted differently. The former is taken as evidence that $\textsf {PA}$ does not prove its own consistency. While the latter is not generally taken as showing that $\textsf {Q}$ fails to prove the consistency of $\textsf {PA}$ , $\textsf {Q}$ being too weak to “understand” $\mathsf {con}(\mathsf {Q})$ (let alone $\mathsf {con}(\mathsf {PA})$ ) as a consistency statement.Footnote ¹⁶ There is, more generally, an interesting interplay between the choice of the formula representing some properties and the choice of the theory. Much like the conditions criterion with a fixed base theory, the resemblance criterion fails to capture such an interplay.

This analysis suggests that these criteria have two fundamentally distinct roles. First, the resemblance criterion aims to specify the reasonableness of a representation. It is the relation between a formula, that is, the representation, and the description of some relation, that is, what is being represented, which informs us whether such representation is reasonable or not. The resemblance criterion simply states that resemblance ensures the reasonableness of the representation. Such a notion is independent of any theory, as it takes place between a formula and a description.

On the other hand, the conditions criterion is not about representation in itself, but rather about reasonable representation for a given theory T. It is one thing to have a reasonable representation but another to realise or recognise this representation as reasonable. The conditions criterion is concerned with the latter. On this view, whether a proof of a statement within that theory can be legitimately interpreted as being about what the statement represents also depends on whether the theory recognises it as reasonable. There are many examples where a representation is reasonable, but a theory is too weak to recognise and use it, that is, too weak to prove the conditions criterion for it. The standard arithmetisation of terms with $\mathsf {gn}_1$ seems reasonable, yet $\textsf {I} \Delta _0$ fails to prove the conditions for it. Similarly, $\mathsf {con}(\mathsf {PA})$ is a reasonable consistency statement of $\textsf {PA}$ , as well as for $\textsf {PA}$ but not for $\textsf {Q}$ . Hence, a formula can be a reasonable representation tout court without being reasonable for T (and vice versa). If our analysis is correct, then both the resemblance and conditions criteria are needed to fully capture the indeterminacy in metamathematics.

A complete defence and analysis of these claims is beyond the scope of this paper. In the remaining parts of this article, my aim is to apply this understanding to the question of reasonable numbering, which we treat as a case study of the more general thesis. But before applying the resemblance and conditions criteria to numberings, it is first necessary to define and motivate what exactly a numbering is supposed to represent.

5.1 The data structures conception

Following Gödel [Reference Gödel25], the standard approach to arithmetise syntax assigns a unique number to each element of the background universe. Typically, it “consists in the arithmetic imitation of the linear arrangement of signs.” The usual definitions of the syntax are then arithmetised with tracking functions of concatenation (see, e.g., [Reference Rautenberg69, sec. 6.2] or [Reference Smith72, chap. 20]).

Grabmayr [Reference Grabmayr31] proposes generalising this approach with the notion of a data structure. Roughly, a data structure $\mathbf {D}$ is an algebra with a domain D together with some fundamental operations that finitely generate D.Footnote ¹⁹ Examples include the Kleene star $A^\ast $ with concatenation, that is, $\langle A^\ast , {{}^\smallfrown } \rangle $ , the natural numbers and the successor operation, and the hereditary finite sets with the adjunction operation. All these domains provide common background universes for defining our formal expressions.

Since standard background universes can generally be presented as data structure domains, Grabmayr [Reference Grabmayr31] analyses numberings in relation to their data structures. Given a data structure $\mathbf {D}$ , a numbering $\alpha $ of D induces a structure isomorphic to $\mathbf {D}$ with $\alpha (D)$ as its domain and with the $\alpha $ -tracking functions of $\mathbf {D}$ ’s fundamental operations as its fundamental operations. For instance, with the data structure $\langle A^\ast , {{}^\smallfrown } \rangle $ , our standard numbering $\mathsf {gn}_1$ of $A^\ast $ induces the isomorphic structure $\langle \mathsf {gn}_1(A^\ast ), {{}^\smallfrown }^{\mathsf {gn}_1} \rangle $ . Such an arithmetical structure is then taken to be the basis of the arithmetisation of $\mathbf {D}$ , that is, as the representation or simulation of $\mathbf {D}$ induced by the numbering [Reference Grabmayr29, sec. 3.1]. We then say that, for a data structure $\mathbf {D}$ , a numbering $\alpha $ of D is a computable simulation of $\mathbf {D}$ iff $\alpha (D)$ is decidable and all $\alpha $ -tracking functions of the fundamental operations of $\mathbf {D}$ are recursive.Footnote ²⁰ A generalisation of Mal’cev’s theorem then shows that any two computable simulations of $\mathbf {D}$ are $\mathbb {REC}$ -equivalent, and so they agree on which sets and functions are decidable and recursive, respectively [Reference Grabmayr30, sec. 2.3]. A version of $\textsf {G}2$ can then be proved to be invariant for numberings that computably simulate their data structure (together with additional conditions on the notation, see [Reference Grabmayr31]).

Under this conception, the arithmetisation of syntax, and hence the evaluation of numberings, is understood primarily through the arithmetisation of data structures. The syntax with its constructor operations is arithmetised and evaluated through the tracking functions of the data structure’s fundamental operations. While this approach is widely adopted in many instances of arithmetisation, I consider it to be inadequate for addressing the question of reasonable numberings.

First, the notion of a data structure and its arithmetisation appears to be orthogonal to the arithmetisation of syntax. Although the background universe used to define syntax is often the domain D of a data structure, not every object in D typically represents a syntactic expression. Take $+{\rightarrow }\mathsf {0} \in A^\ast $ , which has no role in, say, the implementation $\textsf {pre}$ . Why should such a string have a code? A numbering $\alpha $ of ${A^\ast \setminus \{+{\rightarrow }\mathsf {0}\}}$ that agrees with $\mathsf {gn}_1$ on its domain seems as reasonable as $\mathsf {gn}_1$ , and most proofs using $\alpha $ , for example, of $\textsf {G}2$ , are identical to those using the standard numbering $\mathsf {gn}_1$ . As illustrated by our numbering $\mathsf {gn}_3$ on $\mathsf {pre}$ , which is defined on $\mathrm {Exp}_{\mathsf {pre}}$ but not on $A^\ast $ , encoding the set of syntactic expressions is already sufficient. There is thus no need to encode the whole background universe used to define the syntax.

A similar point applies to the notion of computable simulation. For a numbering $\alpha $ on D, it is not clear why we should require the whole $\alpha (D)$ to be decidable, and similarly for the relevant $\alpha $ -tracking functions. Take, for instance, a non-recursive function (on the relevant domain) h, and consider the numbering $\alpha $ on $\textsf {pre}$ defined as $2 \cdot h(\mathsf {gn}_1(s)) + 1 $ for any $t \in A^\ast $ and $s \equiv +{\rightarrow }\mathsf {0}t$ and as $\mathsf {gn}_1$ otherwise. In this case, the tracking function ${{{}^\smallfrown }}^{\alpha }$ is not recursive, so $\alpha $ is not a computable simulation of $\langle A^\ast , {{}^\smallfrown } \rangle $ . Yet, the sets of codes of $\textsf {pre}$ -terms and of $\textsf {pre}$ -formulas are still $\Delta _1$ in $\textsf {PA}$ as they can be defined using the same standard definition with $\mathsf {gn}_1$ , and the usual $\alpha $ -tracking functions of the $\textsf {pre}$ -constructor functions are all $\textsf {PA}$ -provably recursive, since the corresponding $\mathsf {gn}_1$ -tracking functions are.

Second, even if one insists on arithmetising a whole data structure, the focus on data structures adds an additional layer, which introduces further indeterminacy and distracts from the question of reasonable numberings.

The numberings sharing a given mathematical property, and hence the associated invariance results, are relative to the choice of data structure. For a given data structure $\mathbf {D}$ , Mal’cev’s theorem implies that any two computable simulations of $\mathbf {D}$ are $\mathbb {REC}$ -equivalent. However, this does not imply that computable simulations of two distinct data structures are $\mathbb {REC}$ -equivalent, even on the same domain. Moreover, a suitable data structure is neither guaranteed to exist nor to be unique: For a numbering $\alpha $ on $\imath $ , there might be no data structure $\mathbf {D}$ whose domain is $\mathrm {dom}(\alpha ) \supseteq \mathrm {Exp}_\imath $ (as, e.g., with the $\alpha $ defined on $A^\ast \setminus \{+{\rightarrow }\mathsf {0}\}$ ). And even when such a data structure exists, it need not be unique. For the numbering $\mathsf {gn}_1$ of $A^\ast $ , there are many different data structures with domain $A^\ast $ , that is, many ways to finitely generate $A^\ast $ (with the usual concatenation operation ${{}^\smallfrown }$ , with “successor” operations ${{}^\smallfrown } a$ for each $a\in A$ , etc.). Which of these should we take $\mathsf {gn}_1$ to represent?

This indeterminacy runs even deeper. Among the many data structures, some are deviant (see [Reference Grabmayr31, sec. 5.2] and [Reference Grabmayr32, sec. 7]). Using such deviant data structures, it is possible to make clearly unreasonable numberings, such as our unreasonable $\mathsf {gn}_4$ with X as the set of T-provable sentences, into computable simulations.Footnote ²¹ Thus, unreasonable numberings can still induce a perfectly adequate representation of a deviant data structure. This forces us to consider not only the choice of numberings but also the choice of data structures, thereby introducing a further indeterminacy.

For these reasons, I consider the first conception of arithmetisation inadequate for defining reasonable numberings.Footnote ²² I now turn to the second conception.

5.2 The proto-syntax conception

Following Hilbert and Bernays [Reference Hilbert and Bernays43], the second conception of the arithmetisation of syntax focuses on the generation of syntactic expressions. Since an implementation $\imath $ associates the symbols of the alphabet with $\imath $ -constructor functions, this conception of arithmetisation associates such functions with arithmetical functions. In the same way a formula is generated by some sequence of $\imath $ -constructor functions, its code is generated by the same sequence of arithmetised $\imath $ -constructor functions.

At first sight, this suggests assessing numberings with respect to their representation of the underlying implementation. However, this would understate the independence of arithmetisation from the specific implementation. Hilbert and Bernays [Reference Hilbert and Bernays43, p. 217]’s reference to the “grammatical construction” appears to run deeper than any specific implementation of that construction. Kleene [Reference Kleene47, pp. 246–258] adopts a similar position with his notion of “generalized arithmetic entities” which are built so as to “emphasize [the] structure (i.e., modes of generation)” of each syntactic expression. Indeed, we can arithmetise the generation of a formula, for example, via a compositional numbering, independently of the specific generation of the formula given by the implementation. While some authors do define compositional numberings to mimic their implementation, for example, our $\mathsf {gn}_3$ on $\textsf {pre}$ or van Dalen's numbering on $\textsf {inf}$ [Reference van Dalen15, p. 246], it is more common to define them independently of their underlying implementation (see, e.g., [Reference Avigad1, p. 259] or [Reference Hilbert and Bernays43, pp. 217–219] both of which implement syntax with $\textsf {inf}$ but arithmetise it by mimicking the simpler $\textsf {pre}$ implementation).

To articulate this approach, I rely on the notion of proto-syntax, which extends our presentation of the syntax in §2. This notion is motivated by the insight that both ‘ $\rightarrow \!\varphi \,\psi $ ’ and ‘ $(\varphi \rightarrow \psi )$ ’ are different representations, in prefix and infix notation, respectively, of the implication from $\varphi $ to $\psi $ . There is thus, by abstraction, an intuitive notion of implication, and similarly with any constructor function, which guides the implementation of syntax.Footnote ²³ As Kleene [Reference Kleene47, p. 62] nicely puts it: “An intuitive mathematics is necessary even to define the formal mathematics.” It is precisely such an intuitive mathematics that helps us to understand why we share the insight that our metamathematical results should hold with some generality and independently of the non-essential details of implementation and arithmetisation. Let us then refer to the intuitive conception of syntax that underlies any implementation and arithmetisation as the proto-syntax. Following Grabmayr [Reference Grabmayr31, secs. 4.1–4.2], let $\Omega (\mathcal {L})$ be the abstract signature of the language $\mathcal {L}$ . Since an implementation $\imath $ inductively and freely generates the $\imath $ -variables, $\imath $ -terms, and $\imath $ -formulas, there is a unique free $\Omega (\mathcal {L})$ -algebra $\mathbf {S}_\imath $ whose (overall) domain is the set of $\imath $ -expressions and whose fundamental operations are the $\imath $ -constructor functions. The structure of the proto-syntax is then the free algebra $\mathbf {S}$ , which, for each implementation $\imath $ , is isomorphic to $ \mathbf {S}_\imath $ . An implementation can then be analysed as specifying a particular instantiation of $\mathbf {S}$ . More details can be found in the Appendix A.Footnote ²⁴

I suggest understanding the arithmetisation of syntax through the arithmetisation of proto-syntax, and in particular its structure $\mathbf {S}$ . A numbering is not taken as representing a given implementation of syntax (or a data structure), but rather as giving its own representation, or instantiation, of the proto-syntax. Since, by definition, every numbering is defined on the set of expressions, the particular representation of the proto-syntax of any numbering can be defined as follows: Given a numbering $\alpha $ on an implementation $\imath $ , there is an induced free algebra, whose (overall) domain is $\alpha (\mathrm {Exp}_\imath )$ and whose fundamental operations are the $\alpha $ -tracking functions of the $\imath $ -constructor functions. Let us call such an arithmetical structure the $\alpha $ -syntax. Being a free algebra on $\Omega (\mathcal {L})$ , the $\alpha $ -syntax is also isomorphic to $\mathbf {S}$ , and it is this structure that I take to be the arithmetical representation of the proto-syntax induced by $\alpha $ . See Appendix A for a specific example of this construction.

The proto-syntax conception may be viewed as a special case of the data structures conception, in which the only relevant data structure, common by definition to all numberings, is the proto-syntax (see also [Reference Grabmayr31, remark 4.12]). The key advantage of this restriction is that it frees the analysis of numberings from what Halbach and Visser [Reference Halbach and Visser40, p. 711] call the various “matter[s] of implementation.” Which implementation and background universe are reasonable? What is the “essence of conjunction”? Are brackets essential or not? (See, e.g., [Reference Grabmayr32, secs. 6–7], [Reference Halbach and Visser40, p. 711], and [Reference Grabmayr31, sec. 5].) In the present framework, such distracting questions are set aside in favour of questions concerning the numbering itself and its representation of the proto-syntax.

This abstraction is justified by the fact that the induced syntax does not retain information about the implementation on which it was induced. Although the construction of the $\alpha $ -syntax refers to the particular implementation on which the numbering $\alpha $ is defined, the resulting structure is purely arithmetical and represents the syntax independently of that implementation. Indeed, one cannot recover from the $\alpha $ -syntax the particular implementation or data structure used in its construction. Furthermore, given any implementation $\imath $ , one can define a numbering $\beta $ on $\imath $ whose induced $\beta $ -syntax is identical to the $\alpha $ -syntax. Thus, the specific implementation plays no essential role once the induced syntax has been obtained. There is therefore no need to further generalise over implementations, data structures, or background universes: the representation of the proto-syntax by a numbering is independent of such notions.

A further advantage of this conception is its uniformity. Since every numbering $\alpha $ induces an $\alpha $ -syntax that is isomorphic to the structure of the proto-syntax $\mathbf {S}$ , all numberings can be studied within a single and uniform framework. Conditions imposed on the notion of induced syntax apply uniformly across all numberings, thereby defining classes of numberings that are not relative to any particular implementation or data structure.

To illustrate, suppose that the domains and fundamental operations of each induced syntax are required to be decidable and recursive, respectively. Mal’cev’s theorem then yields a unique class of $\mathbb {REC}$ -equivalent numberings relative to their induced syntax. Of course, numberings in this class need not themselves be $\mathbb {REC}$ -equivalent, since they may not even be defined on the same domain. Nevertheless, since the basic syntactic relations are solely defined on the syntactic expressions, the recursivity of any such syntactic relation is invariant throughout this class. Together with an analysis of the proofs in Grabmayr [Reference Grabmayr31, sec. 7], this observation shows that our standard metamathematical results generalise to this class of numberings.

6.1 Resemblance criterion for numberings

Which properties of numberings can be motivated by the resemblance criterion for numberings? On the present analysis, the key properties of the proto-syntax will provide, via resemblance, some necessary conditions on reasonable numberings. I first discuss structural properties, followed by computable properties, which, as argued in §4.1, also enter the resemblance criterion.

6.2 Conditions criterion for numberings

Let us turn now to the question of how the choice of the base theory interacts with the choice of numbering. If the preceding resemblance criterion provides some necessary conditions for a numbering to be reasonable, by itself, it does not settle the question of what it means for a numbering to be reasonable for a given theory.

The intuitive distinction between a numbering being reasonable simpliciter and its being reasonable for a given theory T can be illustrated as follows. Presumably, the standard numbering $\mathsf {gn}_1$ is both reasonable and reasonable for $\textsf {PA}$ . However, in §3, I showed that $\textsf {I} \Delta _0$ fails to prove most basic syntactic results with $\mathsf {gn}_1$ . In this sense, despite being reasonable, $\mathsf {gn}_1$ fails to be reasonable for $\textsf {I} \Delta _0$ . The numbering $\mathsf {gn}_4$ , with X as the set of $\textsf {PA}$ -provable sentences, is an obvious candidate for a numbering that is neither reasonable nor reasonable for $\textsf {PA}$ since $\textsf {PA}$ even fails to binumerate some of the $\mathsf {gn}_4$ -tracking functions of the $\mathsf {pre}$ -constructor functions. Note, however, that $\mathsf {gn}_4$ may be reasonable for stronger (not necessarily c.e.) base theories, provided that they can handle $\textsf {PA}$ -provability, while still being an unreasonable numbering. A similar phenomenon occurs when we consider $\textsf {I} \Sigma _1$ and $\textsf {PA}$ with the numbering $\mathsf {gn}_4$ with X as the set of $\textsf {I} \Sigma _1$ -provable sentences. Finally, self-referential numberings such as $\mathsf {gn}_5$ could well be taken as unreasonable, while still being reasonable for $\textsf {PA}$ . Indeed, $\mathsf {gn}_5$ can be made $\mathbb {REC}$ -equivalent to $\mathsf {gn}_1$ .

In §4.3, I briefly argued that the conditions criterion gives us a way to specify when a representation is reasonable for a given theory T. Given our previous analysis, for a numbering $\alpha $ to be reasonable for T, T should recognise that the structure induced by $\alpha $ is a representation of the proto-syntax. In other words, it should prove sufficiently many basic features of the $\alpha $ -syntax. The aim of this section is not to offer a complete or decisive analysis of the conditions criterion for numberings. Rather, starting from the previous necessary structural and computable properties for reasonable numberings, I outline a conditions criterion for numberings which relativises the class of reasonable numberings to the choice of the base theory.