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.
I don’t have much time to look into this now, but this equivalence should be reconciled with the statement made just before this section, that LEM isn’t implied by CSB if we consider topos models. Perhaps I was missing some subtlety when I first wrote that (I think it was me).
Interesting, I didn’t see that remark! I think the point is that Pradic-Brown’s proof uses the natural numbers, while $FinSet^C$ doesn’t have a NNO. They remark on this very example in their footnote 5. This should be clarified on the page – but I don’t have time to do it right now.
Added mention of and link to
The proof on the mailing list uses a NNO, doesn’t it? Actually Freyd mentions there more or less the same counterexample otherwise. See also remark #3 above.
Nevertheless, since $FinSet^G$ is Boolean for any finite group $G$, one should replace ’any” with ’some’ in the nLab entry or use finite monoids that are not groups as counterexample in the footsteps of Freyd instead of mere finite cats.
Thanks Todd! I obviously completely misunderstood what Dusko wanted to say here, sorry for that!
Actually, I don’t think you did – he was making several points. FWIW, if he’s reading: the “nontriviality” of the power $C$ refers to the possibility that $Fin^C$ may be be non-Boolean – perhaps it would be better just to cite the specific example $C = \mathbf{2}$, although I think any finite non-groupoid would do.
I am still very embarrassed to have fed that semi-silly line to Dusko after his helpful comment. Concerning the second point I think it is ok to have the generality in the counterexample (which might be useful on other occasions) but as formulated it is a bit irritating and relies heavily on the reader’s collaboration (e.g. I was reading the ’nontriviality’ as $\mathcal{C}\neq 0,1$).
Huh, I thought I had announced the most recent edit – see if you think it reads better now. (You’re right – “nontrivial” was certainly suboptimal.)
Having posted my comments yesterday after already having called it a day, “as formulated” should be read as “as it was formulated a week ago”, meaning if you had already attended to the point no criticism of the altered version was intended. The current version sure looks ok to me!
I have also added a reference to Freyd’s proof.
Added reference to Dedekind’s proof
- {#Dedekind} Richard Dedekind (1932), Robert Fricke; Emmy Noether; Øystein Ore (eds.), Gesammelte mathematische Werke, vol. 3, Braunschweig: Friedr. Vieweg & Sohn, pp. 447–449 (Ch.62) Göttinger Digitalisierungszentrum
and prose mentioning the specific date and context of the proof. The previous text was the much more tentative “Wikipedia reports that”.
Regarding Cantor’s proof, I’m fairly sure he only originally proved the case of sets with cardinality $\leq \omega_1$ (in his 1883 Grundlagen). For finite sets its obvious, for infinite countable sets this is not too bad, and Cantor used sets equipped with a well-ordering iso to $\omega_1$ itself for the proof of the last case. In 1887 Cantor published the statement of the theorem for arbitrary sets but didn’t give a proof at all. In November 1882 Cantor wrote to Dedekind saying he didn’t know how to prove the result. Putting the general claim in his 1887 paper without finding a proof is a very gutsy move.
1 to 21 of 21