A comparison of minimal systems for constructive analysis
Abstract
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 CF_d 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.
Keywords
Cite
@article{arxiv.1808.00383,
title = {A comparison of minimal systems for constructive analysis},
author = {Garyfallia Vafeiadou},
journal= {arXiv preprint arXiv:1808.00383},
year = {2018}
}
Comments
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