6
$\begingroup$

Note. The title was modified. Previous title was "Every theorem t has a proof no more complex than~|t|. Is this right?"

The question ("Is Kolmogorov complexity (KC) relevant for proof theory?") arises because every theorem has a proof with low Kolmogorov complexity". To be more specific,

Every theorem $t$ has a proof $p$ with $K(p)\leq K(t)+c\leq|t|+c'$, where $c$ and $c'$ are constants.
Proof: It is assumed that there is a proof checking algorithm $C(x)$ that outputs TRUE if $x$ is a correct proof, FALSE otherwise. Then there exists a fixed (depending on the formal system) Turing machine $M$ with Input: $t$ a string (that may be a theorem)
- $M$ enumerates all the proofs until (and if) $t$ is proved.
- When $t$ is proved, print the proof $p$ and halt.
Thus, if $t$ is a theorem, $M(t)$ prints a proof of $t$.
Using the universal TM, we get $ K(p) \leq K(t) + c \leq |t| + c' $ where $c$ and $c'$ are constants.

Thus, and apart from a constant, no theorem needs a proof with Kolmogorov complexity greater than $|t|$. To me this seems a bit strange.

In other words, the number of bits of "inspiration" (or "non-deterministic bits", or "oracle bits") needed to prove any theorem $t$ is at most $|t|+c$.

If this is true, the very lengthy proofs that sometimes are needed to prove some simple to state theorems are necessarily very regular / structured / compressible (synonymous).

Improve this question
$\endgroup$
8
  • 3
    $\begingroup$ The technical part is correct, but I disagree with the interpretation. The fact that a proof can be (in principle) found by exhaustive search does not make it in any way regular or structured. $\endgroup$
    – Emil Jeřábek
    Commented Jan 24, 2014 at 13:24
  • 13
    $\begingroup$ This is why people don't use Kolmogorov complexity to measure proof length: it's not very meaningful to compress a proof of the classification of finite simple groups all the way down to essentially saying "it's the shortest proof of the classification of finite simple groups". I wouldn't interpret Kolmogorov complexity as "bits of inspiration", though, since almost all these bits are just stating the theorem and describing the formal proof system. All you need is one bit of inspiration: if you know there is a proof, then you can definitely find it by brute force if you search long enough. $\endgroup$
    – Henry Cohn
    Commented Jan 24, 2014 at 13:55
  • 3
    $\begingroup$ What exactly is the question here? (Also, Henry's comment is spot-on.) $\endgroup$
    – Noah Schweber
    Commented Jan 24, 2014 at 18:37
  • 1
    $\begingroup$ Would you say that the digits of $\pi$ are "very regular, structured, and compressible"? After all, the first $n$ digits of $\pi$ have Kolmogorov complexity at most $\log(n) + c$. I guess they compress pretty well, but they don't look regular to me... Perhaps what makes your thesis unsatisfying is that you don't measure the other resources required to run the program that finds the proof. $\endgroup$
    – Sam Nead
    Commented Jan 24, 2014 at 19:31
  • 1
    $\begingroup$ I think a better measure for proof theory would actually be time and space complexity, in the computational sense. In the KC sense, a description of just $k$ bits can produce a $BB(k)$-length string (busy beaver function). So perhaps there is "order", but it is very hard to work with. On the other hand, if you can make a time-complexity statement, this may be a much more reasonable measure of regularity or simplicity. $\endgroup$
    – usul
    Commented Jan 25, 2014 at 13:14

1 Answer 1

Reset to default
2
$\begingroup$

After making the above comment I did a quick Google search and found a paper entitled "Kolmogorov Complexity and Computational Complexity" by Lance Fortnow. The paper is about resource-bounded variants of Kolmogorov complexity. After giving the standard definition and some consequences he writes the following.

Of course this definition of Kolmogorov complexity makes any complexity theorist cringe: what good is a small program [for] $x$ if it takes the life of the universe to produce $x$?

Perhaps he could give you more precise pointers to the literature.

[Edit] - Your main observation has been made before, by Henry Cohn, on MathOverflow. See the last paragraph of his answer here.

Improve this answer
$\endgroup$

Not the answer you're looking for? Browse other questions tagged .