FOM: categorical mis-foundations: real analysis; IHOL; simplicity; schemes
Stephen G Simpson
simpson at math.psu.edu
Tue Feb 3 14:24:10 EST 1998
I'd appreciate it if Awodey, McLarty, or some other topos person would
comment on a specific technical point, which I have raised several
times (postings of 18 Jan 1998 14:39:24, 26 Jan 1998 12:15:34, perhaps
others). I wrote:
> Consider the standard undergraduate calculus theorem saying that
> every continuous real-valued function on [0,1] has a maximum
> value. .... I surmise that it's a difficulty for "categorical
> foundations", because it's probably not provable in topos plus
(NNO := natural number object). What do the topos people have to
say about this? Is my surmise meaningful? Is it correct? If it is
correct, what additional axioms are appropriate to prove this and
other basic theorems of real analysis? How does all this affect the
project of "categorical foundations"?
Note: In the above, when I say "appropriate axioms", I'm not
necessarily asking for the sharpest possible results, a la reverse
mathematics. I'm only asking for a broad-brush portrait of how the
alleged "categorical foundations" would actually work. Is this too
much to ask? Is it a wrong-headed question?
I've had a look at the Lambek/Scott book and I can confirm that, as
Awodey 1 Feb 1998 15:35:54 said,
> there's nothing sneaky going on.
In other words, IHOL as defined there really can be viewed as a kind
of intuitionistic higher order logic, complete with propositional
connectives and quantifiers. So my earlier suspicions about the
topos-theoretic meaning of IHOL were not correct.
On the other hand, Awodey writes:
> if you start with a theory T in IHOL and take the topos E(T) it
> generates, then take the theory T(E(T)) associated to that topos,
> the result will be "the same" theory as T , _up_to_ the kind of
> syntactical intertranslatabilty which obtains between the theories
> of boolean algebras and boolean rings. (I would regard this as a
> syntactic isomorphism.) The composite operation E(T(-)) has an
> analogous property.
and I find this unacceptable. Although Awodey's remark is not very
clear, I think what's going on is that T(E(T)) is something like a
maximal extension by definitions of T. In particular, the carefully
selected primitives of T have been submerged in a sea of additional
primitives, so obviously a lot of structure has been lost, and I
don't see how Awodey can honestly say that T is "the same" as
T(E(T)). They may be "the same" from the viewpoint of topos theory,
i.e. yield isomorphic toposes, but they are certainly not "the same"
from the viewpoint of logic. In general, they are very different as
logical theories; for example, the signature of T may be finite,
while the signature of T(E(T)) is infinite.
I think the real difficulty here is that the topos people are
algebraists at heart and simply don't appreciate the foundational
importance and motivation of things like intuitionistic logic. As
if to confirm this, Awodey writes:
> As for the question of motivation, I for one am happy to invoke the
> inference that Simpson recently "suggested": If X is equivalent Y,
> and X is well-motivated fom, then so is Y. Here using the notion
> of "equivalence" that was just considered.
Regarding the question of measures of simplicity of the ZFC axioms,
> I've already mentioned one measure of simplicity that I consider
> significant, and under which the topos axioms are notably simpler
> than those for ZFC.
What measure was that?
For the record, to correct McLarty's comment in his posting of 2 Feb
1998 15:29:42, I definitely *did not* misunderstand Harvey
Friedman's fully formal axiomatization of ZFC. I rightly understood
the replacement scheme as a scheme. I regard schemes as part of the
normal apparatus of first-order logic, i.e. schemes are something
that we have to teach in basic mathematical logic courses, because
of their use in things like Peano arithmetic, the axioms for a real
closed field, etc. Harvey's use of schemes should not be regarded
as a disadvantage with respect to complexity, because schemes are
part of the standard logical apparatus.
More information about the FOM