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?