ABSTRACT
Friedman and Simpson's program of reverse classical mathematics, with
primitive recursive arithmetic PRA as base, is gradually producing a
linear taxonomy for classical analysis. A small number of
successively stronger induction principles and set existence axioms
divide mathematical theorems into equivalence classes based on
classical logic.
Reverse constructive mathematics is more complicated. Linearity is
out of the question, as the recognized varieties of constructive
mathematics agree on basic intuitionistic logic and on some core
mathematical principles such as unrestricted induction but disagree on
others. The fine structure of the common core includes distinctions
which disappear with classical logic.
The precision needed for a constructive taxonomy can be achieved
informally, as in Veldman's axiomatic reverse intuitionistic
mathematics, but formalization is efficient. This talk illustrates a
formal taxonomic structure for intuitionistic and constructive
analysis, based on function existence principles and developed in
collaboration with Garyfallia Vafeiadou in the tradition of Kleene,
Vesley and Troelstra.
