[FOM] one way up via interpretability?

[Matthew Frank]

On Oct. 28, Harvey Friedman wrote:
(http://www.cs.nyu.edu/pipermail/fom/2003-October/007596.html)

> IN THE NATURAL WORLD of systems that come up in math. logic/f.o.m.,
> provided S,T contain a tiny amount of stuff, we do seem to have:
> S is interpretable in T, or T is interpretable in S.

Consider the axiom systems in ch. VII of Moerdijk and Reyes's "Models for
Smooth Infinitesimal Analysis", and their fragments:  they do not
obviously fall into this pattern.  I have asked experts on the subject
(Ieke Moerdijk and Erik Palmgren) about how how these theories relate to
the standard hierarchy; they do not know and regard the question as
difficult.  

These particular systems are interesting for the above issue because:

1) they use intutionist logic, and are inconsistent when classical logic
is added, thanks to axioms like
(forall f)(exists unique g)(forall x,y) f(x)-f(y) = (x-y)g(x,y); 

2) they are strong in the quantifications which they use, but almost 
completely lack axioms of choice, and are weak in induction axioms
(only for formulas constructed from:  and, or, true, false, exists)

3) they are sufficiently natural and powerful that an interesting body of
mathematics (namely, Lawvere-style synthetic differential geomtery) can be
developed within them.

If anyone knows good results on the strength of these theories relative to
the standard hierarchies of theories, I'd like to hear about them.

--Matt