Newest at the top
| 2026-01-16 00:28:51 +0100 | <jreicher> | And so SillyType is countable, yes? |
| 2026-01-16 00:27:29 +0100 | <monochrom> | I map 0 to the infinite stream z = I z, 1 to bottom, 2 to I bottom, 3 to I (I bottom), etc. |
| 2026-01-16 00:26:51 +0100 | <jreicher> | Every proof I sketch out results in an inconsistency. |
| 2026-01-16 00:26:25 +0100 | <jreicher> | No, prove away, please. I'd like to understand. |
| 2026-01-16 00:26:11 +0100 | <monochrom> | I can prove them, but if you're asking for intuition, I think I don't have any. |
| 2026-01-16 00:25:59 +0100 | <jreicher> | Surely they're either both countable, or both uncountable, depending on your "definitions" |
| 2026-01-16 00:25:35 +0100 | <jreicher> | I still don't understand why anyone would say SillyType is countable but BitStream is uncountable. |
| 2026-01-16 00:20:22 +0100 | <EvanR> | imaginary numbers are real and real numbers are fictional |
| 2026-01-16 00:20:08 +0100 | <monochrom> | My beef is that "imaginary number" is a misnomer. But I digress. |
| 2026-01-16 00:20:04 +0100 | <jreicher> | Fictionalists unite |
| 2026-01-16 00:19:48 +0100 | <EvanR> | lol |
| 2026-01-16 00:19:43 +0100 | <int-e> | EvanR: "real number" is a misnomer :P |
| 2026-01-16 00:19:40 +0100 | <EvanR> | I'm doing vibes there |
| 2026-01-16 00:19:29 +0100 | <jreicher> | I'm really not doing vibes, so I don't know why you keep saying that |
| 2026-01-16 00:19:26 +0100 | <EvanR> | at least approximately |
| 2026-01-16 00:19:21 +0100 | <EvanR> | well you know where infinitesimals are |
| 2026-01-16 00:19:08 +0100 | <EvanR> | if were doing vibes, this kind of defeats the point of the real line, and the idea of quantity or ordering |
| 2026-01-16 00:19:05 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2026-01-16 00:19:04 +0100 | <jreicher> | I'm pretty sure non-standard analysis does this with asserting the existence of infinitisimals |
| 2026-01-16 00:18:19 +0100 | <jreicher> | yes of course. :) |
| 2026-01-16 00:18:11 +0100 | <EvanR> | at least approximately |
| 2026-01-16 00:17:49 +0100 | <EvanR> | but it would seem kind of odd that these objects don't "sit" somewhere on the real line xD |
| 2026-01-16 00:17:34 +0100 | <EvanR> | I don't doubt you can throw exotic objects in |
| 2026-01-16 00:15:49 +0100 | <jreicher> | I never have |
| 2026-01-16 00:15:43 +0100 | <dolio> | So you can't assume that real numbers are the same things as expansions. |
| 2026-01-16 00:15:43 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-16 00:15:39 +0100 | Googulator69 | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-16 00:15:12 +0100 | <jreicher> | I'm not confused about that. Every bitstream can be interpreted as a numeral corresponding to a number. But that says nothing about the converse, especially since nothing stops you from throwing in all kinds of exotic objects to the set you want to call "the reals" |
| 2026-01-16 00:15:08 +0100 | <dolio> | Yeah, like I said, there's a paper about a topos where the reals are countable. But the diagonal argument holds in every topos. |
| 2026-01-16 00:14:38 +0100 | <EvanR> | if you didn't guess already the argument in the paper is answering "no" to its title... like betteridge's law |
| 2026-01-16 00:14:36 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 00:14:22 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:14:20 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-16 00:13:49 +0100 | <EvanR> | if you keep getting confused thinking stream of bits means "oh reals", and reals means "oh, just a binary expansion", then that equivocation is the point of this old paper |
| 2026-01-16 00:12:35 +0100 | <EvanR> | that's specifically about reals |
| 2026-01-16 00:12:26 +0100 | <EvanR> | that was being discussed |
| 2026-01-16 00:12:19 +0100 | <EvanR> | you brought up chaitin |
| 2026-01-16 00:12:08 +0100 | <jreicher> | Yes, which is why I wasn't entirely understanding why you provided that paper |
| 2026-01-16 00:11:48 +0100 | <EvanR> | you don't even need reals for that, since it's demonstrating uncountability of *something*, in this case just streams of bits |
| 2026-01-16 00:10:17 +0100 | <jreicher> | (Because you don't need every real number to have a decimal/binary expansion for that construction) |
| 2026-01-16 00:08:48 +0100 | AlexNoo | (~AlexNoo@5.139.232.54) |
| 2026-01-16 00:08:26 +0100 | AlexNoo | (~AlexNoo@5.139.232.54) (Read error: Connection reset by peer) |
| 2026-01-16 00:07:57 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) |
| 2026-01-16 00:07:42 +0100 | Googulator | (~Googulato@2a01-036d-0106-29ac-fd48-b0ea-63d3-602a.pool6.digikabel.hu) (Quit: Client closed) |
| 2026-01-16 00:07:38 +0100 | <jreicher> | EvanR: you mean the construction of diagonalisation? |
| 2026-01-16 00:07:32 +0100 | <EvanR> | except skipping the reals |
| 2026-01-16 00:07:24 +0100 | <EvanR> | xD |
| 2026-01-16 00:07:22 +0100 | <EvanR> | we just did that |
| 2026-01-16 00:06:49 +0100 | <TMA> | mapping digit sequences of countably infinite lenght to real numbers is a classic way to show that {0,1}^* (or {0..9}^*) is not countable set |
| 2026-01-16 00:06:38 +0100 | <EvanR> | remarks about about the "construction" hinging on obtaining a digital expansion of any real number |