<p>As I mentioned in the comments, you need to first clarify what you exactly mean by a proof system.</p>

<p>Josh discusses the case where one uses the original definition of a proof system according to Cook-Reckhow.</p>

<p>There is an alternative definition which is also common: a proof system is a binary relation $R$ computable in polynomial time (and satisfying some conditions like soundness) and we say $\pi$ is an $R$-proof of $\varphi$ iff $R(\pi,\varphi)$.</p>

<p>With this definition it is easy to show that there can be a proof system where the K-complexity of a formula is much higher than the K-complexity of some proof of it.</p>

<p>E.g., let $R$ be some usual proof system modified as follows: we first check if $\varphi$ is of the form $\top \lor \psi$ for some formula $\psi$, if that is the case we accept the empty string as a proof of $\varphi$. Otherwise, we fall back to the original proof system.</p>

<p>Since $\psi$ can be any formula the K-complexity of $\varphi$ can be arbitrary high. However the K-compleixty of the empty string which is a proof of $\varphi$ is trivial.</p>

CC BY-SA 3.0
2013-09-17T04:05:09.383Z
2013-09-17T04:14:24.563Z
2013-09-17T04:14:24.563Z
Kaveh
<p>In most "standard" proof systems, the formula $\varphi$ being proved is usually part of the proof itself by definition of the proof system, in which case for all $\varphi$, $K(\varphi) \leq K(\text{proof}) + O(1)$ (the extra constant is for the part of the program which says, basically, "extract the last line of the proof" - anyways, additive $O(1)$ errors are the best one can hope for in Kolmogorov complexity). </p>

<p>Even in a proof system where all that is required is that the formula $\varphi$ appear somewhere amongst the lines of the proof $\pi$, one can still get $K(\varphi) \leq K(\pi) + O(\log|\pi|)$, where here the extra $\log|\pi|$ bits are used to describe the index $i$ of the line of the proof that corresponds to $\varphi$.</p>

<p>In the much more general Cook-Reckhow style of proof system (or its computable analog) - that is, a polynomial-time computable function $f$ (resp., just a computable function $f$) whose range is exactly the set of true sentences of your theory - again, $K(\varphi) \leq K(\text{proof}) + O(1)$, where here the $O(1)$ extra bits describe the function $f$.</p>

<p>(Note that the trick of hard-coding certain tautologies into your proof system, pointed out by Kaveh, is handled by this latter case, as the hard-coded tautologies must be encoded directly into $f$, so they contribute to/are handled by the $O(1)$.)</p>

CC BY-SA 3.0
2013-09-17T02:08:57.747Z
2013-09-17T02:08:57.747Z
Joshua Grochow
<p>Are there a complete decidable $\mathcal{L}$-theory, a formula $\phi$ and a proof of $\phi$ for which the Kolmogorov complexity of the proof of $\phi$ is less than the Kolmogorov complexity of $\phi$?</p>

<p>Proofs in the proof systems I have seen so far are of the form:</p>

<ol>
<li><p><i>mathematical reasoning</i></p></li>
<li><p>therefore $\phi$</p></li>
</ol>

<p>Hence our intuition tells us that the Kolmogorov complexity of the proof has to be at least the Kolmogorov complexity of $\phi$. But this intuition does not prove any statement formally and it does not exclude the possibility of having a proof system where $p$ would be a proof of $\phi$ while Kolmogorov($p$) &lt; Kolmogorov($\phi$) or even Kolmogorov(<i>mathematical reasoning</i> concatenate $\phi$) &lt; Kolmogorov($\phi$).</p>

