Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
However, if any finite set greater than 1 is choice, or if every 2-indexed set is projective, then the logic must be classical (see excluded middle for a proof).
I copied the above from finite set. I don’t like the phrase ’set greater than 1’, even though I know what it means. I gather we can’t say ’set with cardinality greater then 1’, because that assumes that cardinality is well-defined and perhaps is circular. What can we say instead of the existing phrase?
“with more than one element”?
Well, I feel it’s getting deep into ’Toby territory’ here, seeing as the finite set in question may have only one element but still not be isomorphic to 1. Say for a subterminal object. Unless I’m imagining levels of constructivism beyond the really there…
I gather we can’t say ’set with cardinality greater then 1’, because that assumes that cardinality is well-defined and perhaps is circular.
The only really sensible basic definition of a cardinal number is that a cardinal number is a set, with two cardinal numbers equal iff the two sets are bijective; any other definition may be useful but only if it is equivalent to this one. So cardinality is well-defined even if cardinal numbers might not be totally ordered, or if the surjection might not split, etc.
All of which is my way of saying that, even deep in my territory, I countenance using “cardinality” here if it helps you understand. But I probably didn’t use that word myself (assuming that I wrote the current wording at all, which I haven’t checked) because I expect readers of the nLab to interpret “bigger” in terms of cardinality anyway.
However, nothing wrong with clearer wording, so I’ve changed it.
Even constructively, a finite set always has a well-defined cardinality that is a natural number, essentially by definition of “finite.” If U is a nontrivial subterminal, then 1+U is not generally finite in this sense. It’s true that if our constructive logic is the internal logic of a topos, then 1+U has only one global element, but one cannot assert in the constructive logic itself that “1+U has only one element.”
Actually I was concerned about the use of the word ’bigger’
Fair enough; without choice (and especially without excluded middle), there are a few different ways that ‘bigger’ can be interepreted. So that’s why I changed to a more precise wording.
Thanks!
1 to 8 of 8