It has become standard that, when a SAT solver decides that a CNF $Γ$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $Γ$ in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) -- for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al.~2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system $G_1$, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER.

Abstract We study the first-order consequences of Ramsey’s Theorem fork-colourings ofn-tuples, for fixed $n, k \ge 2$ , over the relatively weak second-order arithmetic theory $\mathrm {RCA}^*_0$ . Using the Chong–Mourad coding lemma, we show that in a model of $\mathrm {RCA}^*_0$ that does not satisfy $\Sigma ^0_1$ induction, $\mathrm {RT}^n_k$ is equivalent to its relativization to any proper $\Sigma ^0_1$ -definable cut, so its truth value remains unchanged in all extensions of the model with the same first-order universe. We give a complete axiomatization of the first-order consequences of $\mathrm {RCA}^*_0 + \mathrm {RT}^n_k$ for $n \ge 3$ . We show that they form a non-finitely axiomatizable subtheory of $\mathrm {PA}$ whose $\Pi _3$ fragment coincides with $\mathrm {B} \Sigma _1 + \exp $ and whose $\Pi _{\ell +3}$ fragment for $\ell \ge 1$ lies between $\mathrm {I} \Sigma _\ell \Rightarrow \mathrm {B} \Sigma _{\ell +1}$ and $\mathrm {B} \Sigma _{\ell +1}$ . We also give a complete axiomatization of the first-order consequences of $\mathrm {RCA}^*_0 + \mathrm {RT}^2_k + \neg \mathrm {I} \Sigma _1$ . In general, we show that the first-order consequences of $\mathrm {RCA}^*_0 + \mathrm {RT}^2_k$ form a subtheory of $\mathrm {I} \Sigma _2$ whose $\Pi _3$ fragment coincides with $\mathrm {B} \Sigma _1 + \exp $ and whose $\Pi _4$ fragment is strictly weaker than $\mathrm {B} \Sigma _2$ but not contained in $\mathrm {I} \Sigma _1$ . Additionally, we consider a principle $\Delta ^0_2$ - $\mathrm {RT}^2_2$ which is defined like $\mathrm {RT}^2_2$ but with both the $2$ -colourings and the solutions allowed to be $\Delta ^0_2$ -sets rather than just sets. We show that the behaviour of $\Delta ^0_2$ - $\mathrm {RT}^2_2$ over $\mathrm {RCA}_0 + \mathrm {B}\Sigma ^0_2$ is in many ways analogous to that of $\mathrm {RT}^2_2$ over $\mathrm {RCA}^*_0$ , and that

We show that if a k-CNF requires width w to refute in resolution, then it requires space square root of √ω to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is the first analogue, in polynomial calculus, of Atserias and Dalmau's result lower-bounding clause space in resolution by resolution width. As a by-product of our new approach to space lower bounds we give a simple proof of Bonacina's recent result that total space in resolution (the total number of variable occurrences that must be kept in memory) is lower-bounded by the width squared. As corollaries of the main result we obtain some new lower bounds on the PCR space needed to refute specific formulas, as well as partial answers to some open problems about relations between space, size, and degree for polynomial calculus.

We study the strength of axioms needed to prove various results related to automata on infinite words and B\"uchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$: (1) the induction scheme for $\Sigma^0_2$ formulae of arithmetic, (2) a variant of Ramsey's Theorem for pairs restricted to so-called additive colourings, (3) B\"uchi's complementation theorem for nondeterministic automata on infinite words, (4) the decidability of the depth-$n$ fragment of the MSO theory of $(N, {\le})$, for each $n \ge 5$. Moreover, each of (1)-(4) implies McNaughton's determinisation theorem for automata on infinite words, as well as the "bounded-width" version of K\"onig's Lemma, often used in proofs of McNaughton's theorem.

We consider three relatively strong families of subsystems of AC 0 [2]-Frege proof systems, i.e., propositional proof systems using constant-depth formulas with an additional parity connective, for which exponential lower bounds on proof size are known. In order of increasing strength, the subsystems are (i) constant-depth proof systems with parity axioms and the (ii) treelike and (iii) daglike versions of systems introduced by Krajíček which we call PK c d (⊕). In a PK c d (⊕)-proof, lines are disjunctions (cedents) in which all disjuncts have depth at most d , parities can only appear as the outermost connectives of disjuncts, and all but c disjuncts contain no parity connective at all. We prove that treelike PK O (1) O (1) (⊕) is quasipolynomially but not polynomially equivalent to constant-depth systems with parity axioms. We also verify that the technique for separating parity axioms from parity connectives due to Impagliazzo and Segerlind can be adapted to give a superpolynomial separation between daglike PK O (1) O (1) (⊕) and AC 0 [2]-Frege; the technique is inherently unable to prove superquasipolynomial separations. We also study proof systems related to the system Res-Lin introduced by Itsykson and Sokolov. We prove that an extension of treelike Res-Lin is polynomially simulated by a system related to daglike PK O(1) O(1) (⊕), and obtain an exponential lower bound for this system.

We study the strength of set-theoretic axioms needed to prove Rabin's theorem on the decidability of the MSO theory of the infinite binary tree. We first show that over the second-order arithmetic theory ACA0, the complementation theorem for nondeterministic tree automata is equivalent to a statement expressing the determinacy of all Gale-Stewart games given by Bool(∑02) sets. It follows that the complementation theorem is provable from Π13- but not Δ13-comprehension.

