direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments

Preprint 3-2019

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

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe