See also Löb’s theorem: https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem Compare Löb’s theorem with the s

See also Löb’s theorem: https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem https://en.wikipedia.org/wiki/L%C3%B6b%27s_theorem Compare Löb’s theorem with the signature of `loeb` with some renaming to make them match up: > in any formal system F, for any formula P, if it is provable in F that "if P is provable in F then P is true", then P is provable in F loeb :: Functor f => f (f p -> p) -> f p To see it even better, look at the section that introduces the modal logic operator (the square that operates on formulae). See more on the Löb-spreadsheet equivalence here http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet.html http://blog.sigfpe.com/2006/11/from-l-theorem-to-spreadsheet...