A Proof-theoretic Foundation for Mathematics

Two readings of incompleteness

The context and consequences of Gödel's incompleteness theorems for the foundations of mathematics in the early 20th century are doubtless familiar. The orthodox view—and Gödel's own reading—is that there is a real world of arithmetic that outstrips our ability to formalize it by finitary systems. Tarski developed model-theoretic semantics as a formal account of this view, and it has been the dominant approach to semantics within logic for the last century. This is, however, not the only possible reading.

According to Dummett, this construal begs the very question incompleteness is supposed to bear on. To say that the consistency statement is true but unprovable presupposes a notion of arithmetical truth that floats free of provability, but it is precisely such truth that is at issue. The orthodox reading, therefore, does not discover a gap between truth and provability in some neutral way; rather, it builds one in from the outset. Dummett's own proposal was that the proper moral lies elsewhere. He argued that the concept of a ground for asserting something of all natural numbers is indefinitely extensible: any recursive characterisation of such grounds can be extended, by the Gödelian construction, to a strictly more inclusive one. The proposal attracted important objections—notably from Wright, Moore, and Raatikainen—and in his Reply, Dummett clarified that the principle of extension must itself admit of a precise characterisation, even though the totality it generates cannot.

In what follows I should like to suggest that recent developments in proof-theoretic semantics (P-tS) permit such a characterisation to be given, and that they thereby furnish a technically grounded reading of Dummett's proposal. The vehicle is the base-extension semantics (B-eS) for classical logic developed by Sandqvist; see also Gheorghiu. This semantics is itself presented as a candidate realisation of Dummett's wider programme for logic and mathematics.

Base-extension semantics

Fix a first-order signature $\sigma$. An atomic rule is an inference figure

$$\dfrac{p_1 \quad \cdots \quad p_n}{C}$$

in which $C$ and the $p_i$ are closed atomic formulas ($\bot$ is not counted as atomic). A base $\mathfrak{B}$ is a set of atomic rules, and $\vdash_{\mathfrak{B}}$ denotes the relation of derivability obtained by closing the rules of $\mathfrak{B}$ under composition. The support relation $\Vdash$ is then defined inductively by the clauses in Figure 1; validity is given by $\Gamma \Vdash \phi$ iff $\Gamma \Vdash_{\varnothing} \phi$.

Classical derivability is sound with respect to support. It is also complete in the presence of an infinite reserve of constants disjoint from the theory under consideration; crucially, it may be incomplete without this reserve. The role played by such constants is, in effect, that of eigenvariables; and the requirement that they be available is, philosophically speaking, the requirement that the language be open to extension. I argue that this gap is where we ought to understand the Gödelian incompleteness phenomenon to be about.

Inferential ontology

Dummett believed that logic was determined by a theory of meaning, which was itself determined by a set of practices for justifying the assertion of expressions. This view applied to logic arguably delivers the B-eS above. When applied to a first-order theory $T$, we may read it as saying that the ontology is fixed not by reference to an antecedently given domain but by the inferential practice licensed by $T$ for the closed terms within it. That is, an inferential ontology is determined by the signature $\sigma$—as it specifies the closed terms—together with $T$—as it specifies their inferential roles.

Two cases must therefore be sharply distinguished. In the signature $\sigma := \langle 0, S, +, \cdot \rangle$ in which arithmetic is ordinarily formulated, if the theory $T$ is such that every closed term is equivalent to a numeral, then the ontology is exhausted by the numerals. In a richer signature with additional constants $(c_i)_{i \in \mathbb{N}}$, by contrast, this may not be the case. A constant $c$ for which, using only the inferences of $T$, we cannot assert to be equal to a numeral plays the role of a non-standard number. These two setups have very different properties.

Working in the standard signature $\sigma$, let us say that a theory $T$ is sufficiently strong if it decides $\Delta_0$-sentences and identities between numerals—conditions met by Robinson's $\textsf{Q}$ and by $\textsf{PA}$ alike—and let $\mathrm{Prov}_T(x)$ be the standard provability predicate for $T$. The reflection schema then obtains:

$$T \Vdash \mathrm{Prov}_T(\ulcorner \phi \urcorner) \to \phi \qquad \text{for every sentence } \phi.$$

Taking $\phi$ to be $\bot$ gives $T \Vdash \mathrm{Con}(T)$. The proof follows the structure of a naïve internal soundness proof using the fact that the ontology is exhausted by the numerals: any putative witness to $\mathrm{Prov}_T(\ulcorner \phi \urcorner)$ must be a numeral coding an actual $T$-derivation, and one then proceeds by induction on the length of that derivation—full details are given in Gheorghiu. In the enriched setting with additional constants, the naïve soundness proof does not go through, as the ontology outruns the coding.

Two morals

First, in the finite signature in which arithmetic is naturally formulated, derivability and support come apart, but they do so within a single theory rather than as a divergence between proof and an externally given structure. On the present framework, then, Gödel's second incompleteness theorem is explicable as a consequence of the ontology's being fixed by the theory itself. In a richer signature with extra constants, where nonstandard witnesses become available, classical completeness is recovered and reflection fails accordingly—as it must, on pain of contradicting Gödel.

Second, the reflection schema $\mathrm{Prov}_T(\ulcorner \phi \urcorner) \to \phi$ is precisely such a general characterisation of the principle of extension as Dummett insisted upon in the reply to Wright. To assert the premiss $\mathrm{Prov}_T(\ulcorner \phi \urcorner)$ is to perform the act of extension, not to describe a number already present in some antecedently fixed domain; and the indefinite iterability of the schema is what ensures that no recursive axiomatisation can capture its closure.

References