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!