[eigenket]

Aleph 1 turns up when you try to (very) formally deal with probability theory, specifically when dealing with probability measures over the reals. This is sort of useful for physics for example when trying to be very careful about operators like position and momentum in quantum mechanics but it isn't really central. Its sort of nice to know you can do this stuff "properly" but physicists don't care much.

[Vecr]

It's arguable that there's no such thing as a probability measure over the reals, because Solomonoff induction only works over computable programs, and the reals (in the sense needed) are not computable.

[eigenket]

I think such an argument would need quite a lot more work, the lack of Solomonoff induction doesn't mean we don't have probability theory.

[Vecr]

No, I mean even if you had (perfect, non-approximated) Solomonoff induction, you could only generate probabilities for computable "theories" (programs that predict all your past and future input), but I suppose it's possible that the impossibility proofs actually depend in some way on Aleph 1, so you would need it for consistency.