<p>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.</p>

<p>Vikraman Arvind, Johannes Köbler, Martin Mundhenk, Jacobo Torán,
<a href="http://portal.acm.org/citation.cfm?id=646514.695827" rel="nofollow">Nondeterministic Instance Complexity and Hard-to-Prove Tautologies, </a>
<a href="http://portal.acm.org/citation.cfm?id=646514.695827" rel="nofollow"></a></p>

CC BY-SA 2.5
2010-09-15T02:12:41.570Z
2010-09-15T02:12:41.570Z
Mohammad Al-Turkistany
<p>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.</p>

<blockquote>
  <p>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?</p>
</blockquote>

<p>In this Ph.D. dissertation 
<a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.37.3250&amp;rep=rep1&amp;type=pdf">On the Complexity of Propositional Proof Systems
</a>
<a href="http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.37.3250&amp;rep=rep1&amp;type=pdf"></a>  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?</p>

CC BY-SA 2.5
2010-09-13T04:31:27.620Z
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.
Ryan Williams
CC BY-SA 2.5
2010-09-13T04:43:03.063Z
I was not clear, I mean Kolmogorov complexity results. Question is edited.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-09-13T06:24:45.013Z
I suspect that might be possible, maybe something similar to using formulas expressing circuit complexity lowerbounds to obtain hard tautologies, but I was not able to find anything in the proof complexity books I have or on the pages of famous proof complexity theorists I checked or between Eric Allender's papers. There is a relativized world result by Buhrman, Fenner, Fortnow and van Melkebeek from 2000 but don't know if it is what you are looking for. There might be something in Li and Vitani but I don't have it right now to check, and others may know better.
Kaveh
CC BY-SA 2.5
2010-09-13T09:49:20.623Z
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.
András Salamon
CC BY-SA 2.5
2010-09-13T13:18:51.533Z
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.
András Salamon
CC BY-SA 2.5
2010-09-13T13:51:34.410Z
@András, What if we exclude any brute-force algorithms?
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-09-13T13:57:32.330Z
Neither "proof" nor "proof complexity" appears in the index of Li and Vitanyi, 3rd ed.
Aaron Sterling
CC BY-SA 2.5
2010-09-13T14:42:01.870Z
@András: Thank you for checking Li and Vitanyi. I think I understood the question in a different way. For me, the question was not about Kolmogorov complexity of hard tautologies, it was about using Kolmogorov complexity (indirectly) to create hard tautologies. But I guess this was not what turkistany had in his mind.
Kaveh
CC BY-SA 2.5
2010-09-13T20:08:50.123Z
Excluding brute-force might work, but what is a good way to define this?  There is no "universal" definition of brute-force.  It seems easier to bound the resources that the algorithm can use.
András Salamon
CC BY-SA 2.5
2010-09-14T01:27:50.643Z
@turkistany: please see http://meta.cstheory.stackexchange.com/questions/300/how-to-ask-a-good-question.
Kaveh
CC BY-SA 2.5
2010-09-14T01:49:04.437Z
@Kaveh, Thanks. One such question got the attention of distinguished scholar and he spent some of his valuable time to provide an excellent answer. [http://cstheory.stackexchange.com/questions/668/is-there-a-complexity-theory-analogue-of-rices-theorem-in-computability-theory](http://cstheory.stackexchange.com/questions/668/is-there-a-complexity-theory-analogue-of-rices-theorem-in-computability-theory)
Mohammad Al-Turkistany
<lower-bounds><proof-complexity><kolmogorov-complexity>
Using Kolmogorov complexity to establish proof complexity lower bounds?
Mohammad Al-Turkistany
# Using Kolmogorov complexity to establish proof complexity lower bounds?

(Asked by: username_0 on 2010-09-13)

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](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.37.3250&rep=rep1&type=pdf)
 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?

**Tags:** lower-bounds, proof-complexity, kolmogorov-complexity

> **Comments:**
> **username_1**: 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.  
> **username_0**: I was not clear, I mean Kolmogorov complexity results. Question is edited.  
> **username_2**: I suspect that might be possible, maybe something similar to using formulas expressing circuit complexity lowerbounds to obtain hard tautologies, but I was not able to find anything in the proof complexity books I have or on the pages of famous proof complexity theorists I checked or between Eric Allender's papers. There is a relativized world result by Buhrman, Fenner, Fortnow and van Melkebeek from 2000 but don't know if it is what you are looking for. There might be something in Li and Vitani but I don't have it right now to check, and others may know better.  
> **username_3**: 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.  
> **username_3**: 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.  
> **username_0**: @András, What if we exclude any brute-force algorithms?  
> **username_4**: Neither "proof" nor "proof complexity" appears in the index of Li and Vitanyi, 3rd ed.  
> **username_2**: @András: Thank you for checking Li and Vitanyi. I think I understood the question in a different way. For me, the question was not about Kolmogorov complexity of hard tautologies, it was about using Kolmogorov complexity (indirectly) to create hard tautologies. But I guess this was not what turkistany had in his mind.  
> **username_3**: Excluding brute-force might work, but what is a good way to define this?  There is no "universal" definition of brute-force.  It seems easier to bound the resources that the algorithm can use.  
> **username_2**: @turkistany: please see http://meta.cstheory.stackexchange.com/questions/300/how-to-ask-a-good-question.  
> **username_0**: @username_2, Thanks. One such question got the attention of distinguished scholar and he spent some of his valuable time to provide an excellent answer. [http://cstheory.stackexchange.com/questions/668/is-there-a-complexity-theory-analogue-of-rices-theorem-in-computability-theory](http://cstheory.stackexchange.com/questions/668/is-there-a-complexity-theory-analogue-of-rices-theorem-in-computability-theory)  

---

## 1 answers

### Answer by username_0 on 2010-09-15. Score: 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,](http://portal.acm.org/citation.cfm?id=646514.695827)


---

