Computability · The Lumenary

Lens

MotivationH

A question no program can answer

Here is a five-line program. Given a positive integer $n$ , it repeatedly halves $n$ if $n$ is even and replaces $n$ by $3n + 1$ if $n$ is odd, and it stops when it reaches $1$ .

while n != 1:
    if n % 2 == 0: n = n // 2
    else:          n = 3 * n + 1

Does it stop for every starting value? This is the Collatz problem, and nobody knows. Computers have checked starting values into the quintillions, and every one has reached $1$ — but that is evidence, not proof.

A software company would love a tool that reads any program and its input and reports, correctly and always, whether the program eventually stops or runs forever. Such a tool would settle the Collatz problem in an afternoon, and Goldbach's conjecture too (write a program that searches for a counterexample and ask whether it stops). In 1936 Alan Turing proved that no such tool can exist — not because it would be slow, or because we have not been clever enough, but because its existence is contradictory.

Turing was answering a question of David Hilbert's: is there a mechanical procedure that decides, for every statement of first-order logic, whether it is valid? To answer "no", he first had to say precisely what a mechanical procedure is. His answer — the Turing machine — is the founding definition of computer science, and this lesson is about what it can and cannot do. It builds on algorithms and their correctness and on countability and Cantor's diagonal argument, which will reappear in a new guise.

IntuitionH

Programs are data

Two simple observations drive the whole subject.

Programs can be written down. A program is a finite string of symbols, so programs can be listed: $P_0, P_1, P_2, \dots$ (say, in order of length and then alphabetically). In particular there are only countably many programs, while there are uncountably many functions $\N \to \N$ . Before doing anything else, we already know that almost all functions cannot be computed by any program.

Programs can read programs. Compilers, interpreters and virus scanners take programs as input. In particular there is a single universal program $U$ that, given the text of any program $P$ and an input $x$ , simulates $P$ on $x$ . A Python interpreter is, in effect, such a program.

Put these together and something strange becomes possible: a program can be run on its own text. Picture an infinite table whose rows are the programs and whose columns are the inputs $0, 1, 2, \dots$ ; entry $(e, x)$ records whether $P_e$ halts on input $x$ . Cantor's diagonal argument walks down the diagonal of a table like this and builds a row that differs from every row. Here the diagonal row is a program — provided some program could read the table — and that will be the contradiction behind the halting problem.

DefinitionsH

Turing machines and what they compute

Definition— Turing machine

A (deterministic, one-tape) Turing machine consists of a finite set $Q$ of states with a start state $q_0 \in Q$ , a finite tape alphabet $\Gamma$ containing a blank symbol $\sqcup$ , and a transition function

\delta : Q \times \Gamma \to \Gamma \times \{\mathrm{L}, \mathrm{R}\} \times (Q \cup \{\mathrm{halt}\}).

The machine works on a tape of cells indexed by $\Z$ , all blank except finitely many, with a head scanning one cell. If it is in state $q$ scanning symbol $s$ and $\delta(q, s) = (s', d, q')$ , it writes $s'$ , moves the head one cell in direction $d$ , and enters state $q'$ — or stops, if $q' = \mathrm{halt}$ .

A configuration is a snapshot (state, tape contents, head position); one application of $\delta$ is a step. Started on an input written on the tape, the machine either halts after finitely many steps or runs forever. Many conventions differ in inessential ways (several tapes, a one-way infinite tape, accepting and rejecting states, larger alphabets); all of them compute the same functions.

Definition— computable function

Fix a way of writing natural numbers on the tape (in binary, say). A machine $M$ computes the partial function $f : \N \rightharpoonup \N$ if, started on input $x$ , it halts with $f(x)$ on the tape whenever $f(x)$ is defined, and runs forever whenever $f(x)$ is undefined. A partial function is (partial) computable if some machine computes it; a computable function is a total one. Write $\varphi_e$ for the partial function computed by the $e$ -th machine $M_e$ in a fixed listing, $\varphi_e(x)\!\downarrow$ if $M_e$ halts on $x$ and $\varphi_e(x)\!\uparrow$ if it does not.

