Comment by nickdrozd
7 years 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?
Probably 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.
Not really an answer but if you check out provability section of 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.