Vol. 84, No. 1, 1979

Recent Issues
Vol. 328: 1
Vol. 327: 1  2
Vol. 326: 1  2
Vol. 325: 1  2
Vol. 324: 1  2
Vol. 323: 1  2
Vol. 322: 1  2
Vol. 321: 1  2
Online Archive
The Journal
Editorial Board
Submission Guidelines
Submission Form
Policies for Authors
ISSN: 1945-5844 (e-only)
ISSN: 0030-8730 (print)
Special Issues
Author Index
To Appear
Other MSP Journals
Goodman’s theorem and beyond

Michael James Beeson

Vol. 84 (1979), No. 1, 1–16

Goodman proved that if the axiom of choice xyA(x,y) →∃fxA(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.

Mathematical Subject Classification 2000
Primary: 03F50
Secondary: 03F35
Received: 30 March 1977
Published: 1 September 1979
Michael James Beeson