CC BY-SA 3.0
2013-09-16T01:21:47.667Z
I assume the existence of the proof system within the theory $\mathcal{L}$ given, however I do not claim any other properties about the proof system. $\phi$ has at least one proof since $\mathcal{L}$-theory is complete, it is allowed to have more proofs. The question asks if it is possible for some proof of some $\phi$ to have a lower Kolmogorov complexity than $\phi$.
Dávid Natingga
CC BY-SA 3.0
2013-09-16T04:14:47.283Z
Are you implying that the Kolmogorov complexity of a string is always more than or equal to the Kolmogorov complexity of its substrings? And what is the definition of a "proof system"? Do you mean something similar to Cook-Reckhow definition of a proof system or are you talking informally (in which case you should define what you mean by a proof system). Also as Ricky said, which proof of $\varphi$? Or do you mean every proof of $\varphi$?
Kaveh
CC BY-SA 3.0
2013-09-16T04:20:03.133Z
It is easy to create proof systems where the Kolmogorov complexity of a proof of a formula is less than the Kolmogorov complexity the formula: just make the empty string be the proof of your true formula and hard code it in the proof system. Then the Kolmogorov complexity of the proof of the formula is $0$ while the formula can have arbitrary large Kolmogorov complexity.
Kaveh
CC BY-SA 3.0
2013-09-16T16:15:14.027Z
How would I define such a proof system and a theory? Could you please provide a very simple example?
Dávid Natingga
CC BY-SA 3.0
2013-09-16T19:08:50.567Z
@Kaveh: I think if you ask for the statement for infinitely many $\varphi$ your trick no longer works.
Joshua Grochow
CC BY-SA 3.0
2013-09-16T21:10:22.017Z
@Joshua, I think we can even hard-code a family of tautologies with high Kolmogorov complexity, e.g. $\top \lor (\text{some high Kolmogorov complexity statement})$.
Kaveh
CC BY-SA 3.0
2013-09-16T21:11:23.443Z
@David, you just hard code it, that is you simply define the empty string to be a proof of the statement.
Kaveh
CC BY-SA 3.0
2013-09-16T22:11:26.130Z
@Kaveh I know how to define a language and a theory, not how to define the proof system within the theory. If it is something simple, I would greatly appreciate an example with hardcoding. Otherwise, a satisfying answer to my question will have to be on hold until I learn more on proof theory. As of now your hardcoding argument is an intuition to me without being proved.
Dávid Natingga
CC BY-SA 3.0
2013-09-16T22:15:35.147Z
Please, note I know how to define the proof system outside of the theory and the language: just specify the deduction rules on the boolean formulas in certain syntactic form. Perhaps, I should ask a new question.
Dávid Natingga
CC BY-SA 3.0
2013-09-17T02:11:06.710Z
@Kaveh: I don't think so... $\top \lor \varphi$ where $\varphi$ has high K is easily seen to be a true statement, but to *derive* it, one must use the rules of the proof system to (essentially *syntactically*) derive $\top \lor \varphi$, which itself has high K. If this could be hard-coded into your proof system, it would have Kolmogorov complexity $O(1)$ - just the description of the proof system. This obviously cannot be true for infinitely many $\varphi$ of high K.
Joshua Grochow
CC BY-SA 3.0
2013-09-17T03:49:09.657Z
@Joshua, checking if something is a tautology doesn't need to imply that, here is how to hard-code it: if $\varphi$ is of the form $\top \lor ( ... )$ then the empty string is a proof of it. It has no implication on the K complexity of $(...)$.
Kaveh
<kolmogorov-complexity><proof-theory>
Is there an $\mathcal{L}$-theory and a formula $\phi$ for which Kolmogorov(proof($\phi$)) $<$ Kolmogorov($\phi$)?
Dávid Natingga
# Is there an $\mathcal{L}$-theory and a formula $\phi$ for which Kolmogorov(proof($\phi$)) $<$ Kolmogorov($\phi$)?

(Asked by: username_0 on 2013-09-15)

Are there a complete decidable $\mathcal{L}$-theory, a formula $\phi$ and a proof of $\phi$ for which the Kolmogorov complexity of the proof of $\phi$ is less than the Kolmogorov complexity of $\phi$?

Proofs in the proof systems I have seen so far are of the form:

1. *mathematical reasoning*
2. therefore $\phi$

Hence our intuition tells us that the Kolmogorov complexity of the proof has to be at least the Kolmogorov complexity of $\phi$. But this intuition does not prove any statement formally and it does not exclude the possibility of having a proof system where $p$ would be a proof of $\phi$ while Kolmogorov($p$) < Kolmogorov($\phi$) or even Kolmogorov(*mathematical reasoning* concatenate $\phi$) < Kolmogorov($\phi$).

**Tags:** kolmogorov-complexity, proof-theory

