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