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 —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 is not provable in the arithmetic’
where denotes the Gödel number of the arithmetical formula .
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, 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 -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.