Truth, Support, and Arithmetic

Support versus derivability

Working within the proof-theoretic semantics of Sandqvist, in which a semantic consequence relation $\Vdash$ is defined compositionally via support in bases of atomic inference rules, we show that this relation and derivability ($\vdash$) diverge for any sufficiently strong, recursively axiomatisable arithmetic theory $A$ in the standard signature $\sigma = \langle 0, S, +, \times \rangle$: one has $A \Vdash \mathrm{Con}(A)$, even though $A \nvdash \mathrm{Con}(A)$. More generally, we establish the uniform reflection principle

$$A \Vdash \mathrm{Prov}_A(\ulcorner \varphi \urcorner) \to \varphi.$$

The proof proceeds by induction on codes of $A$-proofs, analysing the compositional clauses of the support relation. A key new observation is that the finiteness of the signature of arithmetic is what precisely controls the relationship between support and derivability: it prevents the completeness direction of the soundness and completeness theorem from going through, so that semantic support is strictly stronger than derivability. Gödel's theorem is not contradicted; rather, incompleteness arises exactly at the point where completeness breaks down.

An elementary consistency proof

We further show that the framework admits an elementary consistency proof for $\mathsf{PA}$: ordinary induction over the natural numbers suffices to construct a consistent base supporting the axioms of $\mathsf{PA}$, yielding $\mathsf{PA} \nvdash \bot$ by soundness. This stands in notable contrast to Gentzen's use of transfinite induction up to $\varepsilon_0$.

Together, these results establish that Gödel's incompleteness theorems can be understood as a separation between derivability and proof-theoretic semantic consequence, rather than as a gap between syntactic provability and truth in an independently given model.

References