Newest at the top
| 2026-01-15 23:27:17 +0100 | <dolio> | (That uncountability part requires more committment to computable principles.) |
| 2026-01-15 23:26:58 +0100 | <EvanR> | monochrom, it's a slippery slope from there to buffyspeak anything can be anythinged! |
| 2026-01-15 23:26:17 +0100 | <dolio> | But infinity + 1 = infinity, right? |
| 2026-01-15 23:26:15 +0100 | <monochrom> | I achieve "they are all axioms". |
| 2026-01-15 23:26:02 +0100 | <EvanR> | twice as many definitions / axioms? xD |
| 2026-01-15 23:25:56 +0100 | <EvanR> | monochrom, what do you achieve by doing this xD |
| 2026-01-15 23:25:43 +0100 | takuan | (~takuan@d8D86B9E9.access.telenet.be) (Ping timeout: 240 seconds) |
| 2026-01-15 23:25:42 +0100 | <dolio> | How many more are there? At most one. |
| 2026-01-15 23:25:36 +0100 | <monochrom> | EvanR, I clone every definition to be an axiom, e.g., definition "x := 4" is cloned so I add an axiom "x = 4". |
| 2026-01-15 23:25:34 +0100 | <dolio> | The extended natural numbers are uncountable. |
| 2026-01-15 23:25:03 +0100 | <dolio> | Yes, the idea that uncountability is about "size" is an erroneous extrapolation from finite sets. |
| 2026-01-15 23:25:03 +0100 | <EvanR> | again, isn't this saying more about misunderstanding classical notions ? xD |
| 2026-01-15 23:24:39 +0100 | <monochrom> | Because classical uncountability gives me a feeling of size, but constructive uncountability doesn't feel like "bigger size", just "unreachable". |
| 2026-01-15 23:24:34 +0100 | <EvanR> | basically syntactic sugar |
| 2026-01-15 23:23:56 +0100 | <dolio> | The diagonal argument shows that any computable way to enumerate computable bit streams misses some of the computable bit streams. You don't need uncomputable ones for the enumeration to be incomplete. |
| 2026-01-15 23:23:54 +0100 | <EvanR> | monochrom, I'm calling definitions shorthand that expands to something we already had. Unlike e.g. "the answer to any LEM question you name" |
| 2026-01-15 23:23:26 +0100 | <monochrom> | That gives very different feel... But I confess I'm classical in my core, I only pretend to be intuitionistic when it's convenient. :) |
| 2026-01-15 23:22:56 +0100 | merijn | (~merijn@host-cl.cgnat-g.v4.dfn.nl) merijn |
| 2026-01-15 23:22:17 +0100 | <dolio> | So reject them. |
| 2026-01-15 23:21:56 +0100 | <dolio> | But in the natural mathematics of computable things, they are uncountable. The ways to count them are not computable. |
| 2026-01-15 23:21:32 +0100 | <EvanR> | s/finite/countable/ |
| 2026-01-15 23:21:22 +0100 | <EvanR> | another thing, my kneejerk devil's advocate arguement for the countable Bitstream is that you can only have finite many programs. However in haskell you can obtain Bitstream other ways... which perhaps also avoids computability |
| 2026-01-15 23:20:56 +0100 | <dolio> | The only way they look countable is if you believe in classical mathematics and try to build computability within that. |
| 2026-01-15 23:20:55 +0100 | <int-e> | dolio: see me 15 minutes ago ;-) |
| 2026-01-15 23:20:54 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) |
| 2026-01-15 23:20:50 +0100 | <monochrom> | (About theory with/wo axioms. I don't draw lines between axioms, definitions, inference rules either.) |
| 2026-01-15 23:20:41 +0100 | trickard_ | (~trickard@cpe-84-98-47-163.wireline.com.au) (Read error: Connection reset by peer) |
| 2026-01-15 23:20:31 +0100 | <dolio> | Cantor's diagonal argument is constructive, ergo bit streams are uncountable. |
| 2026-01-15 23:20:16 +0100 | <dolio> | All you need to do to have uncountable bit streams is live within constructive mathematics, recognizing that it holds for computable things (computability allows extra principles on top of bare constructive mathematics, actually). |
| 2026-01-15 23:18:26 +0100 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) bitdex |
| 2026-01-15 23:16:07 +0100 | <monochrom> | But if you do the denotational "construct the approximation sequence, take limit" it's plain as day. |
| 2026-01-15 23:15:27 +0100 | <jreicher> | *fiat |
| 2026-01-15 23:15:25 +0100 | chromoblob | (~chromoblo@user/chromob1ot1c) (Ping timeout: 256 seconds) |
| 2026-01-15 23:15:24 +0100 | <jreicher> | "fiar" is "assertion" |
| 2026-01-15 23:15:24 +0100 | <monochrom> | Every textbook or tutorial I saw tried to explain it poorly with lazy evaluation. |
| 2026-01-15 23:15:21 +0100 | <EvanR> | introduced* |
| 2026-01-15 23:15:12 +0100 | <EvanR> | an example of an axiom in type theory is the law of excluded middle. Introduces by fiat. As opposed to proven as a theorem somehow |
| 2026-01-15 23:14:53 +0100 | <jreicher> | int-e: monochrom: I appreciate the use of "extra" infinity as a simplification. Not the first time I've heard that argument. |
| 2026-01-15 23:14:51 +0100 | <monochrom> | The hardest example made easy being fs = 1 : 1 : zipWith (+) fs (tail fs). |
| 2026-01-15 23:14:22 +0100 | <EvanR> | to save space |
| 2026-01-15 23:14:16 +0100 | <EvanR> | definition is just naming something that you could already say long winded |
| 2026-01-15 23:14:10 +0100 | <jreicher> | Not for a formal theory, no |
| 2026-01-15 23:13:57 +0100 | <EvanR> | well that's muddying things a lot isn't it |
| 2026-01-15 23:13:55 +0100 | <int-e> | Again, keeping things as mathematically simple as possible. |
| 2026-01-15 23:13:46 +0100 | <jreicher> | Definitions are axioms |
| 2026-01-15 23:13:40 +0100 | <int-e> | And, correspondingly, the easiest model for streams of Bools gives you an arbitrary boolean value for the n-th element of the stream, for each natural number N. The set of all these functions is uncountable. |
| 2026-01-15 23:13:37 +0100 | <EvanR> | definitions |
| 2026-01-15 23:13:33 +0100 | <jreicher> | How can you have a theory without axioms? |
| 2026-01-15 23:13:20 +0100 | <EvanR> | jreicher, in type theory, we don't always have axioms! |
| 2026-01-15 23:13:13 +0100 | <monochrom> | My lecture notes also shows that if you use this "unrealistic" (but still sound) denotational approach, it is easier to predict the outcome of certain recursive definitions. |