Question

I recall hearing about a result, or maybe a cluster of results, in some area of complexity theory, probably algebraic, to the effect that there are known, specific, short formulas whose minimal derivation is known to be exceedingly long. Or perhaps it is a specific function that requires an exceedingly deep curcuit. The "philosophy" seemed to be that such examples would threaten to make the older asymptotic question obsolete: "Who cares about asymptotics if the constants are huge." Can anyone, given these hints, describe ( and direct me to) the result I overheard?

Answer 1

Perhaps you were told about

Larry J. Stockmeyer, Albert R. Meyer: Cosmological lower bound on the circuit complexity of a small problem in logic. J. ACM 49(6): 753-784 (2002)

From the abstract: "An exponential lower bound on the circuit complexity of deciding the weak monadic second-order theory of one successor (WS1S) is proved. Circuits are built from binary operations, or 2-input gates, which compute arbitrary Boolean functions. In particular, to decide the truth of logical formulas of length at most 610 in this second-order language requires a circuit containing at least $10^{125}$ gates. So even if each gate were the size of a proton, the circuit would not fit in the known universe.

This demonstrates a specific function for which all inputs of size 610 cannot be determined within the physical universe. The proof is essentially a diagonalization argument, but is very carefully executed to take all constants into account.

(Note this is actually based on an asymptotic result, but it took some work to get a concrete lower bound out of it.)

Answer 2

The general fact surrounding some of the other answers is the following:

Every computably axiomatizable consistent theory $T$ containing trivial arithmetic admits very short theorems requiring extremely long proofs.

The basic fact is that there can be no total computable bound on the length of the proof required. To see this, suppose that there is a computable total function $f$ such that whenever statement $\psi$ is a statement of size at most $n$ provable from $T$, then there is a proof of size at most $f(n)$. In this case, the question of whether $T$ proves $\psi$ will be decidable, since we can simply inspect all proofs of length $f(n)$, where $n=|\psi|$ and check if any of them are proofs of $\psi$. But it is impossible that $T$ proves $\psi$ is decidable, since we could then produce a consistent completion of $T$, by the usual process of completing a theory, which is effective for decidable theories. This would produce a computable complete consistent theory of arithmetic, in contradiction to the incompleteness theorem.

One can make the conclusion fairly concrete via the halting problem. If $T$ is true and contains some trivial arithmetic, then $T$ will prove all true instances of the assertion program $p$ halts on input $m$, and prove no false instances. If there were a total computable function $f(p,m)$ such that whenever $p$ halted on input $m$, then there was a proof of this of length at most $f(p,m)$, then we could decide the halting problem: on input $(p,m)$, compute $f(p,m)$ and then look at all proofs of that length and determine if there is a proof of halting or not.

In conclusion:

Theorem. For any computably axiomatizable true theory $T$ and for any total computable function $f$, there is a program $p$ and input $m$ such that $T$ proves that $p$ halts on input $m$, but there is no proof of this in fewer than $f(p,m)$ steps.

Since as we all know, the computable functions can grow quite outrageously, this means that for any theory there will be short theorems that require extremely long proofs.

Answer 3

Are you by any chance referring to examples like Haken's proof that the pigeonhole principle requires exponentially long resolution proofs ?

Answer 4

This is a result due to Godel in his 1936 paper "Uber die Lange von Beweisen" (on the lengths of proofs), republished in English translation in volume 1 of his collected works. Roughly speaking, he shows that there are short theorems that have extremely long shortest proofs in certain formal systems, but much shorter proofs in more powerful systems. Harvey Friedman found some rather dramatic explicit examples, described by Smorynski in The varieties of arboreal experience

Answer 5

It's clear from the space and time hierarchy theorems in computational complexity, and more specifically non-deterministic time hierarchy theorems, that there are statements with extremely long proofs in any formal system that: (1) can describe Turing machines or cellular automata or similar; (2) can describe large numbers; and (3) has proofs that can be checked in a reasonable amount of time, such as polynomial time or even exponential time. The non-deterministic hierarchy theorem says that $\text{NTIME}(f(n)) \ne \text{NTIME}(g(n))$ if $f(n)$ and $g(n)$ are reasonably separated functions. A fairly precise version of this result is due to Cook, but if $f(n)$ and $g(n)$ are far enough apart, you can conclude that there is a separation just by comparison to deterministic time. The corollary then is that you can turn instances of such a slow computational problem into a claim which cannot have a short proof; if it did have a short proof, you could find it quickly to answer the computational question.

For example, for each fixed $n$, you can take a question of the form, "can the following unit squares with teeth and notches added tile a square of size $A(n)$, the Ackermann function?" The answer is always provably yes or provably no, because it is a finite question. You can use a diagonalization argument in the sense of complexity theory to show that sometimes the proof has an Ackermann-like length.

Actually Mike sent me his question by e-mail, but I didn't think of this answer then and suggested posting the question here. I don't know if this is the result sought, or merely a similar result. I also don't see a way to convincingly argue that asymptotic results are obsolete. It is true that because some computational problems are asymptotically slow, you can make a sequence of computational problems that are all asymptotically fast, but with a worse and worse constant factor.

Answer 6

Establishing that minimal proofs (or "derivations") of certain statements or theorems are long, is the prime target of the area called proof complexity. Concerning examples given in prior answers, like Haken's size lower bound on proofs of the pigeonhole principle, they deal with propositional logic only. Therefore, they are asymptotic results of the form: "there exists a constant $ 0<\epsilon<1 $ such that any resolution refutation of the propositional pigenohole principle $ PHP_n$ must be of length (i.e., number of steps) at least $ 2^{n^\epsilon}$"; Where $ PHP_n \;$, $ n=1,2,\ldots ,$ is an infinite family of propositional contradictions (expressing the $ n+ 1 $ to $ n\; $ pigeonhole principle). So propositional proof complexity does not seem to answer the question about non-asymptotic lower bounds.

On the other hand, lower bounds on first order proofs (having quantifiers, i.e., not propositional logic) are not necessarily asymptotic, and if this is what you are looking for, the only thorough survey I know of (dealing with both propositional and non-propositional) proof complexity is: Pavel Pudlak: The lengths of proofs, in Handbook of Proof Theory, S.R. Buss ed., Elsevier, 1998, pp.547-637, available here

(There is also an older book by Orevkov on non-propositional proof complexity: [1993] Complexity of Proofs and Their Transformations in Axiomatic theories, vol. 128 of Translations of Mathematical Monographs, American Mathematical Society, Providence, Rhode Island.)

Answer 7

I found a citation to this paper by Joel Spencer: "Short Theorems with Long Proofs" [Amer. Math. Monthly 90(6) 365-366 (1983)]. But I do not have access to it at the moment. Certainly seems relevant from the title!

Edit. But apparently, not according to michael's comment. The abstract of this paper by Marian Mrozek, "Inheritable Properties and Computer Assisted Proofs in Dynamics" says

Since there exist short theorems having arbitrarily long proofs (a consequence of G"odel's incompletness theorems, see [4, 6, 23]) ...

Reference [4] is Spencer's paper. So I guess this just confirms that this is common knowledge, without providing the explicit example you seek. Apologies for the distraction!