Newest at the top
| 2026-01-15 23:51:05 +0100 | <jreicher> | dolio: I haven't heard the view that Chaitin's omega is not a real number. Interesting. What kind of object is it then? |
| 2026-01-15 23:50:57 +0100 | <monochrom> | hehe me too |
| 2026-01-15 23:50:49 +0100 | <c_wraith> | as if I only use a single meaning |
| 2026-01-15 23:50:30 +0100 | <monochrom> | Ugh. But everybody uses a different meaning for "exists"! |
| 2026-01-15 23:50:25 +0100 | <jreicher> | Normal people then. :p |
| 2026-01-15 23:50:14 +0100 | <EvanR> | everybody doesn't sound right... |
| 2026-01-15 23:50:01 +0100 | <jreicher> | EvanR: :D I'm just trying to use the word "exists" the same way everybody else does |
| 2026-01-15 23:49:47 +0100 | <dolio> | It's not a real number, at least. |
| 2026-01-15 23:49:33 +0100 | <EvanR> | you said you weren't a platonist! |
| 2026-01-15 23:49:29 +0100 | michalz | (~michalz@185.246.207.205) (Remote host closed the connection) |
| 2026-01-15 23:49:18 +0100 | <jreicher> | So you don't believe something like Chaitin's omega exists? |
| 2026-01-15 23:49:05 +0100 | <dolio> | That is the premise, at least. We are in the world where everything is inherently computable. |
| 2026-01-15 23:48:58 +0100 | <EvanR> | which definition are you having issues with again |
| 2026-01-15 23:48:43 +0100 | mange | (~mange@user/mange) mange |
| 2026-01-15 23:48:41 +0100 | <jreicher> | Oh. I haven't heard that view before. |
| 2026-01-15 23:48:29 +0100 | <dolio> | And I don't believe in uncomputable things. So the surjection is computable. |
| 2026-01-15 23:48:26 +0100 | <int-e> | if you dislike "countability" you can say that recursive functions are not recursively enumerable ;-) |
| 2026-01-15 23:48:12 +0100 | <dolio> | (Or similar) |
| 2026-01-15 23:47:50 +0100 | <EvanR> | Bitstream is uncountable (in haskell) <- |
| 2026-01-15 23:47:45 +0100 | <dolio> | Countability is 'there is a surjection from ℕ'. |
| 2026-01-15 23:47:29 +0100 | <jreicher> | Sorry, I mean computable enumeration |
| 2026-01-15 23:47:29 +0100 | jmcantrell_ | jmcantrell |
| 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 |