Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem? Many theorems and "paradoxes" - Cantor's diagonalization, undecidability of hatling, undeciability of Kolmogorov complexity, G&ouml;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&ouml;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?
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.

Proof.  


Suppose for contradiction that $K$ is computable.
Define $K'(x)$ to be the minimum encoding length of any Turing Machine $M$ with $L(M) = \{x\}$.  
There exists a constant $c$ such that $|K(x) - K'(x)|\le c$ for all strings $x$.
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) &gt; |\langle M\rangle| + c$.  
Since $K$ is computable, so is $f$.
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)$.
By the definition of $f$ in line 4, we have $L(M_0) = \{x\}$ such that $K(x) &gt; |\langle M_0\rangle| + c$.
Lines 3 and 7 imply $K'(x) &gt; |\langle M_0\rangle|$.  
But by the definition of $K'$ in line 2, $K'(x) \le |\langle M_0 \rangle|$, contradicting line 8.