Self-quoting fixed point

ID: self-quoting-fixed-point

Let code application and code numeral quotation. For a lambda term , choose a fresh and put and . Then , so . This diagonal argument uses the syntax of the actual term , including any free variables, not an equivalence-class code.

New to topics? Read the docs here!