4 ms·
Loeb's theorem says that you can prove a statement S if you can prove that S is implied by its own provability. It's actually a generalization of Goedel's secon
by nickdrozd 8y ago
Loeb's theorem says that you can prove a statement S if you can prove that S is implied by its own provability. It's actually a generalization of Goedel's second incompleteness theorem (let S be a false statement like 0 = 1). I can see something in the article that looks like Loeb's theorem (f (f a -> a) -> f a, reading f as it can be proved that), but I don't know Haskell, so I'm completely lost after that. Can someone explain in non-Haskell terms what's going on?
- Pranz 8y agoNot really an answer but if you check out provability section of https://en.wikipedia.org/wiki/Löb's_theorem https://en.wikipedia.org/wiki/Löb's_theorem you'll find a formula very similiar to the haskell type, together with a proof in modal logic.
- moomin 8y agoProbably not, but since no-one else is having a go, I will: f is “Functor”, which means roughly the same thing as in category theory (but restricted to the domain of Haskell types). I’m guessing it’s possible to construct a Provability functor. -> in Haskell is just a function. I’ll mention that types and propositions have a structure preserving isomorphism. So “a” is an arbitrary type but you can think of it as an arbitrary proposition. But equally, this holds true for all Functors, so we can specialise the function to something like (List (List Int -> Int) -> List Int I hope this helps, it might not.