I'm interested in examples of theorems that employ the proof techniques that are utilized in the proof of the undecidability of Kolmogorov Complexity.
Definition:(Sipser) Let x be a binary string. We say that the minimal description of x, written as d(x), is the shortest string $\langle$M,w$\rangle$ where TM M on input w halts with x on its tape. So, the Kolmogorov Complexity K(x) is written as, K(x)=|d(x)|. K(x) is defined to be the length of minimal description of x.
Theorem: K(x) is not a computable function.
Proof/Sketch of Proof (attributed to Chor): Proof of negation. $\forall$n, let $y_{n}$ be the lexicographical first string y that satisfies n < K(y). Consider the following TM M: On input n (encoded in binary), M generates one by one all binary strings $x_{0}$, $x_{1}$, $x_{2}$, $x_{3}$... in lexicographic order.
For each $x_{i}$ it produces, M computes K($x_{i}$).
If K($x_{i}$) > n, then the TM M, outputs $x_{i}$ and halts. Else, the TM M, continues to examine the next lexicographical string $x_{i+1}$.
Since the function K is unbounded, it is guaranteed that M will eventually come across a string x satisfying K(x) $>$ n.
Question: what will the TM M output on input n?
By definition on input n TM M outputs $y_{n}$ (the lexicographical first string whose Kolmogorov complexity exceeds n, K(x) > n), but the length of n is $log_{2}$(n). So we have $K_{M}$($y_{n}$) $\leq$ $log_{2}$(n). There is a constant $c_{M}$ such that $\forall$y, K(y) $\leq$ $K_{M}$(y) + $c_{M}$, so $\forall$n K($y_{n}$) $\leq$ $log_{2}$(n) + $c_{M}$.
By definition of $y_{n}$ for all n, n < K($y_{n}$). By combining the two inequalities we get: n < $log_{2}$(n) + $c_{M}$, but for large enough n this is false. Thus a contradiction.
Question: What other theorems utilize a similar proof technique in their proofs?
For example: The proof that the set of incompressible strings is undecidable is very similar with some slight modifications.
