On Mon, 10 Dec 2007, Lutz Schroeder wrote:
Here's another one of these internal/external questions: the fact that an object N with structure map a: N + 1 -> N in a topos is an NNO can be expressed by axioms
ALL d: B + 1 -> B. EX! f: N -> B. f a = d (f + 1)
for every object B, where the quantifiers are external, i.e. range over all morphisms. Does it follow that these formulas hold also internally, i.e. in the internal logic of the topos? (The universal quantifier implicit in the EX! can, of course, be internalised, as a is an isomorphism by Lambek's lemma. I mean the outer universal quantifier for d.)
The answer is yes; and it follows from the fact that if N is a NNO in E then B^*N is a NNO in E/B, for any B. (This depends on the fact that E is cartesian closed; cf. Remark A2.5.3 in the Elephant.) What is perhaps more remarkable is that an object in a topos satisfies "Peano's induction postulate" internally iff it does so externally (cf. Elephant, D5.5.1): that is, one can replace an internal quantification over PN by an external quantification over Sub(N). Peter Johnstone