Newest at the top
| 2026-01-15 23:47:16 +0100 | <jreicher> | dolio: but why is enumeration important here at all? What's the connection with uncountability, for you? |
| 2026-01-15 23:46:38 +0100 | <jreicher> | I know what the definitions and theorems are in classical maths. I don't have a problem with any of that. |
| 2026-01-15 23:46:37 +0100 | <dolio> | The reason the 'program text' thing won't work is that the computable bit streams are (at best) a quotient of program texts. So being able to enumerate program texts won't help you enumerate all the bit streams. |
| 2026-01-15 23:46:32 +0100 | <EvanR> | instead yeah lets understand it on its own terms |
| 2026-01-15 23:46:17 +0100 | <EvanR> | for whatever reason you don't like the result, even though it jives exactly with classical math xD |
| 2026-01-15 23:46:16 +0100 | <jreicher> | At the moment I'm just trying to understand dolio's definitions |
| 2026-01-15 23:45:49 +0100 | <EvanR> | jreicher, you're working on the level of vibes it seems... instead of defining stuff, then proof a theorem |
| 2026-01-15 23:45:33 +0100 | jmcantrell_ | (~weechat@user/jmcantrell) jmcantrell |
| 2026-01-15 23:45:31 +0100 | <jreicher> | I don't really understand why that serves as a meanginful notion of uncountability |
| 2026-01-15 23:45:30 +0100 | <EvanR> | it's valid in of itself |
| 2026-01-15 23:45:26 +0100 | <EvanR> | whatever the proof means, the proof goes through |
| 2026-01-15 23:45:22 +0100 | <dolio> | Because constructive mathematics is valid for computability. |
| 2026-01-15 23:45:09 +0100 | <dolio> | jreicher: Something like that. Maybe it's backwards. The constructive proof of its uncountability 'means' that the computable bit streams are not computably enumerable. |
| 2026-01-15 23:44:33 +0100 | <tomsmeding> | :D |
| 2026-01-15 23:44:27 +0100 | <int-e> | tomsmeding: It's in the nature of IRC that discussions become circular, for better or worse. |
| 2026-01-15 23:44:08 +0100 | <jreicher> | dolio: You're saying that because the set of computable numbers is not itself computably enumrable, that it's "constructively" uncountable? Something like that? |
| 2026-01-15 23:44:02 +0100 | <EvanR> | we're not going to get less bitstreams that way |
| 2026-01-15 23:43:53 +0100 | <EvanR> | if I hook up my Bitstream generator to an external entity then it only makes matters worse |
| 2026-01-15 23:43:50 +0100 | <int-e> | tomsmeding: Ah sorry, I'm not complaining! |
| 2026-01-15 23:43:25 +0100 | <tomsmeding> | int-e: right -- I haven't really been following the discussion. You know what, I'll leave you at it :) |
| 2026-01-15 23:43:15 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2026-01-15 23:42:59 +0100 | <EvanR> | another way to say that, already said, Bitstream is uncountable (in haskell). (Assuming a lot about what kind of haskell you are allowed to write) |
| 2026-01-15 23:42:51 +0100 | <int-e> | tomsmeding: But the only reason we are in this mess is that we pretend that "everything" is computable. As I said earlier, you need to be very clear about object and meta levels for this discussion to be meaningful. |
| 2026-01-15 23:42:34 +0100 | <tomsmeding> | this is not classical set-theoretical "countable", this is "computably countable" |
| 2026-01-15 23:42:28 +0100 | <dolio> | If you want to say there's a non-computable enumeration, you have again exited constructive mathematics. |
| 2026-01-15 23:42:08 +0100 | <dolio> | Yeah. |
| 2026-01-15 23:42:03 +0100 | tomsmeding | . o O ( every _computable_ enumeration -- that bit is relevant here ) |
| 2026-01-15 23:41:34 +0100 | <EvanR> | jreicher, I went over that in a few ways above |
| 2026-01-15 23:41:05 +0100 | <EvanR> | a proof is worth 1000 words |
| 2026-01-15 23:41:00 +0100 | <dolio> | Cantor's diagonal argument shows every computable enumeration of the computable bit streams misses a computable bit stream. |
| 2026-01-15 23:40:55 +0100 | <jreicher> | "computable" can be understood as "generated by a program", and all program texts are finite. So the set of all program texts is countable, and so is the set of computable outputs |
| 2026-01-15 23:40:45 +0100 | <EvanR> | at some point doing the proof might help since this is ... mathematical |
| 2026-01-15 23:40:24 +0100 | <dolio> | No, it isn't. |
| 2026-01-15 23:40:15 +0100 | <jreicher> | And if you only have the computable ones, the set is countable. |
| 2026-01-15 23:39:04 +0100 | <dolio> | They aren't. We only need the computable ones. |
| 2026-01-15 23:38:52 +0100 | <EvanR> | at that time, it wasn't appreciated the subtleties that binary streams created for defining reals... but a stream of bits is pretty simple |
| 2026-01-15 23:38:44 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:38:42 +0100 | <jreicher> | dolio: Ok, I'll stick to bistreams. In what way is a non-computable (infinite) bitstream "constructive"? |
| 2026-01-15 23:38:22 +0100 | <monochrom> | I think GCC for DOS could do 32-bit in real mode. I forgot. But just do whatever GCC-for-DOS does. |
| 2026-01-15 23:38:21 +0100 | <jreicher> | To begin with I'm pretty sure he was |
| 2026-01-15 23:38:18 +0100 | <dolio> | Even though the bit streams are uncountable. |
| 2026-01-15 23:38:10 +0100 | <EvanR> | was cantor even talking about real numbers |
| 2026-01-15 23:38:06 +0100 | <dolio> | It's actually possible for the (Dedekind) reals to be countable in constructive mathematics. |
| 2026-01-15 23:38:04 +0100 | <EvanR> | yes that is what this whole discussion is about |
| 2026-01-15 23:38:01 +0100 | <jreicher> | (Maybe I've misunderstood the idea) |
| 2026-01-15 23:37:56 +0100 | <jreicher> | EvanR: how can you have Cantor's diagonalisation without the reals? |
| 2026-01-15 23:37:33 +0100 | <EvanR> | lol |
| 2026-01-15 23:37:31 +0100 | <dolio> | jreicher: Like 0.11111... = 1.0 (binary). |
| 2026-01-15 23:37:30 +0100 | int-e | runs |
| 2026-01-15 23:37:28 +0100 | <int-e> | (so *now* we're getting off topic, huh) |