Incompleteness in the finite domain

TL;DR

This paper explores conjectures linking computational complexity to the difficulty of proving sentences, aiming to understand the relationship between proof complexity and computational hardness in finite domains.

Contribution

It formalizes and systematizes conjectures connecting complexity theory with proof difficulty, extending previous ideas and establishing new relationships.

Findings

Some conjectures relate high complexity to unprovability in weak theories.

New connections between conjectures and existing proof complexity statements.

Systematization of earlier and new conjectures in the context of finite domains.

Abstract

Motivated by the problem of finding finite versions of classical incompleteness theorems, we present some conjectures that go beyond ${\bf NP\neq co NP}$. These conjectures formally connect computational complexity with the difficulty of proving some sentences, which means that high computational complexity of a problem associated with a sentence implies that the sentence is not provable in a weak theory, or requires a long proof. Another reason for putting forward these conjectures is that some results in proof complexity seem to be special cases of such general statements and we want to formalize and fully understand these statements. In this paper we review some conjectures that we have presented earlier, introduce new conjectures, systematize them and prove new connections between them and some other statements studied before.