Newest at the top
| 2025-02-24 20:46:03 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 20:43:54 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:42:00 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 20:40:04 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 260 seconds) |
| 2025-02-24 20:38:59 +0100 | pavonia | (~user@user/siracusa) siracusa |
| 2025-02-24 20:36:05 +0100 | <EvanR> | Agda = U1, U2, U3, ... U_top1, U_top2, Utop3, ... |
| 2025-02-24 20:33:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 265 seconds) |
| 2025-02-24 20:33:23 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) ash3en |
| 2025-02-24 20:28:18 +0100 | ash3en | (~Thunderbi@2a03:7846:b6eb:101:93ac:a90a:da67:f207) (Ping timeout: 244 seconds) |
| 2025-02-24 20:28:10 +0100 | <haskellbridge> | <Bowuigi> Agda has a hierarchy of top universes, but you can't use level polymorphism on them |
| 2025-02-24 20:28:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:27:15 +0100 | <haskellbridge> | <Bowuigi> EvanR Well, it depends on the kind of top universe, if it is truly the top, it must have type in type or similar. If it isn't, then it belongs to an inaccessible universe. I think it would be sound in the second case (not on the first tho) |
| 2025-02-24 20:21:54 +0100 | plitter | (~plitter@user/plitter) plitter |
| 2025-02-24 20:20:05 +0100 | plitter | (~plitter@user/plitter) (Ping timeout: 252 seconds) |
| 2025-02-24 20:18:28 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 265 seconds) |
| 2025-02-24 20:17:37 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-02-24 20:17:10 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 20:15:27 +0100 | <EvanR> | and what are the consequences of the top universe |
| 2025-02-24 20:14:39 +0100 | ljdarj | (~Thunderbi@user/ljdarj) ljdarj |
| 2025-02-24 20:14:14 +0100 | justsomeguy | (~justsomeg@user/justsomeguy) justsomeguy |
| 2025-02-24 20:12:18 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 20:11:41 +0100 | ljdarj | (~Thunderbi@user/ljdarj) (Ping timeout: 265 seconds) |
| 2025-02-24 20:05:40 +0100 | <dolio> | Which you can do. If you have a 'top' universe above all the finite numbered universes, you can use a numeral on the top universe to do pentation. |
| 2025-02-24 20:04:49 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 248 seconds) |
| 2025-02-24 20:04:27 +0100 | <dolio> | And then you can't do pentation because that requires iterating tetration, which requires one of the numers to determine how many sizes you need, and there's no way to get an adaptive number of sizes unless you add a transfinite universe or something. |
| 2025-02-24 20:03:40 +0100 | sprotte24 | (~sprotte24@p200300d16f3063004006d4006bd9f81a.dip0.t-ipconnect.de) |
| 2025-02-24 20:03:05 +0100 | <dolio> | But operating on numerals requires a bigger numeral type in a predicative setting. |
| 2025-02-24 20:02:44 +0100 | <dolio> | I guess a more detailed explanation is that since exponentiation involves instantiating one numeral to `r -> r`, when you want to do tetration, one of the numbers determines how many nestings of that instantiation you need to do, which isn't possible except by operating on numerals. |
| 2025-02-24 20:01:06 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 248 seconds) |
| 2025-02-24 20:00:39 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 19:59:08 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 272 seconds) |
| 2025-02-24 19:56:30 +0100 | <[exa]> | no. of places where I heard about grzegorczyk's hierarchy: happily increases |
| 2025-02-24 19:56:27 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:52:58 +0100 | <dolio> | And you need to switch to using, like, a numeral, and a numeral on numerals. |
| 2025-02-24 19:52:10 +0100 | <dolio> | The 'reason' is basically that exponentiation is the last hyper operation that can easily be defined by just instantiating numerals with the result type. You instantiate one to `r` and one to `r -> r` or something. So, with infinitely many predicative sorts, you only get one 'level' beyond exponentiation. |
| 2025-02-24 19:47:43 +0100 | <EvanR> | 🤯 |
| 2025-02-24 19:46:44 +0100 | <dolio> | Or, anything in Grzegorczyk's class ε₄, which pentation isn't. |
| 2025-02-24 19:45:33 +0100 | <dolio> | No, System F can define any function provably total in second order arithmetic. But if you remove the impredicativity, and replace it with ω-many universes, you can only define tetration. |
| 2025-02-24 19:45:16 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 19:40:21 +0100 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2025-02-24 19:39:35 +0100 | euleritian | (~euleritia@dynamic-176-006-143-040.176.6.pool.telefonica.de) |
| 2025-02-24 19:38:23 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:35:00 +0100 | JuanDaugherty | ColinRobinson |
| 2025-02-24 19:32:36 +0100 | rherardi | (~rherardi@user/rherardi) (Leaving...) |
| 2025-02-24 19:30:22 +0100 | rherardi | (~rherardi@user/rherardi) rherardi |
| 2025-02-24 19:27:35 +0100 | <EvanR> | does it had a hardcoded limit=4 somewhere |
| 2025-02-24 19:27:28 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 245 seconds) |
| 2025-02-24 19:27:20 +0100 | <EvanR> | system F can do tetration but not pentation, wtf |
| 2025-02-24 19:26:58 +0100 | <dolio> | Yeah. |
| 2025-02-24 19:26:47 +0100 | <EvanR> | had to look this one up, pentation is repeated tetration |