We define the notion of a combinatorics of a first order structure, and a relation of covering between first order structures and propositional proof systems. Namely, a first order structure M combinatorially satisfies an L-sentence Φ iff Φ holds in all L-structures definable in M. The combinatorics Comb(M) of M is the set of all sentences combinatorially satisfied in M. Structure M covers a propositional proof system P iff M combinatorially satisfies all Φ for which the associated sequence of propositional formulas <Φ>_n, encoding that Φ holds in L-structures of size n, have polynomial size P-proofs. That is, Comb(M) contains all Φ feasibly verifiable in P. Finding M that covers P but does not combinatorially satisfy Φ thus gives a super polynomial lower bound for the size of P-proofs of <Φ>_n. We show that any proof system admits a class of structures covering it; these structures are expansions of models of bounded arithmetic. We also give, using structures covering proof systems R*(log) and PC, new lower bounds for these systems that are not apparently amenable to other known methods. We define new type of propositional proof systems based on a combinatorics of (a class of) structures.
展开▼
