A question for Paul Taylor. Are the countable ordinals countable? Count-erintuitively, no. That would be a set that is a member of itself. My question for Paul is, in your approach to ZF, can you prove this as succinctly? After all, maybe the above proof is exploiting V = L, and maybe another Paul, Paul Cohen, can somehow force the countable ordinals to be countable. That's where Hartogs' theorem comes in handy, as Paul and others have pointed out back in the day. I do appreciate the search for shorter proofs, in particular what yet another Paul, Paul Erdős, has called the proof in The Book. Satan's proof of 1+1=2 can be found spread over the first two volumes of Whitehead and Russell's Principia Mathematica. I like the proof that writes natural numbers in Roman numerals, which use concatenation to denote addition instead of multiplication. It is then easily seen that II = II. The proof generalizes to III = III, and to IIII = IIII with clock Roman numerals.. It further generalizes by simplifying the Roman numerals, namely by omitting V, X, L, C, D, etc., obliging the Roman numerals to be the free monoid on a one-letter alphabet, provided we accept = as a theorem about natural numbers. I also appreciate Paul's translation of Friedrich Hartogs' 1915 paper, which I added to the references of the relevant Wikipedia article this morning. A second question. Who first pointed out the applicability of Hartogs' theorem to treating ordinals in the internal logic of a topos? Paul? Vaughan Pratt You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=files&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/groups/groupsubscription?source=EscalatedMessage&action=leave&smtp=categories%40mq.edu.au&bO=true&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>