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?



Computational complexity theoretic incompleteness: is that a thing?
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](https://arxiv.org/abs/1601.01487v2).


