18

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?

Community
  • 1
Joshua Grochow
  • 37,260
  • 4
  • 129
  • 228
  • 2
    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 Mar 23 '17 at 17:16
  • 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 Mar 23 '17 at 18:52
  • 1
    @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 Mar 23 '17 at 19:00
  • 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 Mar 23 '17 at 19:36
  • 2
    @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 Mar 23 '17 at 20:24
  • 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, which may be more familiar to CS folks? – Neal Young Mar 23 '17 at 20:32
  • 1
    @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 Mar 23 '17 at 20:56
  • @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 Mar 23 '17 at 22:15
  • 1
    @MaxNew This is the kind of thing you can very easily google for yourself. – Sasho Nikolov Mar 23 '17 at 22:46
  • 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 Mar 23 '17 at 22:58
  • I am actually having trouble seeing how the Berry paradox proof is a diagonalization argument similar to Cantor's. – Sasho Nikolov Mar 24 '17 at 04:22
  • 1
    (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 Mar 24 '17 at 13:44
  • 1
    [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 Mar 24 '17 at 13:56
  • @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 Mar 24 '17 at 15:29
  • 3
    See also http://cstheory.stackexchange.com/a/2830 – András Salamon Mar 24 '17 at 15:47

1 Answers1

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, $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.

Neal Young
  • 10,546
  • 33
  • 60
  • 4
    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 Mar 25 '17 at 18:34
  • 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? – Neal Young Mar 26 '17 at 01:26
  • 4
    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 Mar 26 '17 at 09:58