Definition— decidable and recursively enumerable sets

A set $A \subseteq \N$ is decidable (or computable, recursive) if its characteristic function $\chi_A$ is computable: some machine halts on every input and answers correctly whether $x \in A$ . It is recursively enumerable (r.e., semi-decidable, computably enumerable) if some machine halts exactly on the members of $A$ , i.e. $A = W_e := \{x \mid \varphi_e(x)\!\downarrow\}$ for some $e$ . It is co-r.e. if its complement $\overline{A} = \N \setminus A$ is r.e.

A semi-decider for $A$ says "yes" on members and stays silent forever on non-members — and silence never turns into an answer, because at no finite time can you tell "silent so far" from "silent forever". The same definitions apply to sets of strings, pairs or programs, via any reasonable coding as natural numbers.

Definition— the halting problem

The halting set is $H = \{\langle e, x\rangle \mid \varphi_e(x)\!\downarrow\}$ , where $\langle e, x \rangle$ is a computable pairing of $\N \times \N$ with $\N$ . Its diagonal is $K = \{e \mid \varphi_e(e)\!\downarrow\}$ . The halting problem is the question whether $H$ is decidable.

Two facts about the listing $M_0, M_1, \dots$ are used constantly. The universal machine theorem: there is a machine $U$ with $\varphi_U(\langle e, x\rangle) \simeq \varphi_e(x)$ for all $e, x$ (both sides defined and equal, or both undefined). Turing built one in 1936; a modern interpreter is one. Kleene's s-m-n theorem: there is a computable function $s$ such that $\varphi_{s(e, y)}(x) \simeq \varphi_e(\langle y, x\rangle)$ — from a program and a value you can compute a program with that value "hard-wired" in. Both are straightforward but long to prove in full detail for Turing machines; any of the texts in the reading list does it.

Note

The Church–Turing thesis says that every function which is effectively calculable — computable by a finite, deterministic, mechanical procedure, with unlimited time and paper — is computable by a Turing machine. It is a thesis, not a theorem: "effectively calculable" is an informal notion, so the claim cannot be proved. The evidence for it is strong. Turing's 1936 analysis of what a human computer can do with pencil and paper leads to his machines; and every other model proposed — Church's λ-calculus, Gödel–Herbrand–Kleene general recursive functions, Post systems, register machines, cellular automata, every programming language — computes exactly the same class of functions, a fact that is proved, model by model.

Worked examplesH

Machines, decidable sets and undecidable ones

A Turing machine in state carry, scanning the last bit of 1011. The tape is unbounded in both directions; all but finitely many cells are blank.

Example— A binary incrementer

One state, carry, with the head on the least significant bit:

state	read	write	move	next
carry	1	0	L	carry
carry	0 or blank	1	L	halt

On $1011$ (eleven) it turns the two trailing $1$ s into $0$ s, turns the $0$ into a $1$ and halts: $1100$ (twelve), in $3$ steps. In general it takes $t + 1$ steps, where $t$ is the number of trailing $1$ s. Although a single increment can take many steps ( $2^k - 1 \mapsto 2^k$ takes $k + 1$ ), counting from $0$ to $2^k - 1$ takes $2^{k+1} - 1$ steps in total — fewer than two per increment on average.

Example— A unary adder

Write $m + n$ as $1^m\,0\,1^n$ ( $m$ ones, a separator, $n$ ones). The machine walks right in state A over the first block; at the separator it writes $1$ and switches to state B; B walks right over the second block; at the blank after it, B steps back left into state C, and C erases the last $1$ and halts. The tape now holds $1^{m+n}$ , after $m + n + 3$ steps.

Example— The two-state busy beaver

Started on a blank tape, the machine with states A, B and table

