Inhalt des Dokuments
Preprint 32-2013
Arithmetical Foundations Recursion. Evaluation. Consistency Excerpt
Author(s) :
Michael Pfender
Preprint series of the Institute of Mathematics, Technische Universität Berlin
Preprint 32-2013
MSC 2000
- 03G30 Categorical logic, topoi
-
03B30 Foundations of classical theories
-
03D75 Abstract and axiomatic computability and recursion theory
Abstract :
Recursive maps, nowadays called primitive recursive maps, PR maps,
have been introduced by Gödel in his 1931 article for the arithmetisation,
gödelisation, of metamathematics.
For construction of his undecidable formula he introduces a nonconstructive,
non-recursive predicate beweisbar, provable.
Staying within the area of categorical free-variables theory PR
of primitive recursion or appropriate extensions opens the chance to
avoid the two (original) Gödel's incompleteness theorems: these are
stated for Principia Mathematica und verwandte Systeme, "relatedsystems" such as in particular Zermelo-Fraenkel set theory ZF and v. Neumann Gödel Bernays set theory NGB.
On the basis of primitive recursion we consider μ-recursive maps as partial p. r. maps. Special terminating general recursive maps considered are complexity controlled iterations. Map code evaluation is then given in terms of such an iteration.
We discuss iterative p. r. map code evaluation versus termination
conditioned soundness and based on this decidability of primitive recursive
predicates. This leads to consistency provability and soundness
for classical, quantified arithmetical and set theories as well as for the
PR descent theory πR, with unexpected consequences:
We show inconsistency provability for the quantified theories as
well as consistency provability and logical soundness for the theory
πR of primitive recursion, strengthened by an axiom scheme of noninfinite
descent of complexity controlled iterations like (iterative) mapcode
evaluation.