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

<p>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.)</p>

<p>Let $K(x)$ be the Kolmogorov complexity of string $x$.  </p>

<p><strong>lemma</strong>.  <em>$K$ is not computable</em>.</p>

<p><em>Proof</em>.  </p>

<ol>
<li><p>Suppose for contradiction that $K$ is computable.</p></li>
<li><p>Define $K'(x)$ to be the minimum encoding length of any Turing Machine $M$ with $L(M) = \{x\}$.  </p></li>
<li><p>There exists a constant $c$ such that $|K(x) - K'(x)|\le c$ for all strings $x$.</p></li>
<li><p>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$.  </p></li>
<li><p>Since $K$ is computable, so is $f$.</p></li>
<li><p>By <a href="https://en.wikipedia.org/wiki/Kleene&#39;s_recursion_theorem#Rogers.27_fixed-point_theorem" rel="nofollow noreferrer">Roger's fixed-point theorem</a>, $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)$.</p></li>
<li><p>By the definition of $f$ in line 4, we have $L(M_0) = \{x\}$ such that $K(x) &gt; |\langle M_0\rangle| + c$.</p></li>
<li><p>Lines 3 and 7 imply $K'(x) &gt; |\langle M_0\rangle|$.  </p></li>
<li><p>But by the definition of $K'$ in line 2, $K'(x) \le |\langle M_0 \rangle|$, contradicting line 8.</p></li>
</ol>

CC BY-SA 3.0
2017-03-25T18:34:02.020Z
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.)
Andrej Bauer
CC BY-SA 3.0
2017-03-26T01:26:06.917Z
Above my pay grade, @AndrejBauer -- I don't know category theory.  Tried reading [this](http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/) and your answer [here](http://mathoverflow.net/questions/131173/lawveres-fixed-point-theorem-and-the-recursion-theorem).  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?
Neal Young
CC BY-SA 3.0
2017-03-26T09:58:17.557Z
Slides 45 and 46 in http://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).
Andrej Bauer
CC BY-SA 3.0
2017-03-24T16:39:36.140Z
2017-03-28T01:04:31.563Z
2017-03-28T01:04:31.563Z
Neal Young
<p>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 <em>same</em> diagonalization; for more details see, e.g. <a href="https://arxiv.org/abs/math/0305282" rel="nofollow noreferrer">Yanofsky</a>, or for a much more brief and less formalized account  <a href="https://cstheory.stackexchange.com/a/21952/129">my answer</a> to <a href="https://cstheory.stackexchange.com/questions/21917/proof-of-undecidability-not-by-reduction-from-the-halting-problem">this question</a>). </p>

<p>In a comment on the above-mentioned question, Sasho Nikolov pointed out that most of those were special cases of <a href="https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem" rel="nofollow noreferrer">Lawvere's Fixed Point Theorem</a>. 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.</p>

<p>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., <a href="https://mathoverflow.net/questions/139645/applications-of-lawveres-fixed-point-theorem">here</a>, <a href="https://mathoverflow.net/questions/131173/lawveres-fixed-point-theorem-and-the-recursion-theorem">here</a> or <a href="https://arxiv.org/abs/math/0305282" rel="nofollow noreferrer">Yanofsky</a>). 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:</p>

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

CC BY-SA 3.0
2017-03-23T17:16:57.593Z
I should say that all I ever knew about this topic I learned from this blog post by Andrej Bauer: http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/
Sasho Nikolov
CC BY-SA 3.0
2017-03-23T18:52:41.780Z
Could you add a link to a "traditional" proof of the uncomputability of Kolmogorov complexity to help those of us that don't know about it?
Max New
CC BY-SA 3.0
2017-03-23T19:00:04.163Z
@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)$.
Joshua Grochow
CC BY-SA 3.0
2017-03-23T19:36:47.207Z
What you are asking for seems very similar to asking to prove the undecidability of K-complexity via a reduction from, say, the halting problem.  That question is discussed here: http://cstheory.stackexchange.com/questions/31278/proof-for-kolmogorov-complexity-is-uncomputable-using-reductions?rq=1 .
Neal Young
CC BY-SA 3.0
2017-03-23T20:24:42.960Z
@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.
Joshua Grochow
CC BY-SA 3.0
2017-03-23T20:32:12.673Z
For those of us who don't know Lawvere's Theorem, it's setting is a bit abstract ("cartesian closed category"?  "morphism"?).  Does it generalize, say, [Roger's fixed point theorem](http://cs.stackexchange.com/questions/22684/what-is-a-fixed-point-in-the-context-of-rogers-fixed-point-theorem), which may be more familiar to CS folks?
Neal Young
CC BY-SA 3.0
2017-03-23T20:56:19.620Z
@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.
Joshua Grochow
CC BY-SA 3.0
2017-03-23T22:15:24.710Z
@JoshuaGrochow I'd like also an explanation of what Kolmogorov complexity is, I can't really follow your terse proof without more context (also what is C?)
Max New
CC BY-SA 3.0
2017-03-23T22:46:11.720Z
@MaxNew This is the kind of thing you can very easily google for yourself.
Sasho Nikolov
CC BY-SA 3.0
2017-03-23T22:58:22.673Z
I know, and I have, but it would improve the question if there were some links about the proof the question is asking about.
Max New
CC BY-SA 3.0
2017-03-24T04:22:08.187Z
I am actually having trouble seeing how the Berry paradox proof is a diagonalization argument similar to Cantor's.
Sasho Nikolov
CC BY-SA 3.0
2017-03-24T13:44:35.267Z
(To ease notation, identify $M$ with encoding $\langle M \rangle$.)
Let $K(x)$ be K-complexity of $x$.  Assume for contradiction that $K$ is computable. Let $K'(x)$ be the min encoding length of any $M$ s.t. $L(M)=\{x\}$.  There is a constant $c$ s.t. $|K'(x)-K(x)| \le c$ for all $x$.   Define $f( M ) =  M' $ where $L(M') = \{x\}$ for the min $x$ with $K(x) >  | M | + c$.  Function $f$ is computable because $K$ is.  By Roger's, $f$ has a fixed point, that is, there exists $M$ such that $L(M) = L(f( M )) = \{x\}$ with $K(x)   > | M |+c$.  So $K'(x) >  | M |$.  But by defn, $K'(x) \le | M |$.
Neal Young
CC BY-SA 3.0
2017-03-24T13:56:20.740Z
[regarding my last two comments above, my point is to suggest that you can answer your question by using Roger's theorem as a special case of Lawvere's theorem.]
Neal Young
CC BY-SA 3.0
2017-03-24T15:29:53.847Z
@NealYoung: Ah, great! That's basically the standard proof, but phrased in a way so that all of the "action" happens from the fixed point theorem. I'm a little embarrassed to not have seen it myself, but please post it as an answer!
Joshua Grochow
CC BY-SA 3.0
2017-03-24T15:47:10.210Z
See also http://cstheory.stackexchange.com/a/2830
András Salamon
<lo.logic><computability><ct.category-theory><kolmogorov-complexity>
Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?
Joshua Grochow
# Does the uncomputability of Kolmogorov complexity follow from Lawvere's Fixed Point Theorem?

