Does anybody know what is meant by the statement that is “functorial” on sets? (I suppose you could take the core groupoid on , and consider ordinals and their isomorphisms as forming an essentially discrete category, but in that case there is not much content to the statement.)
I suppose the sentiment is that the operation is “structural” (an operation on sets, not numbers) in some sense…
]]>Assuming the axiom of choice (countable choice and excluded middle are enough), we have as a cardinal.
What’s the definition of in this context? And presumably is the Hartogs number of the natural numbers?
]]>Added a proof for a claim in the Properties section.
]]>Clarified the proof of non-existence of an injection from the Hartogs of a set into that set.
]]>Yes, I was trying to think if we can parallel the diagonal argument a bit more closely, in that given a function we can construct an element not in its image (and analogously for other cases). But the proofs all work by assuming surjectivity, then arriving at a contradiction. The case for the ordinary Hartogs number really does require Choice as well, since it’s possible for a set to surject onto its Hartogs number under the negation of AC.
]]>I expect that that gives an ordinal definable in any topos with the property that doesn’t surject onto it. However, it’s not clear to me that one will be able to do very much with it beyond that; even the ordinary Hartogs number doesn’t seem to be very useful without LEM, since its defining property is purely negative.
]]>To answer your question, Mike, I think I’m after something that would work at least in any topos with nno. Defining the thing shouldn’t be a problem, it’s proving it has the desired properties that makes me pause.
And something that is more predicative would be good. I mean, what sort of ’cardinals’ can one construct in an arithmetic universe, for instance? Or less ambitiously, in a -pretopos with nno?
]]>Actually, I found one reference that defines a “surjective Hartogs number” of a set as being the set of ordinals admitting a surjection from . With LEM this would be the same as the set of ordinals that are subquotients, so it’s reasonable. And for all sets, with for well-orderable .
]]>How constructive/predicative are you trying to be? LEM (no AC) suffices for to be classically well-ordered.
Taking the supremum of all well-ordered quotients or subquotients does seem an obvious dual of the Hartogs construction, but I haven’t thought about whether it works.
]]>And this MO question discusses the dual notion
is defined as the least ordinal such that there exists no surjection with a subset of .
however this uses the well-ordering of and seems rather impredicative. For the case of there’s no problem, as the question indicates that returns the usual Hartogs number given a well-ordered set, but conceptually it’s messy.
Maybe something like taking the supremum of all well-orderings of subquotients of my given set? This seems better.
]]>Hmm, this MO question tells me that one can have surjecting onto in the absence of AC. So it would have to be some other type of construction. I was thinking about and , and how constructive the proof is that has the properties it has, from different points of view. Certainly seems ok, but was thinking about the ordering, which is the one that the diagonal argument uses to show is smaller than .
]]>I’ve been looking around and can’t find the following. Given a set , a “least” set such that does not surject onto . The Hartogs number doesn’t quite work, because it’s a least set such that does not inject into . With AC, given a surjection , take a section, hence an injection , which can’t exist. But without AC it’s not clear, let alone without EM.
The library lost its copy of Practical Foundation of Mathematics, and I suspect something like it could be in there (it is buying another copy).
]]>Added the proof that the Hartogs of doesn’t inject into .
]]>I added a few more examples (equivalent forms of AC) to Hartogs number, to illustrate the kinds of things you can do with it.
]]>Localised to alephs? Of course, ’local’ has a fairly established meaning in set theory as well, which is better suited to specific instances of CH at a given set/cardinal.
]]>“global” to me implies that the other one would be “local” in some way, which doesn’t seem to be the case.
]]>As for the nomenclature, I have no strong opinions. I’m fine with implementing the proposed theorem in #14 if agreement is reached.
I’m pretty sure BZ suffices. Each subset of equipped with a well-ordering is uniquely specified by its set of principal ideals or downsets, i.e., an element of . An equivalence class of well-orderings is then a subset of or an element of , so the set of equivalence classes is a subset of as advertised. There is no funny business with unbounded quantifiers or replacement that I can see anywhere; everything is locally definable. This is probably worth a remark at Hartogs number.
]]>Also: is the full strength of ZF even used? The argument looks like it could be done in BZ.
]]>The latter should be ’global CH’, since it applies to all sets, and the traditional ’G(eneralised )CH’ can be saved for the version with only alephs.
]]>Thanks!! Dedekind-infiniteness is definitely an unexpected gotcha: you expect that constructive mathematics may have trouble defining “infinite”, but it’s surprising (to me) that even in ZF there’s some ambiguity left in what you mean by “infinite”.
Morally, I feel like and ought to have two different names, like “weak GCH” and “strong GCH”. Then the theorem would be that strong GCH is equivalent to the conjunction of weak GCH and AC.
]]>And finally (Mike), I added some remarks to continuum hypothesis to cover the point you brought up in #9. Sierpinski of course uses the stronger form of GCH.
]]>Okay, I just consulted Wikipedia, and yes you’re right that Dedekind-infinite and infinite are distinct in ZF in classical logic. (Live and learn.) However, the patch is easy: just embed into a Dedekind-infinite set like , and take the power set of that. The proof then goes through. I’ll put the patch in now.
]]>As for #9: I don’t know the history, but maybe someone should check on Sierpinski’s article. You again raise an interesting point.
]]>