I wrote in part:
[...] ask of a topos with [...] whether the negation of X over N (the internal hom [0, X] taken in the slice category over N) can also be occupied.
I have one and a half things backwards here. First of all, of course negation is [X, 0] rather than [0, X]. (But in exponential notation, it is 0^X; that is my excuse.) Also, my placement of "can" implies that the relevant question is whether there ~exists~ a topos E (with given properties) and there exists an object X in E (with the properties that I described); rather, the question is whether for ~every~ E (with given properties) there exists an object X in E (with the properties that I described). Iff so, then the properties required of E are omega-inconsistent. (Iff E must be a terminal category, then they are simply inconsistent. Thus omega-inconsistency is weaker than inconsistency, and omega-consistency is stronger than mere consistency.) --Toby
I wrote in part:
given a morphism X -> N whose pullbacks 0, 1, 2, ...: 1 -> N are all occupied [...]
Another typo; the word "along" is missing; it should be
given a morphism X -> N whose pullbacks along 0, 1, 2, ...: 1 -> N are all occupied [...]
So: Given a collection of conditions on a locally cartesian-closed category E with an initial object 0, a final object 1, and a natural-numbers object N (various refinements should be possible for more general theories), these conditions are _omega-inconsistent_ if in every such E there exists an object X and a morphism p: X -> N such that: * defining the numerals [i]: 1 -> N using the stucture maps of N (so [0]: 1 -> N, [1]: 1 -> N -> N, [2]: 1 -> N -> N -> N, etc) and letting X_i be the pullback of p: X -> N and [i]: 1 -> N, each X_i has a morphism a_i: 1 -> X_i; * letting [X,0]_N be the internal hom from X to 0 in the slice category E/N, there is (in E itself) a morphism b: 1 -> [X,0]_N. I've read this 5 times, in different orders, so there should be no mistakes. I apologise for any confusion from my abbreviations and corrections. --Toby
participants (1)
-
Toby Bartels