Beyond Goedel : Simply consistent constructive systems of first order Peano's Arithmetic that do not yield undecidable propositions by Goedel's reasoning

Abstract

In this paper, we argue that formal systems of first order Arithmetic that admit Goedelian undecidable propositions validly are abnormally non-constructive. We argue that, in such systems, the strong representation of primitive recursive predicates admits abnormally non-constructive, Platonistic, elements into the formal system that are not reflected in the predicates which they are intended to formalise. We argue that the source of such abnormal Platonistic elements in these systems is the non-constructive Generalisation rule of inference of first order logic. We argue that, in most simply consistent systems that faithfully formalise intuitive Arithmetic, we cannot infer from Goedel's reasoning the Platonistic existence of abnormally non-constructive propositions that are formally undecidable, but true under every interpretation. We define a constructive formal system of Peano's Arithmetic, omega2-PA, whose axioms are identical to the axioms of standard Peano's Arithmetic PA, but lead to significantly different logical consequences. We thus argue that the formal undecidability of true Arithmetical propositions is a characteristic not of relations that are Platonistically inherent in any Arithmetic of the natural numbers, but of the particular formalisation chosen to represent them.