Kleene's recursion theorem

TheoremA quine#✓fully proved

There is a code \(c\) of a partial recursive function on \(\mathbb{N}\) that, on every input \(n \in \mathbb{N}\), halts and outputs the number encoding \(c\).

theorem exists_quine : ∃ c : Code, ∀ n, c.eval n = Part.some (encode c)

TheoremA code that halts exactly on its own number#✓fully proved

There is a code \(c\) of a partial recursive function on \(\mathbb{N}\) such that, for every \(n \in \mathbb{N}\), \(c\) halts on input \(n\) if and only if \(n\) is the number encoding \(c\).

theorem exists_dom_eq_singleton_encode : ∃ c : Code, c.eval.Dom = {encode c}

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.