\mathrm{A}0 \to 1\mathrm{R}\mathrm{B}, \qquad \mathrm{A}1 \to 1\mathrm{L}\mathrm{B}, \qquad \mathrm{B}0 \to 1\mathrm{L}\mathrm{A}, \qquad \mathrm{B}1 \to 1\mathrm{R}\,\mathrm{halt}

runs for $6$ steps and leaves four $1$ s on the tape. Tibor Radó (1962) defined the busy-beaver function $S(n)$ : the largest number of steps taken by an $n$ -state, two-symbol machine that halts when started on a blank tape. There are only finitely many such machines, so $S(n)$ is a perfectly well-defined number — but we shall see that $S$ is not computable. The machine above shows $S(2) \ge 6$ ; the experiment below proves $S(2) = 6$ by settling all $20\,736$ two-state machines.

Example— Decidable sets

The primes, the even numbers, the set of $n$ such that $n$ is a perfect number, the set of (codes of) propositional tautologies, and the set of pairs $(G, k)$ such that the finite graph $G$ has a $k$ -colouring are all decidable: in each case a finite search answers the question. The set of $e$ such that machine $M_e$ has fewer than $10$ states is decidable — you only have to read the table, not run it. Decidability says nothing about speed; that is the subject of computational complexity.

Example— Recursively enumerable sets

$\{e \mid \varphi_e(0) = 7\}$ is r.e.: run $M_e$ on $0$ and halt if the output is $7$ . The halting set $H$ is r.e.: run the universal machine. The set of theorems of Peano arithmetic is r.e.: enumerate all finite strings and halt when one is a proof of the given sentence. The set of polynomials $p \in \Z[x_1, \dots, x_n]$ with an integer root is r.e.: search through all integer tuples. We will see that $H$ is not decidable; the other three are not decidable either.

Example— A set that is not even r.e.

$\overline{K} = \{e \mid \varphi_e(e)\!\uparrow\}$ , the set of machines that do not halt on their own index, is not r.e. (Corollary below). Neither is $\mathrm{Tot} = \{e \mid \varphi_e \text{ is total}\}$ (Exercise).

ProofH

The halting problem, reductions and Rice's theorem

Theorem— Theorem 1 (most functions are not computable)

There are only countably many computable partial functions $\N \rightharpoonup \N$ , but uncountably many functions $\N \to \N$ . In particular, some total function $\N \to \N$ is not computable.

Proof

A Turing machine is determined by its finite table, which can be written as a finite string over a fixed finite alphabet (name the states $q_0, q_1, \dots$ in binary). The set of finite strings over a finite alphabet is countable, so there are countably many machines, and each computes exactly one partial function.

On the other hand, given any sequence $f_0, f_1, f_2, \dots$ of functions $\N \to \N$ , the function $g(n) = f_n(n) + 1$ differs from $f_n$ at the input $n$ , so $g$ is not in the sequence: $\N \to \N$ is uncountable. A countable set cannot contain an uncountable one, so some $f : \N \to \N$ is computed by no machine.

∎

This proof is non-constructive: it does not name a non-computable function. The next theorem does.

Theorem— Theorem 2 (Turing, 1936: the halting problem is undecidable)

The set $K = \{e \mid \varphi_e(e)\!\downarrow\}$ is not decidable. Consequently the halting set $H = \{\langle e, x\rangle \mid \varphi_e(x)\!\downarrow\}$ is not decidable.

Proof

Suppose some machine decides $K$ : it computes the total function $h$ with $h(e) = 1$ if $\varphi_e(e)\!\downarrow$ and $h(e) = 0$ otherwise. Build a new machine $D$ which, on input $x$ , computes $h(x)$ and then

if $h(x) = 1$ , enters a loop that never halts;
if $h(x) = 0$ , halts.

$D$ is a genuine Turing machine (it runs the machine for $h$ as a subroutine and then does one of two trivial things), so $D = M_d$ for some index $d$ . Now ask whether $D$ halts on its own index $d$ :

