If anyone's wondering, the Y combinator gets mentioned on page 14, though only in passing. Didn't seem to mention fixed points in the section on representing p

If anyone's wondering, the Y combinator gets mentioned on page 14, though only in passing. Didn't seem to mention fixed points in the section on representing proofs in lambda calculus, though. It can easily be observed that the type of Y is (P -> P) -> P, that is, a proposition implying itself implies itself. Since the first part is obviously a tautology, this reduces to a proof of "for all P, P is true". Hooray, anything is possible! This is closely related to Löb's theorem, Gödel's incompleteness theorems, and all those other fun things. The net result is that there is a fundamental equivalence between true theorems that cannot be proven (cf. Gödel) and correct programs that cannot be shown to halt (cf. Turing).