Goodman proved that if the
axiom of choice ∀x∃yA(x,y) →∃f∀xA(x,f(x)) is added to intuitionistic arithmetic
(here x, y, and f are functionals of finite type), then no new arithmetic theorems
are obtained. His original proof used his theory of constructions, and was
widely thought to be perhaps not the simplest proof possible. Moreover,
the generalization of the result to show that the axiom of choice remains
conservative even in the presence of extensionality, has remained unsolved, despite
its inclusion in Friedman’s list of “102 Problems in Mathematical Logic”.
In this paper, we give a conceptually clear proof of Goodman’s theorem,
and use the method to solve Friedman’s problem just mentioned, as well
as to obtain several other extensions of Goodman’s theorem and related
results.
