Léon Probst

The choice of Gödel numberings is one of the sources of indeterminacy in metamathematics; for certain numberings, our well-known theorems, such as Gödel’s second incompleteness theorem, do not hold. However, it is widely believed that all our metamathematical theorems hold for all reasonable Gödel numberings. This article investigates this notion of reasonable Gödel numberings and provides a general framework for answering philosophical questions about Gödel numberings and the arithmetisation of syntax.

Metamathematical results are formulated and proved relative to various formalisation choices, including the choice of Gödel numbering. Recent work shows that classical metamathematical results, such as Gödel’s, Tarski’s, and Church’s theorems, hold for all reasonable choices of numbering. In contrast, the consistency of certain type-free truth theories strongly depends on the underlying numbering. This calls into question whether these axiomatic theories can be taken to faithfully reflect informal reasoning about truth. In this paper, we introduce a new constraint on numberings, which we call uniformity. The guiding idea is that a reasonable numbering should encode the inductive structure of its domain uniformly, without exploiting case distinctions that introduce illicit information. We show that almost all canonical numberings in the literature are uniform. Moreover, we show that the consistency of these truth theories is invariant across all uniform numberings. Uniformity thus provides a principled way of distinguishing genuine metamathematical phenomena from artefacts of coding.

There is a well-known gap between the metamathematical theorems we prove and call Gödel’s second incompleteness theorem and its standard interpretation, which says, roughly, that no consistent and sufficiently strong theory proves its own consistency.

This article argues that the standard approach to this problem, which takes the derivability conditions to be necessary conditions on reasonable representations of provability, fails in its present state. It then sketches an alternative approach based on the resemblance criterion both for justifying the standard interpretation and, more generally, for dealing with reasonable choices in metamathematics.

We discuss some problems of the principle of generic attribution and propose a typed theory of arbitrary objects that avoids them.