I am just putting the finishing touches to a paper in which I show that there are at least as many Gödelian undecidable’ arithmetical propositions as there are recursive relations!

The paper offers a finitary view of Gödel’s and Rosser’s undecidable’ propositions from a computational perspective; where I argue against the widely accepted conclusion of self-referential causality that Kurt Gödel has drawn from his seminal 1931 paper on formally undecidable arithmetical propositions.

This is the conclusion that Gödel’s undecidable’ arithmetical proposition—which is of the form $[(\exists x)R(x)]$—is undecidable because it involves self-reference; in the sense that, under any model of the arithmetic, the proposition can be taken to assert that:

The arithmetical formula with Gödel number $\lceil [(\exists x)R(x)]\rceil$ is not provable in the arithmetic’

where $\lceil [F] \rceil$ denotes the Gödel number of the arithmetical formula $[F]$.

I suggest that, to some extent, such a perception of self-reference (and perhaps even of diagonalisation) as the primary—or even as a necessary—cause of arithmetical undecidability’ may be misleading.

For instance, in the Gödelian case above, $[R(x)]$ is the standard arithmetical representation of a standard (albeit unusually defined in a seemingly circular way) primitive recursive relation.

I show that, if we assume the standard interpretation of PA as sound (in the sense of defining a model of PA), then Gödel’s arithmetical representation of any recursive relation yields a similarly undecidable’ PA formula.

I further show that this Gödelian characteristic is merely a reflection of the fact that, by the instantiational nature of their constructive definition in terms of Gödel’s $\beta$-function, such formulas are designed to be algorithmically verifiable, but not algorithmically computable, under the standard interpretation of PA.

From this perspective, the significance of Gödel’s 1931 construction of an undecidable’ proposition is that it facilitates formalisation of a distinction between algorithmically verifiable’ arithmetical formulas and algorithmically computable’ arithmetical formulas.

When expressed formally, this distinction leads naturally to the two distinctly different—and hitherto unsuspected—finitary interpretations of the first order Peano Arithmetic PA detailed in a paper that I had presented in Birmingham last July at the Symposium on Computational Philosophy at the AISB/IACAP World Congress 2012-Alan Turing 2012.

The first is the standard interpretation of PA over the natural numbers in which the true sentences are defined as all those PA-propositions that are algorithmically verifiable as true.

This interpretation admits the existence of formally undecidable’ Gödelian propositions, but does not define a model of PA from a finitary perspective.

The second is an algorithmic interpretation over the natural numbers, in which the true sentences are defined as only those PA-propositions that are algorithmically computable as true.

Prima facie, this interpretation does not admit the existence of formally `undecidable’ Gödelian propositions, but it does define a model of PA from a finitary perspective.

Author’s working archives & abstracts of investigations