Volume 106, 1990
Some Theories Conservative over Intuitionistic Arithmetic
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.
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
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
Subsequently the author showed that
is conservative over HA, and pointed
out that a similar result for one of Feferman's theories (without join) is rela-
was discovered independently by several authors that Martin-
(the one without "universes") is also conservative over HA.
See Beeson  (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
$.25 per page