Newest at the top
| 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 |
| 2025-02-24 19:24:58 +0100 | <dolio> | E.G. a predicative version of System F can't do pentation. |
| 2025-02-24 19:24:46 +0100 | comonad | (~comonad@p200300d027488b00f8b6e4e070ffbc0b.dip0.t-ipconnect.de) |
| 2025-02-24 19:24:27 +0100 | comonad | (~comonad@pd9e07a19.dip0.t-ipconnect.de) (Quit: WeeChat 4.6.0-dev) |
| 2025-02-24 19:22:36 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:20:36 +0100 | <dolio> | So they don't even have the proper ability to do recursive stuff in general. |
| 2025-02-24 19:19:14 +0100 | <dolio> | The problem with predicativity is that encodings quantify over all the types that you're allowed to do recursion into, but then you're bigger than any of the things you can recurse into, and you can't recurse into anything bigger than what you picked. |
| 2025-02-24 19:18:18 +0100 | alfiee | (~alfiee@user/alfiee) (Ping timeout: 245 seconds) |
| 2025-02-24 19:18:11 +0100 | <EvanR> | Ç plus plus (must be pronounced french) |
| 2025-02-24 19:15:57 +0100 | <dolio> | But I don't think it'd solve the predicativity part. |
| 2025-02-24 19:15:55 +0100 | <mauke> | I should invent a language called Ç |
| 2025-02-24 19:15:14 +0100 | <dolio> | Well, cedille solves the fact that you can't really encode inductive things at all, from the type theory end. |
| 2025-02-24 19:14:44 +0100 | rherardi | (~rherardi@user/rherardi) (Ping timeout: 260 seconds) |
| 2025-02-24 19:14:15 +0100 | alfiee | (~alfiee@user/alfiee) alfiee |
| 2025-02-24 19:13:39 +0100 | <haskellbridge> | <Bowuigi> dolio yeah Barendegt's PTSs don't have much power in terms of common theorem proving. Technically there's a way to regain that power but it requires fancy features, either the ones in CDLE/Cedille or that one encoding method I found on a random thesis and I can't find again |
| 2025-02-24 19:11:37 +0100 | JSharp | (sid4580@user/JSharp) JSharp |
| 2025-02-24 19:11:32 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) (Ping timeout: 252 seconds) |
| 2025-02-24 19:09:26 +0100 | mustafa | (sid502723@rockylinux/releng/mustafa) mustafa |
| 2025-02-24 19:08:08 +0100 | gmc | (sid58314@id-58314.ilkley.irccloud.com) gmc |
| 2025-02-24 19:07:59 +0100 | Pent | (sid313808@id-313808.lymington.irccloud.com) Pent____ |
| 2025-02-24 19:07:56 +0100 | tv | (~tv@user/tv) tv |
| 2025-02-24 19:07:47 +0100 | tapas | (sid467876@id-467876.ilkley.irccloud.com) tapas |
| 2025-02-24 19:07:43 +0100 | tv | (~tv@user/tv) (Quit: derp) |
| 2025-02-24 19:07:43 +0100 | cbarrett | (sid192934@id-192934.helmsley.irccloud.com) cbarrett |
| 2025-02-24 19:07:33 +0100 | sa | (sid1055@id-1055.tinside.irccloud.com) sa |
| 2025-02-24 19:06:48 +0100 | merijn | (~merijn@host-vr.cgnat-g.v4.dfn.nl) merijn |
| 2025-02-24 19:06:27 +0100 | mustafa | (sid502723@rockylinux/releng/mustafa) (Ping timeout: 265 seconds) |
| 2025-02-24 19:05:23 +0100 | gmc | (sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 2025-02-24 19:05:23 +0100 | JSharp | (sid4580@user/JSharp) (Ping timeout: 245 seconds) |
| 2025-02-24 19:05:00 +0100 | cbarrett | (sid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 265 seconds) |
| 2025-02-24 19:04:34 +0100 | Square2 | (~Square4@user/square) (Ping timeout: 252 seconds) |
| 2025-02-24 19:04:33 +0100 | tapas | (sid467876@id-467876.ilkley.irccloud.com) (Ping timeout: 245 seconds) |