Set theoretic foundations for constructive analysis


We introduce an extensional set theoretic formalism $\mathbf{B}$, a subsystem of Zeromelo set theory based on intuitionistic logic, which provides a set theoretic foundation for consturctive anlaysis which is strikingly analogous to the usual set theoretic foundations for ordinary analysis. We prove that $\mathbf{B}$ has the same elementary $(\Pi_2^0)$ consequences as first order arithmetic, and that every arithmetic consequence of $\mathbf{B}$ is a consequence of Peanu arithmetic. We indicate a definitional translation of $\mathbf{B}$ into an intensional theory of predicates, which in turn has a natural interpreptation in the informal theory of constructions. Variants of $\mathbf{B}$ are discussed, including some related work of ours bearing on formalisms for ordinary analysis.


Harvey Friedman