Combinatorics of first order structures and propositional proof systems
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.
- A logical approach to asymptotic combinatorics I. First order properties
- The Andrews-Curtis conjecture, term rewriting and first-order proofs
- Tight size-degree bounds for sums-of-squares proofs
- The treewidth of proofs
- Partially definable forcing and bounded arithmetic
- A transformation scheme for infinitary first-order combinatorics presenting computational level of expressiveness in predicate logic
- scientific article; zbMATH DE number 1688382 (Why is no real title available?)
- Relativization makes contradictions harder for resolution
- scientific article; zbMATH DE number 1907992 (Why is no real title available?)
- Expansions of pseudoinfinite structures and circuit and proof complexity
- Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
- A note on propositional proof complexity of some Ramsey-type statements
This page was built for publication: Combinatorics of first order structures and propositional proof systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q701740)