(Asked by: username_0 on 2017-03-23)

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](https://arxiv.org/abs/math/0305282), or for a much more brief and less formalized account [my answer](https://cstheory.stackexchange.com/a/21952/129) to [this question](https://cstheory.stackexchange.com/questions/21917/proof-of-undecidability-not-by-reduction-from-the-halting-problem)).

In a comment on the above-mentioned question, username_1 pointed out that most of those were special cases of [Lawvere's Fixed Point Theorem](https://ncatlab.org/nlab/show/Lawvere%27s+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](https://mathoverflow.net/questions/139645/applications-of-lawveres-fixed-point-theorem), [here](https://mathoverflow.net/questions/131173/lawveres-fixed-point-theorem-and-the-recursion-theorem) or [Yanofsky](https://arxiv.org/abs/math/0305282)). 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?

**Tags:** lo.logic, computability, ct.category-theory, kolmogorov-complexity

> **Comments:**
> **username_1**: I should say that all I ever knew about this topic I learned from this blog post by username_5: http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/  
> **username_2**: Could you add a link to a "traditional" proof of the uncomputability of Kolmogorov complexity to help those of us that don't know about it?  
> **username_0**: @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)$.  
> **username_3**: What you are asking for seems very similar to asking to prove the undecidability of K-complexity via a reduction from, say, the halting problem.  That question is discussed here: http://cstheory.stackexchange.com/questions/31278/proof-for-kolmogorov-complexity-is-uncomputable-using-reductions?rq=1 .  
> **username_0**: @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.  
> **username_3**: For those of us who don't know Lawvere's Theorem, it's setting is a bit abstract ("cartesian closed category"?  "morphism"?).  Does it generalize, say, [Roger's fixed point theorem](http://cs.stackexchange.com/questions/22684/what-is-a-fixed-point-in-the-context-of-rogers-fixed-point-theorem), which may be more familiar to CS folks?  
> **username_0**: @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.  
> **username_2**: @JoshuaGrochow I'd like also an explanation of what Kolmogorov complexity is, I can't really follow your terse proof without more context (also what is C?)  
> **username_1**: @MaxNew This is the kind of thing you can very easily google for yourself.  
> **username_2**: I know, and I have, but it would improve the question if there were some links about the proof the question is asking about.  
> **username_1**: I am actually having trouble seeing how the Berry paradox proof is a diagonalization argument similar to Cantor's.  
> **username_3**: (To ease notation, identify $M$ with encoding $\langle M \rangle$.) Let $K(x)$ be K-complexity of $x$.  Assume for contradiction that $K$ is computable. Let $K'(x)$ be the min encoding length of any $M$ s.t. $L(M)=\{x\}$.  There is a constant $c$ s.t. $|K'(x)-K(x)| \le c$ for all $x$.   Define $f( M ) =  M' $ where $L(M') = \{x\}$ for the min $x$ with $K(x) >  | M | + c$.  Function $f$ is computable because $K$ is.  By Roger's, $f$ has a fixed point, that is, there exists $M$ such that $L(M) = L(f( M )) = \{x\}$ with $K(x)   > | M |+c$.  So $K'(x) >  | M |$.  But by defn, $K'(x) \le | M |$.  
> **username_3**: [regarding my last two comments above, my point is to suggest that you can answer your question by using Roger's theorem as a special case of Lawvere's theorem.]  
> **username_0**: @NealYoung: Ah, great! That's basically the standard proof, but phrased in a way so that all of the "action" happens from the fixed point theorem. I'm a little embarrassed to not have seen it myself, but please post it as an answer!  
> **username_4**: See also http://cstheory.stackexchange.com/a/2830  

---

## 1 answers

### Answer by username_3 on 2017-03-24. Score: 14

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*.

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](https://en.wikipedia.org/wiki/Kleene's_recursion_theorem#Rogers.27_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.

> **Comments:**
> **username_5**: 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.)  
> **username_3**: Above my pay grade, @AndrejBauer -- I don't know category theory.  Tried reading [this](http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/) and your answer [here](http://mathoverflow.net/questions/131173/lawveres-fixed-point-theorem-and-the-recursion-theorem).  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?  
> **username_5**: Slides 45 and 46 in http://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).  

---

