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

Bhupinder Singh Anand