Abstract We prove that if the linear-time and polynomial-time hierarchies coincide, then every model of Π1(ℕ) + ¬Ω1has a proper end-extension to a model of Π1(ℕ), and so Π1(ℕ) + ¬Ω ⊢ BΣ1. Under an even stronger complexity-theoretic assumption which nevertheless seems hard to disprove using present-day methods, Π1(ℕ) + ¬Exp ⊢ BΣ1. Both assumptions can be modified to versions which make it possible to replace Π1(ℕ) by IΔ0as the base theory. We also show that any proof that IΔ0+ ¬Exp does not prove a given finite fragment of BΣ1has to be “nonrelativizing”, in the sense that it will not work in the presence of an arbitrary oracle.

Abstract We study the long-standing open problem of giving $\forall {\rm{\Sigma }}_1^b$ separations for fragments of bounded arithmetic in the relativized setting. Rather than considering the usual fragments defined by the amount of induction they allow, we study Jeřábek’s theories for approximate counting and their subtheories. We show that the $\forall {\rm{\Sigma }}_1^b$ Herbrandized ordering principle is unprovable in a fragment of bounded arithmetic that includes the injective weak pigeonhole principle for polynomial time functions, and also in a fragment that includes the surjective weak pigeonhole principle for FPNPfunctions. We further give new propositional translations, in terms of random resolution refutations, for the consequences of $T_2^1$ augmented with the surjective weak pigeonhole principle for polynomial time functions.

Abstract We prove that: • if there is a model of IΔ0 + ¬exp with cofinal Σ1-definable elements and a Σ1 truth definition for Σ1 sentences, then IΔ0 + ¬exp + ¬BΣ1 is consistent, • there is a model of IΔ0 + Ω1 + ¬exp with cofinal Σ1-definable elements, both a Σ2 and a Π2 truth definition for Σ1 sentences, and for each n ≥ 2, a Σn truth definition for Σn sentences. The latter result is obtained by constructing a model with a recursive truth-preserving translation of Σ1 sentences into boolean combinations of sentences. We also present an old but previously unpublished proof of the consistency of IΔ0 + ¬exp + ¬BΣ1 under the assumption that the size parameter in Lessan's Δ0 universal formula is optimal. We then discuss a possible reason why proving the consistency of IΔ0 + ¬exp + ¬BΣ1 unconditionally has turned out to be so difficult.

The task of XML data exchange is to restructure a document conforming to a source schema under a target schema according to certain mapping rules. The rules are typically expressed as source-to-target dependencies using various kinds of patterns, involving horizontal and vertical navigation, as well as data comparisons. The target schema imposes complex conditions on the structure of solutions, possibly inconsistent with the mapping rules. In consequence, for some source documents there may be no solutions.We investigate three problems: deciding if all documents of the source schema can be mapped to a document of the target schema (absolute consistency), deciding if a given document of the source schema can be mapped (solution existence), and constructing a solution for a given source document (solution building).We show that the complexity of absolute consistency is rather high in general, but within the polynomial hierarchy for bounded depth schemas. The combined complexity of solution existence and solution building behaves similarly, but the data complexity turns out to be very low.In addition to this we show that even for much more expressive mapping rules, based on MSO definable queries, absolute consistency is decidable and data complexity of solution existence is polynomial.

Abstract We show, under the assumption that factoring is hard, that a model of PV exists in which the polynomial hierarchy does not collapse to the linear hierarchy; that a model of exists in which NP is not in the second level of the linear hierarchy; and that a model of exists in which the polynomial hierarchy collapses to the linear hierarchy. Our methods are model-theoretic. We use the assumption about factoring to get a model in which the weak pigeonhole principle fails in a certain way, and then work with this failure to obtain our results. As a corollary of one of the proofs, we also show that in the failure of WPHP (for definable relations) implies that the strict version of PH does not collapse to a finite level.

Abstract Modifying the methods of Z. Adamowicz's paperHerbrand consistency and bounded arithmetic[3] we show that there exists a numbernsuch that ⋃mSm(the union of the bounded arithmetic theoriesSm) does not prove the Herbrand consistency of the finitely axiomatizable theory S3n

Abstract The paper discusses the notion of finite model truth definitions (or FM-truth definitions), introduced by M. Mostowski as a finite model analogue of Tarski's classical notion of truth definition. We compare FM-truth definitions with Vardi's concept of the combined complexity of logics, noting an important difference: the difficulty of defining FM-truth for a logic does not depend on the syntax of , as long as it is decidable. It follows that for a natural there exist FM-truth definitions whose evaluation is much easier than the combined complexly of would suggest. We apply the general theory to give a complexity-theoretical characterization of the logics for which the classes (prenex classes of higher order logics) define FM-truth. For any d ≥ 2, m ≥ 1 we construct a family of syntactically defined fragments of which satisfy this characterization. We also use the classes to give a refinement of known results on the complexity classes captured by . We close with a few simple corollaries, one of which gives a sufficient condition for the existence, given a vocabulary σ, of a fixed number k such that model checking for all first order sentences over σ can be done in deterministic time nk.

Abstract. We use finite model theory (in particular, the method of FM-truth definitions, introduced in [MM01] and developed in [K04], and a normal form result akin to those of [Ste93] and [G97]) to prove: Let m ≥ 2. Then: (A) If there exists k such that NP⊆ Σm TIME(nk)∩ Πm TIME(nk), then for every r there exists kr such that : (B) If there exists a superpolynomial time-constructible function f such that NTIME(f) , then additionally . This strengthens a result by Mocas [M96] that for any r, . In addition, we use FM-truth definitions to give a simple sufficient condition for the arity hierarchy to be strict over finite models.