|
|
|
|
|
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 | |
|
