Thumbnail Image

Arithmetical Foundations - Recursion. Evaluation. Consistency

Pfender, Michael

Preprint-Reihe des Instituts für Mathematik, Technische Universität Berlin

Johannes Zawacki, my high school teacher, told us about Gödel's second theorem, on non-provability of consistency of mathematics within mathematics. Bonmot of André Weil: Dieu existe parceque la Mathématique est consistente, et le diable existe parceque nous ne pouvons pas prouver cela - God exists since Mathematics is consistent, and the devil exists since we cannot prove that. The problem with 19th/20th century mathematical foundations, clearly stated in Skolem 1919, is unbound in nitistic (non-constructive) formal existential quanti cation. In his 1973 Oberwolfach talk André Joyal sketched a categorical - map based - version of the Gödel theorems. A categorical version of the unrestricted non-constructive existential quanti er was still inherent. The consistency formula of set theory (and of arbitrary quanti ed arithmetical theories), namely: not exists a proof code for (the code of ) false, can be introduced as a (primitive) recursive - Gödel 1931 - free variable predicate: "For all arithmetised proofs k : k does not prove (code of) false:" Language restriction to the constructive (categorical) free-variables theory PR of primitive recursion or appropriate extensions opens the possibility to circumvent the two Gödel's incompleteness issues: We discuss iterative map code evaluation in direction of (termination conditioned) soundness, and based on this, decidability of primitive recursive predicates. In combination with Gödel's classical theorems this leads to unexpected consequences, namely to consistency provability and logical soundness for recursive descent theory πR : theory of primitive recursion strengthened by an axiom schema of non-in nite descent, descent in complexity of complexity controlled iterations like in particular (iterative) p.r.-map-code evaluation. We show an antithesis to Weil's above: Set theoretically God need not to exist, since his - Bourbaki's - "Theorie des Ensembles" is inconsistent. The devil does not need to exist, since we can prove inside free-variables recursive mathematics this mathematics consistency formula. By the same token God may exist.