Summary:
This dissertation investigates certain aspects of the formalization and
axiomatization of constructive analysis.
The research in the branches of constructive analysis corresponding to the
various forms of constructivism is carried out in a multitude of formal or
informal systems, whose relations are unclear. This problem becomes quite
crucial for the development of the relatively new field of constructive reverse
mathematics. This work contributes to a clearer picture.
Part 1 contains a precise comparison of the two most widely used systems which
formalize the common core of constructive, intuitionistic, recursive and
classical analysis, namely
Kleene's M and Troelstra's EL. It is shown that EL is weaker than M and that
their difference is captured by a function existence principle asserting that
every decidable predicate of natural numbers has a characteristic function.
Applying similar arguments, comparisons of most of the used minimal systems are
obtained.
In constructive analysis, various forms of choice principles, continuity
principles and many others are used. Part 2 studies relations between many of
them, in their versions having a
uniqueness condition, a feature from which interesting properties follow, as
well as relations between these principles and non-constructive logical
principles, in the spirit of reverse
mathematics.
Keywords:
Analysis, Constructive, Formalization, Axioms, Second-order
