Abstract

We study, from a classical point of view, how the truth of a statement about higher type functionals depends on the underlying model. The models considered are the classical set-theoretic finite type hierarchy and the constructively more meaningful models of continuous functionals, hereditarily effective operations, as well as the closed term model of Gödel's system T. The main results are characterisations of prenex classes for which truth in the full set-theoretic model transfers to truth in the other models. As a corollary we obtain that the axiom of choice is not conservative over Gödel's system T with classical logic for closed ∃2-formulas. We hope that this study will contribute to a clearer delineation and perception of constructive mathematics from a classical perspective