Computational complexity theoretic incompleteness: is that a thing?

Question

Has anyone done research in an area that I have not heard of but that I want to call "Computational complexity theoretic incompleteness", which would mean not absolute incompleteness in the sense that Godel made famous, but in the practical sense of the physical time/space constraints of computers. For example, instead of Godel's self-referential statement $\phi$ which has the property that there can be neither a proof of $\phi$ nor of $\neg \phi$ in PA, this would be a weaker form of incompleteness. There may very well be a proof of $\phi$ in PA, but one can prove that such a proof would have a length (i.e., time complexity) of at least $2 \uparrow \uparrow \uparrow 1000*n$, where $\phi$ is somehow parameterized by n. Does this field already exist?

Answer 1

Yes, this sort of thing has been considered before, for example by Harvey Friedman and Pavel Pudlák. Here is a representative result. If we let $\mathsf{Con}(\mathsf{PA},n)$ denote the statement that there is no $\mathsf{PA}$ proof of a contradiction of length less than $n$, then we can ask for the length of the shortest $\mathsf{PA}$ proof of $\mathsf{Con}(\mathsf{PA},n)$. Friedman has proved an $n^\epsilon$ lower bound on this length (for some $\epsilon>0$), and Pudlák has proved a polynomial upper bound. Perhaps more interesting is the question of the length of the shortest proof of $\mathsf{Con}(\mathsf{PA},n)$ in some weaker system such as $\mathsf{PRA}$. Conjecturally (this is related to various standard conjectures in computational complexity theory), the shortest such proof is superpolynomially long. If this is true, then one philosophical interpretation is that we cannot convince an "ultrafinitist" that it is futile to search for a (short) contradiction in $\mathsf{PA}$, because any futility proof that the ultrafinitist would accept is too long for us to exhibit.

For more on this topic, see for example Pudlák's paper, Incompleteness in the finite domain.

Answer 2

Consider the sentence $P(n)$ which says "This sentence has no proof shorter than $n$ characters." This sentence is true, and even has a proof - enumerate all strings of length $n$ and check them one by one.

You can replace the mention of $n$ by any computable function of $n$ that you like. (Of course, this will add a constant to the length of $P(n)$.) This kind of diagonalisation is why the time and space hierarchies do not collapse.

---

As mentioned in the comments above, this idea is due to Gödel and appears in his speed-up theorem. The sentence I suggest, $P(n)$, is a resource-limited version of the first incompleteness theorem. The sentence Timothy Chow suggests, $\mathsf{Con}(\mathsf{PA},n)$, is a resource-limited version of the second.

Answer 3

These self-referential decision problems are already part of the subject of computational complexity. There are analogues of the halting problem, for example, for many of the various classes in the complexity zoo, which are thereby shown not to be solvable at that level. This is a fundamental tool already implemented throughout the subject.

Answer 4

This might be more of an analogy, but major complexity conjectures like P=NP could be considered related.

Background: a common "complete" problem for a specified time limit is: given a Turing machine, does it accept a given input within the time limit? This is analogous to: given a statement, does it have a proof of a given length? In general, we cannot solve this problem faster than the time limit, i.e. by actually running the Turing machine and checking. This gives time hierarchy theorems, as others mentioned.

So incompleteness feels close to the claim "you cannot in general discover what a TM would do faster than running it." Complexity conjectures are often of this flavor and "feel true" for this reason, but have specific conditions that disallow the standard argument.

Example 1: The NP-complete problem is: given a Turing machine, input, and polynomial time limit, does there exist an auxiliary input that makes it accept in time? It seems "obvious by incompleteness" that this cannot be solved except by trying the Turing machine on all possible auxiliary inputs for a polynomial length of time each, hence an exponential total runtime. But if you can prove it, that's $\mathsf{P} \neq \mathsf{NP}$.

Example 2: A PPAD-complete problem is: given a special type of exponentially-large graph whose neighbor relation is computed by a given polynomial-time Turing machine, and given a source vertex, find a sink vertex. It seems "obvious by incompleteness" that this cannot be solved except by trying the Turing machine on all possible vertices (or along a naive exponential-length path), hence an exponential total runtime. But if you can prove it, that's $\mathsf{PPAD} \subsetneq FP$.