> **Comments:**
> **username_0**: I assume the existence of the proof system within the theory $\mathcal{L}$ given, however I do not claim any other properties about the proof system. $\phi$ has at least one proof since $\mathcal{L}$-theory is complete, it is allowed to have more proofs. The question asks if it is possible for some proof of some $\phi$ to have a lower Kolmogorov complexity than $\phi$.  
> **username_1**: Are you implying that the Kolmogorov complexity of a string is always more than or equal to the Kolmogorov complexity of its substrings? And what is the definition of a "proof system"? Do you mean something similar to Cook-Reckhow definition of a proof system or are you talking informally (in which case you should define what you mean by a proof system). Also as Ricky said, which proof of $\varphi$? Or do you mean every proof of $\varphi$?  
> **username_1**: It is easy to create proof systems where the Kolmogorov complexity of a proof of a formula is less than the Kolmogorov complexity the formula: just make the empty string be the proof of your true formula and hard code it in the proof system. Then the Kolmogorov complexity of the proof of the formula is $0$ while the formula can have arbitrary large Kolmogorov complexity.  
> **username_0**: How would I define such a proof system and a theory? Could you please provide a very simple example?  
> **username_2**: @username_1: I think if you ask for the statement for infinitely many $\varphi$ your trick no longer works.  
> **username_1**: @Joshua, I think we can even hard-code a family of tautologies with high Kolmogorov complexity, e.g. $\top \lor (\text{some high Kolmogorov complexity statement})$.  
> **username_1**: @David, you just hard code it, that is you simply define the empty string to be a proof of the statement.  
> **username_0**: @username_1 I know how to define a language and a theory, not how to define the proof system within the theory. If it is something simple, I would greatly appreciate an example with hardcoding. Otherwise, a satisfying answer to my question will have to be on hold until I learn more on proof theory. As of now your hardcoding argument is an intuition to me without being proved.  
> **username_0**: Please, note I know how to define the proof system outside of the theory and the language: just specify the deduction rules on the boolean formulas in certain syntactic form. Perhaps, I should ask a new question.  
> **username_2**: @username_1: I don't think so... $\top \lor \varphi$ where $\varphi$ has high K is easily seen to be a true statement, but to *derive* it, one must use the rules of the proof system to (essentially *syntactically*) derive $\top \lor \varphi$, which itself has high K. If this could be hard-coded into your proof system, it would have Kolmogorov complexity $O(1)$ - just the description of the proof system. This obviously cannot be true for infinitely many $\varphi$ of high K.  
> **username_1**: @Joshua, checking if something is a tautology doesn't need to imply that, here is how to hard-code it: if $\varphi$ is of the form $\top \lor ( ... )$ then the empty string is a proof of it. It has no implication on the K complexity of $(...)$.  

---

## 2 answers

### Answer by username_1 on 2013-09-17. Score: 1 | Accepted answer

As I mentioned in the comments, you need to first clarify what you exactly mean by a proof system.

Josh discusses the case where one uses the original definition of a proof system according to Cook-Reckhow.

There is an alternative definition which is also common: a proof system is a binary relation $R$ computable in polynomial time (and satisfying some conditions like soundness) and we say $\pi$ is an $R$-proof of $\varphi$ iff $R(\pi,\varphi)$.

With this definition it is easy to show that there can be a proof system where the K-complexity of a formula is much higher than the K-complexity of some proof of it.

E.g., let $R$ be some usual proof system modified as follows: we first check if $\varphi$ is of the form $\top \lor \psi$ for some formula $\psi$, if that is the case we accept the empty string as a proof of $\varphi$. Otherwise, we fall back to the original proof system.

Since $\psi$ can be any formula the K-complexity of $\varphi$ can be arbitrary high. However the K-compleixty of the empty string which is a proof of $\varphi$ is trivial.


---

### Answer by username_2 on 2013-09-17. Score: 2

In most "standard" proof systems, the formula $\varphi$ being proved is usually part of the proof itself by definition of the proof system, in which case for all $\varphi$, $K(\varphi) \leq K(\text{proof}) + O(1)$ (the extra constant is for the part of the program which says, basically, "extract the last line of the proof" - anyways, additive $O(1)$ errors are the best one can hope for in Kolmogorov complexity).

Even in a proof system where all that is required is that the formula $\varphi$ appear somewhere amongst the lines of the proof $\pi$, one can still get $K(\varphi) \leq K(\pi) + O(\log|\pi|)$, where here the extra $\log|\pi|$ bits are used to describe the index $i$ of the line of the proof that corresponds to $\varphi$.

In the much more general Cook-Reckhow style of proof system (or its computable analog) - that is, a polynomial-time computable function $f$ (resp., just a computable function $f$) whose range is exactly the set of true sentences of your theory - again, $K(\varphi) \leq K(\text{proof}) + O(1)$, where here the $O(1)$ extra bits describe the function $f$.

(Note that the trick of hard-coding certain tautologies into your proof system, pointed out by username_1, is handled by this latter case, as the hard-coded tautologies must be encoded directly into $f$, so they contribute to/are handled by the $O(1)$.)


---