\varphi_d(d)\!\downarrow \iff h(d) = 0 \iff \varphi_d(d)\!\uparrow.

The first equivalence is the construction of $D$ ; the second is the correctness of $h$ . This is a contradiction, so no machine decides $K$ .

If $H$ were decidable, then so would be $K$ : to decide whether $e \in K$ , compute the pair $\langle e, e \rangle$ and ask the decider for $H$ .

∎

Note

Notice what the proof did not say. For each single machine $e$ , the question "does $M_e$ halt on $e$ ?" has an answer, and one of the two constant algorithms "always say yes" and "always say no" gives it. Undecidability means that no single algorithm answers correctly for all $e$ . Many individual instances are easy; some (like Collatz) may be hard; the theorem is about uniformity.

Theorem— Theorem 3 (the halting set is recursively enumerable)

$K$ and $H$ are r.e.

Proof

The universal machine halts on $\langle e, x\rangle$ exactly when $M_e$ halts on $x$ , so it is a semi-decider for $H$ . For $K$ , first compute $\langle e, e\rangle$ and then run the universal machine.

∎

Theorem— Theorem 4 (decidable = r.e. and co-r.e.)

A set $A \subseteq \N$ is decidable if and only if both $A$ and its complement $\overline{A}$ are recursively enumerable.

Proof

( $\Rightarrow$ ) If a machine decides $A$ , modify it to loop forever instead of answering "no": that semi-decides $A$ . Modify it to loop instead of answering "yes": that semi-decides $\overline{A}$ .

( $\Leftarrow$ ) Let $M$ semi-decide $A$ and $N$ semi-decide $\overline{A}$ . On input $x$ , simulate one step of $M$ on $x$ , then one step of $N$ on $x$ , then the next step of $M$ , and so on (dovetailing). Every $x$ lies in exactly one of $A$ and $\overline{A}$ , so exactly one of the two simulations eventually halts, after finitely many rounds. Answer "yes" if $M$ halted and "no" if $N$ did. This procedure always halts and is always correct.

∎

This is often called Post's theorem. Note the importance of interleaving: running $M$ to completion first would hang forever on inputs outside $A$ .

Theorem— Corollary 5

$\overline{K}$ is not recursively enumerable. So the class of r.e. sets is not closed under complement.

Proof

$K$ is r.e. (Theorem 3). If $\overline{K}$ were r.e. too, $K$ would be decidable by Theorem 4, contradicting Theorem 2.

∎

The r.e. sets have a useful alternative description, which is how they appear in logic and number theory.

Theorem— Theorem 6 (r.e. = projection of decidable)

$A \subseteq \N$ is r.e. if and only if there is a decidable relation $R \subseteq \N \times \N$ with $A = \{x \mid \exists y\, R(x, y)\}$ .

Proof

( $\Rightarrow$ ) If $A = W_e$ , let $R(x, y)$ say " $M_e$ halts on input $x$ within $y$ steps". $R$ is decidable — simulate $M_e$ for $y$ steps — and $x \in A$ iff $R(x, y)$ for some $y$ .

( $\Leftarrow$ ) Given decidable $R$ , the machine that on input $x$ tests $R(x, 0), R(x, 1), R(x, 2), \dots$ in turn and halts at the first success semi-decides $A$ .

∎

So "r.e." means "membership has a finite, checkable certificate $y$ ": a halting computation, a proof, an integer solution. Decidable sets are those where non-membership also has one.

Reductions

To show a new problem undecidable we rarely repeat the diagonal argument. Instead we reduce a known undecidable problem to it.

Definition— many-one reduction

$A$ is many-one reducible to $B$ , written $A \le_m B$ , if there is a total computable $f : \N \to \N$ with $x \in A \iff f(x) \in B$ for all $x$ .

Theorem— Lemma 7 (reductions transfer decidability)

