Newest at the top
| 2026-01-15 23:57:10 +0100 | <int-e> | (The arrow there is very much informal.) |
| 2026-01-15 23:55:58 +0100 | <int-e> | ...probability". |
| 2026-01-15 23:55:52 +0100 | <int-e> | dolio: Basically you define a prefix code {0,1}^* -> Turing machines. And you map the reals [0,1) to Turing machines via binary expansion and matching a prefix. Assign a non-halting TM to anything that doesn't match a prefix. So now you have a subset of R that corrsponds to halting Turing machines, and you can show classically that it's measurable with measure <= 1. Call that measure "halting... |
| 2026-01-15 23:54:09 +0100 | <EvanR> | instead accidentally |
| 2026-01-15 23:54:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:54:01 +0100 | fp | (~Thunderbi@89-27-10-140.bb.dnainternet.fi) (Ping timeout: 264 seconds) |
| 2026-01-15 23:53:19 +0100 | <EvanR> | or it intrinsically requires an unrestricted choice principle |
| 2026-01-15 23:52:46 +0100 | <dolio> | I'm not that familiar with what it even does, exactly. You can have a halting relation for Turing machines, but that relation will lack properties that would allow constructing a corresponding real number. |
| 2026-01-15 23:52:39 +0100 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2026-01-15 23:52:23 +0100 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Remote host closed the connection) |
| 2026-01-15 23:52:08 +0100 | <EvanR> | because you can often backport the insights you got from constructive math back to classical and realize it was bogus all along |
| 2026-01-15 23:51:53 +0100 | <EvanR> | sometimes that's not the discriminator |
| 2026-01-15 23:51:28 +0100 | <monochrom> | But in this context we only need two: classical math, constructive math |
| 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. |