6 ms·
That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often
by milesrout 2y ago
That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often bolded or double struck as U+1D7DA) used to mean "the set with two elements" and those elements are often called 0 and 1.
- auggierose 2y agoIt is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} If you don't like the meaning of equality here, that is exactly my point. My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually. And the same is true for the "Curry-Howard" way of understanding proofs.