Sie sind hier

## Arithmetical Foundations - Recursion. Evaluation. Consistency

 Source file is available as : Portable Document Format (PDF)

Author(s) : Michael Pfender

Preprint series of the Institute of Mathematics, Technische Universität Berlin
Preprint 3-2019

MSC 2000

03G30 Categorical logic, topoi
03B30 Foundations of classical theories
03D75 Abstract and axiomatic computability and recursion theory

Abstract :
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.

Keywords : primitive recursion, categorical free-variables Arithmetic, code evaluation, Stimmigkeit, soundness, decidability of PR predicates, Goedel theorems, self-inconsistency of quantified arithmetical theories