Combinatorics of first order structures and propositional proof systems (Q701740)

The author continues his work of giving bounds of proof complexity by means of model theory. In this paper, he defines the combinatorics of a first-order structure \(M\), \(\text{Comb}(M)\), and the notion of `\(M\) covers a propositional proof system \(P\)'. Using these, he obtains results that are not amenable to other methods. Namely, the proofs of propositional statements, \(\varphi_0,\varphi_1,\dots, \varphi_k,\dots\) require superpolynomial (in \(k\)) size in each of the systems: resolution \([R^*(\log)]\), Nullstellensatz proof system, and polynomial calculus, where \(\varphi_0,\varphi_1,\dots\) are associated with familiar statements in field theory (like `a finite field cannot be ordered'). The general metatheorem, on which these results are based, relates the existence of an infinite counter-model of the given predicate statement to superpolynomial size of proofs of the associated \(\langle\varphi_k\rangle\). The author also shows how to construct structures that cover the given proof system, on the basis of bounded arithmetic, and conversely (so to speak) how to construct a proof system starting from structures. Some conditions must be met for the construction to work, of course; and a number of results are obtained. For instance, if \(P\) contains a Frege system then any structure constructed covers \(P\), and the system polynomially simulates \(R^*(\log)\) if it is obtained from a class \(C\) of infinite structures such that \(\text{Comb}(C)\) is r.e.