Can Incompleteness be Computable?

Question

Chaitin's incompleteness theorem says no sufficiently strong theory of arithmetic can prove $K(x) > L$ where $K(x)$ is the Kolmogorov complexity of natural number $x$ and $L$ is a sufficiently large constant. The size of $L$ depends on the theory.

The usual definitions for the Kolmogorov complexity of a natural number are uncomputable in general. One such definition uses busy beavers. Let $K(x)$ be the size of the smallest 2-symbol BB that writes exactly $x$ $1's$ and halts. $K(x)$ is uncomputable because it requires determining whether all BB's below a certain size halt. There are 5 state BB's that no one has been able to prove halt or don't halt.

Let $K^{'}(x)$ be the size of the smallest 2-symbol BB that halts after exactly $x$ steps. $K^{'}(x)$ is computable. We can ignore any BB that doesn't halt in $x$ steps. Does Chaitin's incompleteness theorem allow us to prove no sufficiently strong theory of arithmetic can prove $K^{'}(x) > L$ where $L$ is sufficiently large?

It seems it must. Chaitin's incompleteness theorem is a formalization of Berry's paradox, "the smallest positive integer not definable in fewer than twelve words". I don't see why computability of the complexity measure would make any difference.

Answer 1

$K'(x)$ is computable so you can effectively compute it ! Hence you can prove $K'(x)=y$ for any $x$ and prove $K'(x)>L$ for any $x$ as well...

Answer 2

Consider the "lazy Berry paradox":

Let $x$ be the smallest integer not provably describable in fewer than $10^{10}$ characters.

More formally,

Let $x$ be the smallest integer such that there is no pair $(\varphi, P)$, such that $\varphi$ is a formula defining $x$ and $P$ is a proof that $\varphi$ defines $x$, and the sum of the lengths of $\varphi$ and $P$ is at most $10^{10}$.

This actually isn't a paradox at all! We can find this $x$ effectively. Now, it will take a while - about $10^{10}$ "steps" - but we can do it.

$K'$ is to $K$ as the lazy Berry paradox is to the Berry paradox. $K'$ is perfectly computable, if laboriously so, and so no version of Chaitin's argument applies.