Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, Gödel Incompleteness, Chaitin Incompleteness, Russell's paradox, etc. - all have essentially the same proof by diagonalization (note that this is more specific than that they can all be proved by diagonalization; rather, it feels that all of these theorems really use the same diagonalization; for more details see, e.g. Yanofsky, or for a much more brief and less formalized account my answer to this question).

In a comment on the above-mentioned question, Sasho Nikolov pointed out that most of those were special cases of Lawvere's Fixed Point Theorem. If they were all special cases, then this would be a good way to capture the above idea: there really would be one result with one proof (Lawvere's) from which all of the above followed as direct corollaries.

Now, for Gödel Incompleteness and undecidability of the halting problem and their friends, it is well-known that they follow from Lawvere's Fixed Point Theorem (see, e.g., here, here or Yanofsky). But I don't immediately see how to do that for the undecidability of Kolmogorov complexity, despite the fact that the underlying proof is somehow "the same." So:

Is the undecidability of Kolmogorov complexity a quick corollary - requiring no additional diagonalization - of Lawvere's Fixed Point Theorem?

  • 2
    $\begingroup$ I should say that all I ever knew about this topic I learned from this blog post by Andrej Bauer: math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem $\endgroup$ – Sasho Nikolov Mar 23 '17 at 17:16
  • 1
    $\begingroup$ @MaxNew: Let $f$ be a computable function, computed by some TM $M$. Let $M_k$ be the following TM: on empty input, it starts going through strings one at a time until it finds an $x$ with $f(x) \geq |x| > k$ and output $x$. Note that $|M_k| \leq \log_2(k) + c$ for some $c$ depending only on $|M|$. Then for any $k$ such that $k > |M_k|$ (any sufficiently large $k$ will do), either there is no such $x$ (in which case $f \neq C$) or $M_k$ outputs some $x$ such that $f(x) \geq |x| > k$ (by construction), but the fact that $M_k$ output $x$ implies that $C(x) \leq |M_k| < k$, so $f(x) \neq C(x)$. $\endgroup$ – Joshua Grochow Mar 23 '17 at 19:00
  • 2
    $\begingroup$ @NealYoung: Similar, but those don't quite answer my question. Reducing from the halting problem is taking HALT to be the "source" of uncomputability and then using reductions. But (e.g.) the proof I gave in the comments above shows that you can also take K-complexity as the "source of uncomputability," but by a very similar proof to that for HALT. Can that similar proof actually be shown to be the same in some technical sense? (In this case, by showing that they are all instances of Lawvere's Theorem, which seems to me stronger than many kinds of reduction.) That's what I'm really after. $\endgroup$ – Joshua Grochow Mar 23 '17 at 20:24
  • 1
    $\begingroup$ @NealYoung: Yes, it generalizes Roger's fixed point theorem. But if you only think of it as Roger's Theorem you will be missing the point; the point is that Lawvere's is general enough to capture the proof strategy of many different proofs, beyond that in Roger's. The Yonofsky paper linked to in the question is intended to be a "category-free" exposition of Lawvere's Theorem, friendly to people for whom the category theory of Lawvere might be intimidating. $\endgroup$ – Joshua Grochow Mar 23 '17 at 20:56
  • 3
    $\begingroup$ See also cstheory.stackexchange.com/a/2830 $\endgroup$ – András Salamon Mar 24 '17 at 15:47

EDIT: Adding the caveat that Roger's fixed-point theorem may not be a special case of Lawvere's.

Here is a proof that may be "close"... It uses Roger's fixed-point theorem instead of Lawvere's theorem. (See comment section below for further discussion.)

Let $K(x)$ be the Kolmogorov complexity of string $x$.

lemma. $K$ is not computable.


  1. Suppose for contradiction that $K$ is computable.

  2. Define $K'(x)$ to be the minimum encoding length of any Turing Machine $M$ with $L(M) = \{x\}$.

  3. There exists a constant $c$ such that $|K(x) - K'(x)|\le c$ for all strings $x$.

  4. Define function $f$ such that $f(\langle M \rangle) = \langle M' \rangle$ where $L(M') = \{x\}$ such that $x$ is the minimum string such that $K(x) > |\langle M\rangle| + c$.

  5. Since $K$ is computable, so is $f$.

  6. By Roger's fixed-point theorem, $f$ has a fixed point, that is, there exists a Turing Machine $M_0$ such that $L(M_0) = L(M_0')$ where $\langle M_0' \rangle = f(\langle M_0\rangle)$.

  7. By the definition of $f$ in line 4, we have $L(M_0) = \{x\}$ such that $K(x) > |\langle M_0\rangle| + c$.

  8. Lines 3 and 7 imply $K'(x) > |\langle M_0\rangle|$.

  9. But by the definition of $K'$ in line 2, $K'(x) \le |\langle M_0 \rangle|$, contradicting line 8.

  • 4
    $\begingroup$ As far as I know Roger's fixed-point theorem is not an instance of Lawvere's fixed-point theorem. It is a variant, though, because in the effective topos it reads as follows: if $f : \mathbb{N} \rightrightarrows A^\mathbb{N}$ is a mutlivalued surjection then $A$ has the fixed-point property. (Lawvere's theorem in the effective topos is: if $f : B \to A^B$ is a surjection then $A$ has the fixed-point property.) $\endgroup$ – Andrej Bauer Mar 25 '17 at 18:34
  • $\begingroup$ Above my pay grade, @AndrejBauer -- I don't know category theory. Tried reading this and your answer here. Still don't get it. Can you tell me, in your comment above, for Rogers' theorem, what do you take for the function $f$ (with type $f:\mathbb{N}\overrightarrow{\rightarrow} A^{\mathbb{N}}$), and what is $A$? Or maybe suggest an appropriate tutorial? $\endgroup$ – Neal Young Mar 26 '17 at 1:26
  • 4
    $\begingroup$ Slides 45 and 46 in math.andrej.com/wp-content/uploads/2007/05/syncomp-mfps23.pdf (the good news is that now I have a definite plan and a deadline for writing up an extensive paper on synthetic computability). $\endgroup$ – Andrej Bauer Mar 26 '17 at 9:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.