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
Volume:
Issue:
     
The Journal
Subscriptions
Editorial Board
Officers
Contacts
 
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
Abstract

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
Milestones
Received: 30 March 1977
Published: 1 May 1980
Authors
Michael James Beeson