Suppose $A \le_m B$ . If $B$ is decidable, so is $A$ ; if $B$ is r.e., so is $A$ . Equivalently: if $A$ is undecidable, so is $B$ ; if $A$ is not r.e., neither is $B$ .

Proof

Let $f$ be the reduction. To decide (or semi-decide) whether $x \in A$ , compute $f(x)$ — this always halts — and run the decider (or semi-decider) for $B$ on $f(x)$ . Correctness is exactly $x \in A \iff f(x) \in B$ .

∎

The direction matters: to prove $B$ hard, reduce a known hard problem to $B$ .

Example— Halting on the blank tape

Let $H_0 = \{e \mid M_e \text{ halts when started on a blank tape}\}$ . Given $e$ , compute (by the s-m-n theorem) an index $f(e)$ for the machine that ignores its input, writes $e$ on the tape and then runs $M_e$ . Then $M_{f(e)}$ halts on the blank tape iff $\varphi_e(e)\!\downarrow$ , so $K \le_m H_0$ and $H_0$ is undecidable.

Theorem— Corollary 8 (the busy-beaver function is not computable)

$S$ is not computable.

Proof

If it were, we could decide $H_0$ : given $e$ , count the states $n$ of $M_e$ (passing first to an equivalent two-symbol machine, which can be done effectively), compute $S(n)$ , and simulate $M_e$ on the blank tape for $S(n)$ steps. If it has not halted by then, it never will, by the definition of $S(n)$ . This contradicts the undecidability of $H_0$ .

∎

In fact $S$ eventually exceeds every computable function (Radó, 1962). The known values are $S(1) = 1$ , $S(2) = 6$ , $S(3) = 21$ , $S(4) = 107$ and — settled in 2024 by the online Busy Beaver Challenge collaboration, with a proof checked in the Coq proof assistant — $S(5) = 47\,176\,870$ . Already for six states, the question involves machines whose behaviour resembles open problems of Collatz type.

Rice's theorem

Halting is not special. Every question about what a program computes — as opposed to what its text looks like — is undecidable, unless it is trivial.

Theorem— Theorem 9 (Rice, 1953)

Let $\mathcal P$ be a set of partial computable functions which is non-trivial: some partial computable function lies in $\mathcal P$ and some does not. Then the index set $I_{\mathcal P} = \{e \mid \varphi_e \in \mathcal P\}$ is undecidable.

Proof

Let $\bot$ denote the nowhere-defined function. Decidability is preserved by complements, and $I_{\overline{\mathcal P}}$ is the complement of $I_{\mathcal P}$ , so we may assume $\bot \notin \mathcal P$ (otherwise replace $\mathcal P$ by its complement in the partial computable functions, which is also non-trivial). Choose $\psi \in \mathcal P$ , computed by the machine $M_m$ .

For each $e$ , let $g(e)$ be an index of the machine that, on input $y$ , first runs $M_e$ on $e$ and, if that halts, then runs $M_m$ on $y$ and outputs the result. The function $g$ is computable (s-m-n theorem), and

\varphi_{g(e)} = \begin{cases} \psi & \text{if } \varphi_e(e)\!\downarrow, \\ \bot & \text{if } \varphi_e(e)\!\uparrow. \end{cases}

Since $\psi \in \mathcal P$ and $\bot \notin \mathcal P$ , we get $e \in K \iff g(e) \in I_{\mathcal P}$ . So $K \le_m I_{\mathcal P}$ , and $I_{\mathcal P}$ is undecidable by Lemma 7.

∎

Example— What Rice's theorem does and does not say

Undecidable by Rice: " $\varphi_e$ is total", " $\varphi_e(3) = 3$ ", " $\varphi_e$ is the zero function", " $\mathrm{dom}\,\varphi_e$ is finite", " $M_e$ computes the same function as $M_7$ ". Not covered by Rice, because they are about the program text or running time rather than the function computed: " $M_e$ has an even number of states" (decidable), " $M_e$ halts on input $0$ within $100$ steps" (decidable). Rice's theorem is the reason a perfect bug-finder cannot exist: "this program never divides by zero" is a semantic property.

