# Is there an $\mathcal{L}$-theory and a formula $\phi$ for which Kolmogorov(proof($\phi$)) $<$ Kolmogorov($\phi$)?

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$).

• What do you mean by "the proof of $\phi$"? $\:$ Are you assuming the proof system $\hspace{1.53 in}$ and $\phi$ are such that $\phi$ has exactly one proof? $\;\;\;$ – user6973 Sep 16 '13 at 0:19
• 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 Sep 16 '13 at 1:21
• "formula $\phi$ for which" $\:\mapsto\:$ "formula $\phi$ and a proof of $\phi$ for which" $\;\;\;$ – user6973 Sep 16 '13 at 1:24
• 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 Sep 16 '13 at 4:14
• 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 Sep 16 '13 at 4:20

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.

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 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)$.)