Combinatorics of first order structures and propositional proof systems (Q701740): Difference between revisions
From MaRDI portal
Created a new Item |
Set OpenAlex properties. |
||
(2 intermediate revisions by 2 users not shown) | |||
Property / MaRDI profile type | |||
Property / MaRDI profile type: MaRDI publication profile / rank | |||
Normal rank | |||
Property / full work available at URL | |||
Property / full work available at URL: https://doi.org/10.1007/s00153-003-0186-y / rank | |||
Normal rank | |||
Property / OpenAlex ID | |||
Property / OpenAlex ID: W1552145226 / rank | |||
Normal rank | |||
links / mardi / name | links / mardi / name | ||
Latest revision as of 00:33, 20 March 2024
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Combinatorics of first order structures and propositional proof systems |
scientific article |
Statements
Combinatorics of first order structures and propositional proof systems (English)
0 references
16 December 2004
0 references
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.
0 references
complexity of proofs
0 references
model-theoretic method
0 references