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