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 1∪a for a↪1 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 Set→Card 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