The motivation for this question is the fact that most n-bit strings are incompressible. Intuitively, we can propose by analogy that most proofs for Tautologies are incompressible to polynomial size. Basically, my intuition is that some proofs are inherently random and can't be compressed.

Is there a good reference on research effort related to using Kolmogorov complexity results to establish super-polynomial lower bounds on the proof size of Tautologies?

In this Ph.D. dissertation On the Complexity of Propositional Proof Systems the Incompressibility method from Kolmogorov Complexity is used to obtain Urquhart's $\Omega(n/\log n)$ lower bound for a class of Tautologies. I wonder if there are stronger results using the Incompressibility method or other results from Kolmogorov complexity?

  • 4
    $\begingroup$ Kolmogorov complexity would not seem to be useful for Tautologies. For any formal system, the lexicographically first proof that an $n$-bit formula is a tautology is in fact extremely compressible: it can be described in $n+O(1)$ bits, by specifying the formula along with a program that tries all proofs in some formal system in lexicographical order. It would make more sense to look at time-bounded versions of Kolmogorov complexity. $\endgroup$ Commented Sep 13, 2010 at 4:31
  • $\begingroup$ I was not clear, I mean Kolmogorov complexity results. Question is edited. $\endgroup$ Commented Sep 13, 2010 at 4:43
  • 3
    $\begingroup$ Ryan's comment is still appropriate, even after the edit. Unless you bound some resource, the Kolmogorov complexity of any proof is a constant (for the fixed brute-force proof enumerator) plus the size of the sentence. So this way you can't get better lower bounds than linear. $\endgroup$ Commented Sep 13, 2010 at 9:49
  • 2
    $\begingroup$ Your question specifically asks about "super-polynomial lower bounds". Ryan's argument shows that the answer is trivially no, as the Kolmogorov complexity is at most linear. Galesi's lower bound is sublinear, let alone superpolynomial. $\endgroup$ Commented Sep 13, 2010 at 13:18
  • 1
    $\begingroup$ @turkistany: please see meta.cstheory.stackexchange.com/questions/300/…. $\endgroup$
    – Kaveh
    Commented Sep 14, 2010 at 1:27

1 Answer 1


Arvind, Köbler, Mundhenk, and Torán introduced the notion of time-bounded nondeterministic instance complexity. Based on a quick reading, It seems they use Kolmogorov complexity measure that depends on the size of shortest nondeterministic TM. They were able to prove the existence of hard to prove Tautologies under a notion of hardness based on nondeterministic instance complexity.

Vikraman Arvind, Johannes Köbler, Martin Mundhenk, Jacobo Torán, Nondeterministic Instance Complexity and Hard-to-Prove Tautologies,


Your Answer

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

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