Constructing a Quine from Kleene's Second Recursion Theorem

Table of contents

Introduction

It is a well-known fact that the existence of Quines are a consequence of Kleene’s 2nd recursion theorem. I was curious about how easy or difficult it was to use this construction in practice, so I decided to try to formalize it.

One of the virtues of formalization is that it naturally motivates the mathematician to structure their definitions and proofs in a clearer and more concise fashion. The pain of a clunky definition or ill-structured argument is actually felt, and so the goals of expedient proofs and well-structured proofs often align. Far from being a mechanical chore, the act of formalization can actually be a source of insight and creativity (incidentally, this is why I think the popular view of formal verification as a mere exercise in transcription misses the mark).