FOM: fom: IHOL

[Steve Awodey]

In resplonse to

>Date: Tue, 3 Feb 1998 14:24:10 -0500 (EST)
>From: Stephen G Simpson <simpson at math.psu.edu>
>Subject: FOM: categorical mis-foundations: real analysis; IHOL;
>simplicity; schemes
>
...
>
>   > 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.
>
>  (NNO := natural number object).  What do the topos people have to
>  say about this?  Is my surmise meaningful?  Is it correct?

As Carsten Butz in effect pointed out, the Mean Value Theorem is not
provable in an arbitrary topos with NNO, since it's not constructively
valid - and (as we're now beginning to agree) general topos theory is
equivalent to IHOL (in this case, the equivalence relates topos + NNO and
higher-order, intuitionistic Peano arithmetic).  If you still object to
this notion of equivalence, we can instead say something "intertranslatable
with preservation of validity".  If you add the law of excluded middle on
the logical side you get classical higher-order arithmetic, and the theorem
is then of course provable, and it's then also provable in any boolean
topos.  Thus the simple answer to:

>If it is
>  correct, what additional axioms are appropriate to prove this and
>  other basic theorems of real analysis?

is: Excluded Middle (resp. boolean topos).

>How does all this affect the
>  project of "categorical foundations"?

Not at all.  By the way, the axioms Colin stated included booleanness (as a
consequence of well-pointedness).

>IHOL:
>
>  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.

Good, I'm glad that's cleared up.

>  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.

Yes, that's the way Butz explained it.

>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.

Note that I said "will be "the same" theory as T , _up_to_ ..." which was
maybe not a clear way of saying "the two differ at most with regard to ...
"  I free admit that I consider the difference insignificant for most
purposes.

>  I think the real difficulty here is that the topos people are
>  algebraists at heart

There is a sense in which this is quite true.  In passing from T to
T(E(T)), what is lost is the particular choice of generators and relations,
in the usual algebraic sense.  You are saying that _that_ particular choice
is significant, I'm saying it's the algebraic object itself that counts,
and not the generators and relations.  Note that I don't loose the fact
that T(E(T)) is finitely generated (if T is) - only the distinction between
two different choices of primitives and axioms.  Your remark:

> obviously a lot of structure has been lost

is not obvious to me, unless you just mean this structure of a particular
choice of generators and relations (i.e. primitives and axioms).  I'm
indeed happy to forget _that_ structure.

Steve Awodey