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.