2018/08/01 by Garyfallia Vafeiadou, Vafeiadou, Garyfallia
Computer Science · Mathematics · #03F50 #Computability, Logic, AI Algorithms #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #math.LO #msc:03F50
paper · pdf · doi:10.48550/arxiv.1808.00383
The content of this paper (except the results of 8.1) is from Part I of the author's Ph.D. thesis "Formalizing constructive analysis: a comparison of minimal systems and a study of uniqueness principles", July 2012, Athens, Greece
arxiv created 2018/08/01 · openalex publication_date 2018/08/01 · arxiv updated 2018/08/02 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We establish a precise relation between M, a subsystem of the formal axiomatic system of intuitionistic analysis FIM of S. C. Kleene, and elementary analysis EL of A. S. Troelstra, two weak formal systems of two-sorted intuitionistic arithmetic, both widely used as basis for (various forms of) constructive analysis. We show that EL is weaker than M, by introducing an axiom schema CFd asserting that every decidable predicate of natural numbers has a characteristic function. By similar arguments, we compare some more systems of two-sorted intuitionistic arithmetic, including the formal theory BIM of W. Veldman.