Newest at the top
| 2026-01-16 01:05:48 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-16 01:05:34 +0100 | trickard | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-16 00:58:57 +0100 | trickard_ | trickard |
| 2026-01-16 00:57:24 +0100 | <EvanR> | though if you want to get into that there's more exotic constructions |
| 2026-01-16 00:57:21 +0100 | <jreicher> | No, I know. I'm just picking out where the line is. |
| 2026-01-16 00:56:59 +0100 | <EvanR> | they're not needed to make the original point, just as in cantor |
| 2026-01-16 00:56:41 +0100 | <jreicher> | But not transfinite lists |
| 2026-01-16 00:56:17 +0100 | <EvanR> | turns out |
| 2026-01-16 00:56:16 +0100 | ttybitnik | (~ttybitnik@user/wolper) (Ping timeout: 256 seconds) |
| 2026-01-16 00:56:12 +0100 | <EvanR> | this is haskell an we have infinite lists |
| 2026-01-16 00:56:09 +0100 | <int-e> | Also has it really been 2 hours of this... |
| 2026-01-16 00:55:58 +0100 | <TMA> | jreicher: BUT there is just a single such string in the smallest model of the data SillyType = I SillyType theory |
| 2026-01-16 00:55:51 +0100 | <jreicher> | I'm not insisting anything of the sort. I also don't think they're analogous. I'm just trying to understand why. |
| 2026-01-16 00:55:43 +0100 | <EvanR> | jreicher, the original definition of Bitstream and SillyType both have nothing but infinite streams. Not really a double standard |
| 2026-01-16 00:55:43 +0100 | <Inline> | lol |
| 2026-01-16 00:55:38 +0100 | <Inline> | the egotist set |
| 2026-01-16 00:55:29 +0100 | <int-e> | jreicher: You're insisting that two things are analogous despite strong evidence to the contrary, all of which has been laid out in front of you above. |
| 2026-01-16 00:55:24 +0100 | <Inline> | aye aye aye eye eye aye....... |
| 2026-01-16 00:54:54 +0100 | <TMA> | jreicher: there is transfinite silly string... it goes: I I I I I I I I I ... |
| 2026-01-16 00:53:58 +0100 | EvanR | boggles |
| 2026-01-16 00:53:47 +0100 | <jreicher> | I'm not suggesting we do that. I'm just trying to understand the double standard. |
| 2026-01-16 00:53:42 +0100 | <int-e> | . o O ( if you disallow inifinte bitstreams, bitstream becomes empty ) |
| 2026-01-16 00:53:38 +0100 | <EvanR> | would have saved us a lot of trouble |
| 2026-01-16 00:53:32 +0100 | <EvanR> | why didn't cantor think of disallowing infinite streams |
| 2026-01-16 00:53:10 +0100 | <jreicher> | If we disallow infinite bitstreams, bitstream becomes countable. If we allow infinite bitstreams, why can't we allow transfinite silly strings? |
| 2026-01-16 00:52:47 +0100 | <int-e> | EvanR: No, we've crossed that line long ago. |
| 2026-01-16 00:52:37 +0100 | <int-e> | (data SillyType = End | I SillyType) |
| 2026-01-16 00:52:33 +0100 | <EvanR> | it's borderline Silly |
| 2026-01-16 00:52:23 +0100 | <int-e> | (data Nat = Z | S N) |
| 2026-01-16 00:52:18 +0100 | <EvanR> | int-e, looooool |
| 2026-01-16 00:52:12 +0100 | <EvanR> | if you try that on Bitstream, then somebody can come along and get a counterexample stream |
| 2026-01-16 00:52:05 +0100 | <int-e> | (that's borderline stupid; SillyType is obviously isomorphic to Nat) |
| 2026-01-16 00:51:27 +0100 | <EvanR> | specifically, f Z = End; f (S n) = I (f n) |
| 2026-01-16 00:50:45 +0100 | <EvanR> | seems countable |
| 2026-01-16 00:50:44 +0100 | <TMA> | jreicher: BitStream is uncountable. |
| 2026-01-16 00:50:20 +0100 | <EvanR> | I mean, all |
| 2026-01-16 00:50:08 +0100 | <EvanR> | you can map (ok... lazy?) Nat to any SillyType = End | I SillyType |
| 2026-01-16 00:50:07 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) (Ping timeout: 240 seconds) |
| 2026-01-16 00:49:02 +0100 | <EvanR> | you're beyond me now |
| 2026-01-16 00:48:53 +0100 | <EvanR> | well I never brought up classical uncountability |
| 2026-01-16 00:48:51 +0100 | <TMA> | but the smallest model contains just one infinite sequence of Is |
| 2026-01-16 00:48:36 +0100 | <jreicher> | EvanR: sorry, I must be missing something fundamental. I thought bitstream can't be (classically) uncountable without including non-computable streams |
| 2026-01-16 00:48:16 +0100 | <Leary> | jreicher: You can say that if you want to, but as has already been pointed out, you're "crossing the streams" of two settings. You can model BitStream in either a constructive or a classical setting, but it's uncountable in both /because the notion of countability also depends on the setting/. |
| 2026-01-16 00:47:30 +0100 | int-e | loves moving goalposts btw. Not. |
| 2026-01-16 00:47:28 +0100 | <EvanR> | (though I tried to once but everyone ignored me) |
| 2026-01-16 00:47:15 +0100 | <EvanR> | nobody threw in bitstreams that can't be computed that was iterated like 3 times |
| 2026-01-16 00:47:00 +0100 | <jreicher> | TMA: exactly |
| 2026-01-16 00:46:56 +0100 | <jreicher> | OK. So I'm still curious why we think it's OK to throw in bitstreams that can't be computed, but we can't throw in sillytype strings that can't be computed |
| 2026-01-16 00:46:51 +0100 | <int-e> | (It's an infinite type though so adding non-standard elements will generally work.) |
| 2026-01-16 00:46:51 +0100 | <TMA> | so the sequence of ω⁺Is could also be in SillyType |