Contemporary Mathematics
Volume 106, 1990
Some Theories Conservative over Intuitionistic Arithmetic
MICHAEL BEESON
ABSTRACT. Several theories have been proposed for formalizing construc-
tive mathematics. These theories fall into three families: constructive set
theory (introduced by Myhill and Friedman), theories of types (introduced
by Martin-LOf), and theories of operations and classes (introduced by Fe-
ferman). Each family contains theories formulated with only "restricted
induction", and these theories all turn out to be conservative over intuition-
istic arithmetic HA. This paper deals primarily with Feferman's theories: the
main th.:orem is the conservativity over HA of the theory with elementary
comprehension and join. The technique is an analysis of cut-free proofs.
Introduction
This paper should properly be considered as a rather technical variation on
a striking theme. The theme is that there are several natural theories which
are mathematically strong, in that one can formalize a lot of ordinary math-
ematics in them in a natural way, and which are proof-theoretically weak,
in the sense that they are conservative over arithmetic. This phenomenon
was pointed out in Friedman [ 1977], where a constructive set theory was
given which was proved to be conservative for
llb
formulae over intuition-
istic arithmetic. Friedman showed that all essential parts of Bishop's book,
Foundations of Constructive Analysis,
could be formalized in his theory
B.
Subsequently the author showed that
B
is conservative over HA, and pointed
out that a similar result for one of Feferman's theories (without join) is rela-
tively easy.
It
was discovered independently by several authors that Martin-
lofs theory
ML0
(the one without "universes") is also conservative over HA.
See Beeson [1985] (p. 321) for precise statements and proofs of all these
results, as well as more detailed history and credits.
These results, however, left a gap between theories known to be conser-
vative over HA and theories which are clearly not conservative over HA. In
particular, Feferman's theory with elementary comprehension and join (but
1980 Mathematics Subject Classification ( 1985 Revision). Primary 03F05, 03F50.
The results of this paper were first presented at the Special Session on Proof Theory of the
joint AMS/ ASL meeting at Denver in December, 1983. This paper is in final form and no
version of it will be submitted for publication elsewhere ..
©
1990 American Mathematical Society
0271-4132/90 $1.00
+
$.25 per page
http://dx.doi.org/10.1090/conm/106/1057812
Previous Page Next Page