Formal mathematicsF

Computability in Lean and Mathlib

Mathlib's computability library (built by Mario Carneiro) does not start from Turing machines. Its basic notion is the partial recursive function Nat.Partrec : (ℕ →. ℕ) → Prop, generated from zero, successor and pairing by composition, primitive recursion and unbounded search — a model proved equivalent to Turing machines in the classical literature. Programs are an inductive type Nat.Partrec.Code with a universal evaluator Code.eval : Code → ℕ →. ℕ, and Code is countable (indeed Denumerable). The arrow →. is a partial function, valued in Part ℕ; (c.eval n).Dom is the proposition "program c halts on n". Mathlib separately develops Turing machines and proves that they can simulate partial recursive functions.

To make the definitions concrete, this lesson's module also contains a small two-symbol Turing machine simulator of its own:

MachineLean 4Formally verified

/-- A Turing machine with states `Q`: in state `q` reading symbol `b`, it writes a symbol,
moves, and goes to a new state — or halts (`none`). The table is finite when `Q` is. -/
def Machine (Q : Type) := Q → Bool → Bool × Dir × Option Q

Axioms used: No axiomsformal/Lumenary/Computability.leanTry it in the Lean web editor

stepLean 4Formally verified

/-- One step of the machine `M`. A halted configuration stays where it is. -/
def step {Q : Type} (M : Machine Q) : Config Q → Config Q
  | ⟨none, t⟩ => ⟨none, t⟩
  | ⟨some q, t⟩ =>
      let (w, d, q') := M q t.head
      ⟨q', Tape.move d { t with head := w }⟩

Axioms used: No axiomsformal/Lumenary/Computability.leanTry it in the Lean web editor

Concrete runs are checked by evaluation (decide): the incrementer on $1011$ , and the busy beaver halting at step 6 with four $1$ s.

incr_elevenLean 4Proved here from basic factsFormally verified

/-- The incrementer turns `1011` (eleven) into `1100` (twelve) in three steps, checked by
evaluation. The tape then reads `1 1 0 0` from left to right, with the head on its first cell. -/
theorem incr_eleven :
    run incr 3 ⟨some (), ⟨[true, false, true], true, []⟩⟩ =
      ⟨none, ⟨[], true, [true, false, false]⟩⟩ := by
  decide

Axioms used: No axiomsformal/Lumenary/Computability.leanTry it in the Lean web editor

bb2Lean 4Formally verified

/-- The two-state busy beaver (states `false` = A, `true` = B):
A0 → 1RB, A1 → 1LB, B0 → 1LA, B1 → 1R(halt). -/
def bb2 : Machine Bool
  | false, false => (true, .right, some true)
  | false, true => (true, .left, some true)
  | true, false => (true, .left, some false)
  | true, true => (true, .right, none)

Axioms used: No axiomsformal/Lumenary/Computability.leanTry it in the Lean web editor

bb2_runLean 4Proved here from basic factsFormally verified

/-- Started in state A on a blank tape, `bb2` is still running after 5 steps, halts at step 6,
and leaves four `1`s: the values `S(2) = 6` and `Σ(2) = 4` of Radó's busy-beaver functions are
attained by this machine. (That no two-state machine does better needs a proof that every other
two-state machine either halts sooner or never halts; that is not formalised here.) -/
theorem bb2_run :
    (run bb2 5 ⟨some false, ⟨[], false, []⟩⟩).state ≠ none ∧
      (run bb2 6 ⟨some false, ⟨[], false, []⟩⟩).state = none ∧
      (run bb2 6 ⟨some false, ⟨[], false, []⟩⟩).tape.ones = 4 := by
  decide

Axioms used: No axiomsformal/Lumenary/Computability.leanTry it in the Lean web editor

The diagonal argument, abstractly. The heart of Theorem 2 needs nothing about Turing machines: only a "halts" relation and the ability to build the diagonal program. Proved here:

no_halting_deciderLean 4Proved here from basic factsFormally verified

/-- **The diagonal argument behind the halting problem**, for any notion of program.
Let `Halts p q` mean "program `p` halts on input `q`", and let `d` be any proposed decider.
If programs are flexible enough to build the *diagonal program* `e`, which on input `q` halts
exactly when `d` says "`q` does not halt on `q`", then `d` is wrong somewhere: feeding `e` to
itself, `e` halts on `e` iff `d e e = false`, while correctness would demand `d e e = true`. -/
theorem no_halting_decider {P : Type*} (Halts : P → P → Prop) (d : P → P → Bool)
    (diag : ∃ e : P, ∀ q, Halts e q ↔ d q q = false) :
    ¬ ∀ p q, Halts p q ↔ d p q = true := by
  intro hd
  obtain ⟨e, he⟩ := diag
  have h1 : Halts e e ↔ d e e = false := he e
  have h2 : Halts e e ↔ d e e = true := hd e e
  cases hde : d e e
  · -- `d e e = false`: then `e` halts on `e`, so correctness forces `d e e = true`.
    exact Bool.false_ne_true (hde ▸ h2.1 (h1.2 hde))
  · -- `d e e = true`: then `e` halts on `e`, so the diagonal property forces `d e e = false`.
    exact Bool.false_ne_true (hde ▸ (h1.1 (h2.2 hde)).symm)

Axioms used: No axiomsformal/Lumenary/Computability.leanTry it in the Lean web editor

Theorem 1, formalised. Cantor's diagonal argument for $\N \to \N$ , and then the counting argument, using Mathlib's theorem that every computable function has a code:

cantor_diagLean 4Proved here from basic factsFormally verified

/-- **Cantor's diagonal argument.** No sequence `e 0, e 1, e 2, …` of functions `ℕ → ℕ`
contains every function: `f n = e n n + 1` differs from `e n` at the input `n`. -/
theorem cantor_diag (e : ℕ → ℕ → ℕ) : ¬ Function.Surjective e := by
  intro he
  obtain ⟨k, hk⟩ := he (fun n => e n n + 1)
  have : e k k = e k k + 1 := congrFun hk k
  omega

Axioms used: propext, Quot.soundformal/Lumenary/Computability.leanTry it in the Lean web editor

exists_not_computableLean 4Proved here from basic factsFormally verified

/-- **Most functions are not computable.** Every computable `f : ℕ → ℕ` is evaluated by some
program (`Nat.Partrec.Code.exists_code`), different functions need different programs, and there
are only countably many programs. So if every function were computable, `ℕ → ℕ` would be
countable and could be listed as a sequence — contradicting `cantor_diag`. -/
theorem exists_not_computable : ∃ f : ℕ → ℕ, ¬ Computable f := by
  by_contra hall
  push Not at hall
  -- Choose a program for every function.
  have hcode : ∀ f : ℕ → ℕ, ∃ c : Code, c.eval = (f : ℕ →. ℕ) := fun f =>
    Nat.Partrec.Code.exists_code.1 (Partrec.nat_iff.1 (hall f))
  choose code hcode using hcode
  -- Different functions get different programs.
  have hinj : Function.Injective code := by
    intro f g hfg
    funext n
    have h : ((f : ℕ →. ℕ) n) = ((g : ℕ →. ℕ) n) := by
      rw [← hcode f, ← hcode g, hfg]
    exact Part.some_injective h
  -- So `ℕ → ℕ` is countable, hence listed by a sequence, contradicting the diagonal argument.
  have : Countable (ℕ → ℕ) := hinj.countable
  obtain ⟨e, he⟩ := exists_surjective_nat (ℕ → ℕ)
  exact cantor_diag e he