Vol. 88, No. 1, 1980

Recent Issues
Vol. 308: 1
Vol. 307: 1  2
Vol. 306: 1  2
Vol. 305: 1  2
Vol. 304: 1  2
Vol. 303: 1  2
Vol. 302: 1  2
Vol. 301: 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
Extensionality and choice in constructive mathematics

Michael James Beeson

Vol. 88 (1980), No. 1, 1–28

We study the relationships between two kinds of formal systems which have been proposed for formalizing modern constructive mathematics. Essentially, we show how to interpret the set-theoretic systems of Friedman and Myhill in the operation-theoretic systems of Feferman. As a by-product of this interpretation, we prove that Friedman’s system B and certain of Feferman’s systems are conservative over intuitionistic arithmetic. We also hope the interpretation casts some light on the nature of the concepts axiomatized in the two systems.

Mathematical Subject Classification 2000
Primary: 03F50
Received: 30 March 1977
Published: 1 May 1980
Michael James Beeson