Newest at the top
| 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 |
| 2026-01-16 00:06:03 +0100 | <jreicher> | EvanR: no, not the point of the paper, the point you are wanting to make by providing the paper |
| 2026-01-16 00:05:41 +0100 | <monochrom> | Leibniz would have loved that. |
| 2026-01-16 00:05:41 +0100 | <EvanR> | jreicher, the point of the paper? well that's in the paper, and relevant to the above story about chaitin's number |
| 2026-01-16 00:05:17 +0100 | <EvanR> | but hopefully now we can just state our systems and assumptions ahead of time and not debate vibes |
| 2026-01-16 00:05:01 +0100 | <EvanR> | resurrected way later |
| 2026-01-16 00:04:51 +0100 | <EvanR> | around 1940s debate of this sort died out |
| 2026-01-16 00:04:34 +0100 | <jreicher> | EvanR: OK.... Not sure what the point is? (And FYI I don't think classical math has won, but that's a debate for another day/channel) |
| 2026-01-16 00:04:27 +0100 | <EvanR> | no one will drive us out of the paradise cantor created for us |
| 2026-01-16 00:04:07 +0100 | <EvanR> | this was before classical math "won" and "asserted" "yes" xD |
| 2026-01-16 00:03:37 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 264 seconds) |
| 2026-01-16 00:03:16 +0100 | <EvanR> | early* |
| 2026-01-16 00:03:13 +0100 | <EvanR> | jreicher, classic article in the earth days of modern math, "does every real number have a decimal expansion" |
| 2026-01-16 00:03:12 +0100 | <dolio> | So even though the expansions are infinitely long, you only need to look at a finite portion. |
| 2026-01-16 00:02:27 +0100 | <dolio> | Hopefully each real number. |
| 2026-01-16 00:02:17 +0100 | <dolio> | Presumably the prefix code is going to be set up so that there's a unique prefix for each binary expansion. |
| 2026-01-16 00:01:58 +0100 | <monochrom> | Me is even finger-disobeys-brain. (How else do you think I mistyped "you" for "mean"?! :) ) |
| 2026-01-16 00:01:02 +0100 | <geekosaur> | damn, fingers ahead of brain again |
| 2026-01-16 00:00:53 +0100 | <geekosaur> | *infinite |
| 2026-01-16 00:00:48 +0100 | <geekosaur> | right, I was abbreviating "countably finite", thought that would be fairly obvious from the ongoing context |
| 2026-01-15 23:59:56 +0100 | <jreicher> | I misread what you wrote! You said "countable" and I read "finite" |
| 2026-01-15 23:59:47 +0100 | <jreicher> | Oh, sorry |
| 2026-01-15 23:59:10 +0100 | <jreicher> | geekosaur: that might take us back to the start of the debate. :) I think the consensus is that denoting semantics for infinitely executing programs "in principle" simplifies things |
| 2026-01-15 23:58:30 +0100 | <int-e> | I said "classically"> |
| 2026-01-15 23:58:24 +0100 | <geekosaur> | thinking informally, wouldn't a binary expansion have to be countable length? |
| 2026-01-15 23:58:12 +0100 | <jreicher> | (If you accept that the binary expansion exists in the first place) |
| 2026-01-15 23:58:00 +0100 | <dolio> | There's a ∀∃, but not a function, I think. |
| 2026-01-15 23:57:58 +0100 | <jreicher> | Well, the point of Chaitin's omega is that the binary expansion is not computable |
| 2026-01-15 23:57:54 +0100 | <int-e> | you have a set of measure 0 of real numbers that have two expansions. |
| 2026-01-15 23:57:49 +0100 | <dolio> | Or, there is no mapping from reals to binary expansions, I should say. |
| 2026-01-15 23:57:33 +0100 | <dolio> | Okay, so, not every real has a binary expansion. |
| 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) |