18
$\begingroup$

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?

Improve this question
$\endgroup$
15
  • 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, 2017 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, 2017 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, 2017 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, 2017 at 20:56
  • 3
    $\begingroup$ See also cstheory.stackexchange.com/a/2830 $\endgroup$
    – András Salamon
    Mar 24, 2017 at 15:47

1 Answer 1

Reset to default
14
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 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, 2017 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, 2017 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, 2017 at 9:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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