Subject: categories: Re : on the axiom of infinity

From: Thomas Streicher <[email-masked]>
Date: Wed, 31 Mar 2004 20:59:03 +0200 (CEST)

Dear Peter,

this story about ``infinity without infinity axiom'' is a bit confusing from
a (traditional) ``logical point of view''. Is the following reformulation in
accordance with what you mean?

In intutionistic higher order arithmetic (HAH), i.e. the logic of toposes
with NNO, it is consistent to assume that N is a subobject of P^2(Om). Even
more it is consistent to assume (as explained in the last section of part D
of the Elephant) that N is (isomorphic to) the orbit Orb(Phi) arising from
the Phi : P^2(Om) -> P^2(Om) whose least fixpoint is K(Om) \in P^2(Om) (the
Kuratowski finite subsets of Om). In a logical formula one would formulate
this as

          (InF)     Phi has no fixpoint in Orb((Phi)

where InF stands for ``Infinity `a la Freyd''. Evidently HAH does not prove
(InF) because it is inconsistent with classical HAH. But, of course, in
HAH + InF  one can construct a NNO as a subobject of P^2(Om). In other words
T/InF has a NNO (where T is the free topos without arithmetic).

For me HOL + InF (where HOL is *pure* higher order intuit.logic) looks like
a strengthening of HAH which is inconsistent with classical logic rather than
``getting infinity out of pure logic'' (as the logicists were aiming at).

Of course, you get more than mere consistency of HOL + InF because you have
that  Gamma(Orb(Phi))  is actually the rig of natural numbers in Set (where
Gamma = T(1,-) : T -> Set) but inside T one hasn't access to this nice fact
and, therefore, cannot really make use of it.

There arises the question to which extent HOL + InF (or equivalently HAH + InF)
is conservative over HAH. Is it the case that every formula of HA (i.e.
intuit. first order arithmetic) is provable already in HAH whenever it is
provable in HAH + InF?  Clearly, w.r.t. higher order arithmetic formulas
HAH + Inf is not conservative over HAH because InF is not provable in HAH.
But, of course, one might ask whether HAH + InF is conservative over HAH
w.r.t. 2nd order formulas of arithmetic. (These are a good measure because
up to some (admittedly somewhat nasty) coding a fair amount of analysis is
expressible in this fragment.) There is no end to questions like these
because one might also ask whether HAH + InF is conservative over HAH w.r.t.
formulas of HA^\omega, i.e. first order intuit. logic over G\"odel's T.
(HA^\omega is a typical system employed by people doing constructive analysis.)

But first things first. Does it follow from your result(s) whether HAH + InF
is conservative over HAH w.r.t. first order arithmetic formulas?

Best, Thomas