>>12180270Okay, thanks, I get a feel for it now. Hopefully I'll not forget it too soon, though.
But still, it feels like there's some vague tie to ideas. Especially in how the cofinality of jumps between big and small when you're on a successor vs. a limit in the the ordinal. Although I don't really know what ordinals are between such alepha.
>>1218030627:15 - 31:15
is fun to watch
>>12181337There's nothing wrong with working explicitly without the excluded middle, I don't know why this is so misunderstood.
Let be the functions on the naturals.
Let be the functions that can be coded up (in C++, say).
Let be the functions that, on the inputs 0 say, are total / terminating / computable (excludes e.g. infinite while-loops).
Let be an enumeration of all codes.
Let be the index set of terminating functions.
The property of termination is not decidable, i.e. provably there’s no algorithm that you could give any C++ code so that it tells you whether it would terminate
So cannot be decidable either.
As a result, there is no computable surjection
.
As a result, there is no computable surjection
.
If you want to logically reason about this scenario, then you must tune your logic to respect this situation.
LEM plus a few set theory axioms imply that any infinite subsets of the nats is in bijection with it, but this is misleading. If ZF proves some set is "countable", then this word just means a formal existence statement
It's similar to a choice
principle.To claim that every infinite subset of the naturals is "countable" is merely to adopt this as an axiom. Not that there's anything wrong with it.
