FOM: categorical mis-foundations: real analysis; IHOL; simplicity; schemes

[Stephen G Simpson]

Real analysis:

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

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

Simplicity:

  Regarding the question of measures of simplicity of the ZFC axioms,
  Awodey writes:
  
   > 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?

Schemes:

  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.

-- Steve