In the Kritchman-Raz paper the authors recall Chaitin's proof of a version of the first incompleteness theorem (italics are mine):
Chaitin’s incompleteness theorem states that for any rich enough consistent mathematical theory [$T$], there exists a (large enough) integer $L$ (depending on the theory and on the programming language that is used to define Kolmogorov complexity), such that, for any integer $x$, the statement “$K(x) > L$” cannot be proved within the theory [$T$].
The proof given by Chaitin is as follows. Let $L$ be a large enough integer. Assume for a contradiction that for some integer $x$, there is a proof for the statement “$K(x) > L$”. Let $w$ be the first proof (say, according to the lexicographic order) for a statement of the form $“K(x) > L”$. Let $z$ be the integer $x$ such that $w$ proves “$K(x) > L$”. It is easy to give a computer program that outputs $z$: the program enumerates all possible proofs $w$, one by one, and for the first $w$ that proves a statement of the form “$K(x) > L$”, the program outputs $x$ and stops. The length of this program is a constant $+ \log L$. Thus, if $L$ is large enough, the Kolmogorov complexity of z is less than $L$. Since $w$ is a proof for “$K(z) > L$” (which is a false statement), we conclude that the theory is inconsistent.
Some questions:
This proof seems to use the stronger assumption that $T$ is sound instead of just consistent (see italics). What is going on here? I guess you can proceed as follows: the argument establishes that $T \vdash K(x) > L$ implies $K(x) = k$ for some $k < L$. But $K(x) = k$ is $\Sigma_1$, so also $T \vdash K(x) = k$ and hence $T \vdash \bot$. Therefore the consistency of $T$ implies that $T \nvdash K(x) > L$ (as we wished). Is this the implicit argument? I don't find it very clear.
The authors also say that this is a formalization of Berry's paradox using Kolmogorov Complexity. Why is that? Berry's paradox is:
Consider the expression “the smallest positive integer not definable in under eleven words”. This expression defines that integer in under eleven words.
So a formalization would be:
Consider the program that searches for the smallest $x$ such that $K(x) > C$. This program has size less than $C$ (if $C$ is large enough).
The problem here is of course that $K(x)$ is not computable. But how does this relate to Chaitin's proof?
Re: $(1)$, you have the right idea: there is indeed an implicit argument that mere consistency is enough. However, what you've written isn't exactly right since "$K(x)=L$" is not in general $\Sigma_1$ (it's merely $\Sigma_1\wedge\Pi_1$). Rather, you want to focus on the sentence "$K(x)\le L$:" this is $\Sigma_1$ since it amounts to the existence of a single computation, and so our theory can verify each of its true instances. So if in reality $K(x)\le L$ but we prove $K(x)>L$ then we're inconsistent. (More snappily, this amounts to saying: consistency implies $\Pi_1$-soundness since the theory in question is $\Sigma_1$-complete, and "$K(x)>L$" is $\Pi_1$.)
Re: $(2)$, the point is that if $T$ were to prove enough Kolmogorov lower bounds then we could use it to whip up a "computable version" of your idea. Specifically, consider the machine $M$ which on input $c$ searches through $T$-proofs for a proof of the form "$K(n)>c$" for some $n$, halting and outputting the corresponding $n$ once it finds one. Assuming that for each $a$ there is some $b$ such that $T\vdash K(b)>a$, this machine always halts, but this gives a contradiction once $c$ is large enough. You can think of $M$ as - on input $c$ - looking for "the natural number which most obviously takes $>c$-many symbols to concretely describe," where "concretely" refers to $T$-provability and "most obviously" refers to our search through proofs (the idea being that shorter proof = more obviousness).