|
This article is available for purchase or by subscription. See below.
Abstract
|
|
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.
|
Mathematical Subject Classification 2000
Primary: 03F50
Secondary: 03F35
|
PDF Access Denied
We have not been able to recognize your IP address
18.119.17.207
as that of a subscriber to this journal.
Online access to the content of recent issues is by
subscription, or purchase of single articles.
Please contact your institution's librarian suggesting a subscription, for example by using our
journal-recommendation form.
Or, visit our
subscription page
for instructions on purchasing a subscription.
You may also contact us at
contact@msp.org
or by using our
contact form.
Or, you may purchase this single article for
USD 40.00:
Milestones
Received: 30 March 1977
Published: 1 September 1979
|
|
