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.) Thanks, Lutz Schröder -- ------------------------------------------------------------------ PD Dr. Lutz Schröder office @ Universität Bremen: Senior Researcher Cartesium 2.051 Safe and Secure Cognitive Systems Enrique-Schmidt-Str. 5 DFKI-Lab Bremen FB3 Mathematik - Informatik Robert-Hooke-Str. 5 Universität Bremen D-28359 Bremen P.O. Box 330 440 D-28334 Bremen phone: (+49) 421-218-64216 Fax: (+49) 421-218-9864216 mail: Lutz.Schroeder@dfki,de www.dfki.de/sks/staff/lschrode ------------------------------------------------------------------ ------------------------------------------------------------- Deutsches Forschungszentrum für Künstliche Intelligenz GmbH Firmensitz: Trippstadter Strasse 122, D-67663 Kaiserslautern Geschäftsführung: Prof. Dr. Dr. h.c. mult. Wolfgang Wahlster (Vorsitzender) Dr. Walter Olthoff Vorsitzender des Aufsichtsrats: Prof. Dr. h.c. Hans A. Aukes Amtsgericht Kaiserslautern, HRB 2313 -------------------------------------------------------------
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
participants (2)
-
Lutz Schroeder -
Prof. Peter Johnstone