-
The strength of the dominance rule
Authors:
Leszek Aleksander Kołodziejczyk,
Neil Thapen
Abstract:
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]…
▽ More
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.
△ Less
Submitted 19 June, 2024;
originally announced June 2024.
-
An isomorphism theorem for models of Weak König's Lemma without primitive recursion
Authors:
Marta Fiori-Carones,
Leszek Aleksander Kołodziejczyk,
Tin Lok Wong,
Keita Yokoyama
Abstract:
We prove that if $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are countable models of the theory $\mathrm{WKL}^*_0$ such that $\mathrm{I}Σ_1(A)$ fails for some $A \in \mathcal{X} \cap \mathcal{Y}$, then $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are isomorphic. As a consequence, the analytic hierarchy collapses to $Δ^1_1$ provably in $\mathrm{WKL}^*_0 + \neg\mathrm{I}Σ^0_1$, and $\mathrm{WKL}$ is the stro…
▽ More
We prove that if $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are countable models of the theory $\mathrm{WKL}^*_0$ such that $\mathrm{I}Σ_1(A)$ fails for some $A \in \mathcal{X} \cap \mathcal{Y}$, then $(M,\mathcal{X})$ and $(M,\mathcal{Y})$ are isomorphic. As a consequence, the analytic hierarchy collapses to $Δ^1_1$ provably in $\mathrm{WKL}^*_0 + \neg\mathrm{I}Σ^0_1$, and $\mathrm{WKL}$ is the strongest $Π^1_2$ statement that is $Π^1_1$-conservative over $\mathrm{RCA}^*_0 + \neg\mathrm{I}Σ^0_1$.
Applying our results to the $Δ^0_n$-definable sets in models of $\mathrm{RCA}^*_0 + \mathrm{B}Σ^0_n + \neg\mathrm{I}Σ^0_n$ that also satisfy an appropriate relativization of Weak König's Lemma, we prove that for each $n \ge 1$, the set of $Π^1_2$ sentences that are $Π^1_1$-conservative over $\mathrm{RCA}^*_0 + \mathrm{B}Σ^0_n + \neg\mathrm{I}Σ^0_n$ is c.e. In contrast, we prove that the set of $Π^1_2$ sentences that are $Π^1_1$-conservative over $\mathrm{RCA}^*_0 + \mathrm{B}Σ^0_n$ is $Π_2$-complete. This answers a question of Towsner.
We also show that $\mathrm{RCA}_0 + \mathrm{RT}^2_2$ is $Π^1_1$-conservative over $\mathrm{B}Σ^0_2$ if and only if it is conservative over $\mathrm{B}Σ^0_2$ with respect to $\forall Π^0_5$ sentences.
△ Less
Submitted 27 August, 2022; v1 submitted 20 December, 2021;
originally announced December 2021.
-
Weaker cousins of Ramsey's theorem over a weak base theory
Authors:
Marta Fiori-Carones,
Leszek Aleksander Kołodziejczyk,
Katarzyna W. Kowalik
Abstract:
The paper is devoted to a reverse-mathematical study of some well-known consequences of Ramsey's theorem for pairs, focused on the chain-antichain principle $\mathsf{CAC}$, the ascending-descending sequence principle $\mathsf{ADS}$, and the Cohesive Ramsey Theorem for pairs $\mathsf{CRT}^2_2$. We study these principles over the base theory $\mathsf{RCA}^*_0$, which is weaker than the usual base th…
▽ More
The paper is devoted to a reverse-mathematical study of some well-known consequences of Ramsey's theorem for pairs, focused on the chain-antichain principle $\mathsf{CAC}$, the ascending-descending sequence principle $\mathsf{ADS}$, and the Cohesive Ramsey Theorem for pairs $\mathsf{CRT}^2_2$. We study these principles over the base theory $\mathsf{RCA}^*_0$, which is weaker than the usual base theory $\mathsf{RCA}_0$ considered in reverse mathematics in that it allows only $Δ^0_1$-induction as opposed to $Σ^0_1$-induction. In $\mathsf{RCA}^*_0$, it may happen that an unbounded subset of $\mathbb{N}$ is not in bijective correspondence with $\mathbb{N}$. Accordingly, Ramsey-theoretic principles split into at least two variants, "normal" and "long", depending on the sense in which the set witnessing the principle is required to be infinite.
We prove that the normal versions of our principles, like that of Ramsey's theorem for pairs and two colours, are equivalent to their relativizations to proper $Σ^0_1$-definable cuts. Because of this, they are all $Π^0_3$- but not $Π^1_1$-conservative over $\mathsf{RCA}^*_0$, and, in any model of $\mathsf{RCA}^*_0 + \neg \mathsf{RCA}_0$, if they are true then they are computably true relative to some set. The long versions exhibit one of two behaviours: they either imply $\mathsf{RCA}_0$ over $\mathsf{RCA}^*_0$ or are $Π^0_3$-conservative over $\mathsf{RCA}^*_0$. The conservation results are obtained using a variant of the so-called grou** principle.
We also show that the cohesion principle $\mathsf{COH}$, a strengthening of $\mathsf{CRT}^2_2$, is never computably true in a model of $\mathsf{RCA}^*_0$ and, as a consequence, does not follow from $\mathsf{RT}^2_2$ over $\mathsf{RCA}^*_0$.
△ Less
Submitted 24 May, 2021;
originally announced May 2021.
-
How strong is Ramsey's theorem if infinity can be weak?
Authors:
Leszek Aleksander Kołodziejczyk,
Katarzyna W. Kowalik,
Keita Yokoyama
Abstract:
We study the first-order consequences of Ramsey's Theorem for $k$-colourings of $n$-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 + \neg \mathrm{I}Σ^0_1$, $\mathrm{RT}^n_k$ is equivalent to its own relativization to any proper $Σ^0_1$-definable cut, so its…
▽ More
We study the first-order consequences of Ramsey's Theorem for $k$-colourings of $n$-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 + \neg \mathrm{I}Σ^0_1$, $\mathrm{RT}^n_k$ is equivalent to its own relativization to any proper $Σ^0_1$-definable cut, so its truth value remains unchanged in all extensions of the model with the same first-order universe.
We give an 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 PA whose $Π_3$ fragment is $\mathrm{B}Σ_1 + \exp$ and whose $Π_{\ell+3}$ fragment for $\ell \ge 1$ lies between $\mathrm{I}Σ_\ell \Rightarrow \mathrm{B}Σ_{\ell+1}$ and $\mathrm{B}Σ_{\ell+1}$. We also consider the first-order consequences of $\mathrm{RCA}^*_0 + \mathrm{RT}^2_k$. We show that they form a subtheory of $\mathrm{I}Σ_2$ whose $Π_3$ fragment is $\mathrm{B}Σ_1 + \exp$ and whose $Π_4$ fragment is strictly weaker than $\mathrm{B}Σ_2$ but not contained in $\mathrm{I}Σ_1$.
Additionally, we consider a principle $Δ^0_2$-$\mathrm{RT}^2_2$, defined like $\mathrm{RT}^2_2$ but with both the $2$-colourings and the solutions allowed to be $Δ^0_2$-sets. We show that the behaviour of $Δ^0_2$-$\mathrm{RT}^2_2$ over $\mathrm{RCA}_0 + \mathrm{B}Σ^0_2$ is similar to that of $\mathrm{RT}^2_2$ over $\mathrm{RCA}^*_0$, and that $\mathrm{RCA}_0 + \mathrm{B}Σ^0_2 + Δ^0_2$-$\mathrm{RT}^2_2$ is $Π_4$- but not $Π_5$-conservative over $\mathrm{B}Σ_2$. However, the statement we use to witness lack of $Π_5$-conservativity is not provable in $\mathrm{RCA}_0 +\mathrm{RT}^2_2$.
△ Less
Submitted 16 January, 2021; v1 submitted 4 November, 2020;
originally announced November 2020.
-
Ramsey's theorem for pairs, collection, and proof size
Authors:
Leszek Aleksander Kołodziejczyk,
Tin Lok Wong,
Keita Yokoyama
Abstract:
We prove that any proof of a $\forall Σ^0_2$ sentence in the theory $\mathrm{WKL}_0 + \mathrm{RT}^2_2$ can be translated into a proof in $\mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the proof in $\mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the other hand, $\mathrm{RT}^2_2$ has non-elementary speedup over the weaker base theory $\mathrm{RCA}^*_0$ for p…
▽ More
We prove that any proof of a $\forall Σ^0_2$ sentence in the theory $\mathrm{WKL}_0 + \mathrm{RT}^2_2$ can be translated into a proof in $\mathrm{RCA}_0$ at the cost of a polynomial increase in size. In fact, the proof in $\mathrm{RCA}_0$ can be found by a polynomial-time algorithm. On the other hand, $\mathrm{RT}^2_2$ has non-elementary speedup over the weaker base theory $\mathrm{RCA}^*_0$ for proofs of $Σ_1$ sentences.
We also show that for $n \ge 0$, proofs of $Π_{n+2}$ sentences in $\mathrm{B}Σ_{n+1}+\exp$ can be translated into proofs in $\mathrm{I}Σ_{n} + \exp$ at polynomial cost. Moreover, the $Π_{n+2}$-conservativity of $\mathrm{B}Σ_{n+1} + \exp$ over $\mathrm{I}Σ_{n} + \exp$ can be proved in $\mathrm{PV}$, a fragment of bounded arithmetic corresponding to polynomial-time computation. For $n \ge 1$, this answers a question of Clote, Hájek, and Paris.
△ Less
Submitted 16 January, 2021; v1 submitted 14 May, 2020;
originally announced May 2020.
-
Approximate counting and NP search problems
Authors:
Leszek Aleksander Kołodziejczyk,
Neil Thapen
Abstract:
We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory $\mathrm{APC}_2$ of [Jeřábek 2009]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational characterization of this class an…
▽ More
We study a new class of NP search problems, those which can be proved total using standard combinatorial reasoning based on approximate counting. Our model for this kind of reasoning is the bounded arithmetic theory $\mathrm{APC}_2$ of [Jeřábek 2009]. In particular, the Ramsey and weak pigeonhole search problems lie in the new class. We give a purely computational characterization of this class and show that, relative to an oracle, it does not contain the problem CPLS, a strengthening of PLS.
As CPLS is provably total in the theory $T^2_2$, this shows that $\mathrm{APC}_2$ does not prove every $\forall Σ^b_1$ sentence which is provable in bounded arithmetic. This answers the question posed in [Buss, Kołodziejczyk, Thapen 2014] and represents some progress in the programme of separating the levels of the bounded arithmetic hierarchy by low-complexity sentences.
Our main technical tool is an extension of the "fixing lemma" from [Pudlák, Thapen 2017], a form of switching lemma, which we use to show that a random partial oracle from a certain distribution will, with high probability, determine an entire computation of a $\textrm{P}^{\textrm{NP}}$ oracle machine. The introduction to the paper is intended to make the statements and context of the results accessible to someone unfamiliar with NP search problems or with bounded arithmetic.
△ Less
Submitted 26 November, 2021; v1 submitted 27 December, 2018;
originally announced December 2018.
-
Some upper bounds on ordinal-valued Ramsey numbers for colourings of pairs
Authors:
Leszek Aleksander Kołodziejczyk,
Keita Yokoyama
Abstract:
We study Ramsey's theorem for pairs and two colours in the context of the theory of $α$-large sets introduced by Ketonen and Solovay. We prove that any $2$-colouring of pairs from an $ω^{300n}$-large set admits an $ω^n$-large homogeneous set. We explain how a formalized version of this bound gives a more direct proof, and a strengthening, of the recent result of Patey and Yokoyama [Adv. Math. 330…
▽ More
We study Ramsey's theorem for pairs and two colours in the context of the theory of $α$-large sets introduced by Ketonen and Solovay. We prove that any $2$-colouring of pairs from an $ω^{300n}$-large set admits an $ω^n$-large homogeneous set. We explain how a formalized version of this bound gives a more direct proof, and a strengthening, of the recent result of Patey and Yokoyama [Adv. Math. 330 (2018), 1034--1070] stating that Ramsey's theorem for pairs and two colours is $\forallΣ^0_2$-conservative over the axiomatic theory $\mathsf{RCA}_0$ (recursive comprehension).
△ Less
Submitted 9 November, 2018; v1 submitted 2 July, 2018;
originally announced July 2018.
-
New bounds on the strength of some restrictions of Hindman's Theorem
Authors:
Lorenzo Carlucci,
Leszek Aleksander Kołodziejczyk,
Francesco Lepore,
Konrad Zdanowski
Abstract:
We prove upper and lower bounds on the effective content and logical strength for a variety of natural restrictions of Hindman's Finite Sums Theorem. For example, we show that Hindman's Theorem for sums of length at most 2 and 4 colors implies $\mathsf{ACA}_0$. An emerging {\em leitmotiv} is that the known lower bounds for Hindman's Theorem and for its restriction to sums of at most 2 elements are…
▽ More
We prove upper and lower bounds on the effective content and logical strength for a variety of natural restrictions of Hindman's Finite Sums Theorem. For example, we show that Hindman's Theorem for sums of length at most 2 and 4 colors implies $\mathsf{ACA}_0$. An emerging {\em leitmotiv} is that the known lower bounds for Hindman's Theorem and for its restriction to sums of at most 2 elements are already valid for a number of restricted versions which have simple proofs and better computability- and proof-theoretic upper bounds than the known upper bound for the full version of the theorem. We highlight the role of a sparsity-like condition on the solution set, which we call apartness.
△ Less
Submitted 15 November, 2017; v1 submitted 21 January, 2017;
originally announced January 2017.
-
How unprovable is Rabin's decidability theorem?
Authors:
Leszek Aleksander Kołodziejczyk,
Henryk Michalewski
Abstract:
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 the complementation theorem for tree automata, which forms the technical core of typical proofs of Rabin's theorem, is equivalent over the moderately strong second-order arithmetic theory $\mathsf{ACA}_0$ to a determinacy principle impl…
▽ More
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 the complementation theorem for tree automata, which forms the technical core of typical proofs of Rabin's theorem, is equivalent over the moderately strong second-order arithmetic theory $\mathsf{ACA}_0$ to a determinacy principle implied by the positional determinacy of all parity games and implying the determinacy of all Gale-Stewart games given by boolean combinations of ${\bf Σ^0_2}$ sets. It follows that complementation for tree automata is provable from $Π^1_3$- but not $Δ^1_3$-comprehension.
We then use results due to MedSalem-Tanaka, Möllerfeld and Heinatsch-Möllerfeld to prove that over $Π^1_2$-comprehension, the complementation theorem for tree automata, decidability of the MSO theory of the infinite binary tree, positional determinacy of parity games and determinacy of $\mathrm{Bool}({\bf Σ^0_2})$ Gale-Stewart games are all equivalent. Moreover, these statements are equivalent to the $Π^1_3$-reflection principle for $Π^1_2$-comprehension. It follows in particular that Rabin's decidability theorem is not provable in $Δ^1_3$-comprehension.
△ Less
Submitted 27 August, 2015;
originally announced August 2015.
-
End-extensions of models of weak arithmetic from complexity-theoretic containments
Authors:
Leszek Aleksander Kołodziejczyk
Abstract:
We prove that if the linear-time and polynomial-time hierarchies coincide, then every model of $Π_1(\mathbb{N}) + \neg Ω_1$ has a proper end-extension to a model of $Π_1(\mathbb{N})$, and so $Π_1(\mathbb{N}) + \neg Ω_1 \vdash \mathrm{B}Σ_1$. Under an even stronger complexity-theoretic assumption which nevertheless seems hard to disprove using present-day methods,…
▽ More
We prove that if the linear-time and polynomial-time hierarchies coincide, then every model of $Π_1(\mathbb{N}) + \neg Ω_1$ has a proper end-extension to a model of $Π_1(\mathbb{N})$, and so $Π_1(\mathbb{N}) + \neg Ω_1 \vdash \mathrm{B}Σ_1$. Under an even stronger complexity-theoretic assumption which nevertheless seems hard to disprove using present-day methods, $Π_1(\mathbb{N}) + \neg \mathrm{Exp} \vdash \mathrm{B}Σ_1$. Both assumptions can be modified to versions which make it possible to replace $Π_1(\mathbb{N})$ by $\mathrm{I}Δ_0$ as the base theory.
We also show that any proof that $\mathrm{I}Δ_0 + \neg \exp$ does not prove a given finite fragment of $\mathrm{B}Σ_1$ has to be "non-relativizing", in the sense that it will not work in the presence of an arbitrary oracle.
△ Less
Submitted 25 November, 2014;
originally announced November 2014.
-
Categorical characterizations of the natural numbers require primitive recursion
Authors:
Leszek Aleksander Kołodziejczyk,
Keita Yokoyama
Abstract:
Simpson and the second author asked whether there exists a characterization of the natural numbers by a second-order sentence which is provably categorical in the theory RCA$^*_0$. We answer in the negative, showing that for any characterization of the natural numbers which is provably true in WKL$^*_0$, the categoricity theorem implies $Σ^0_1$ induction. On the other hand, we show that RCA$^*_0$…
▽ More
Simpson and the second author asked whether there exists a characterization of the natural numbers by a second-order sentence which is provably categorical in the theory RCA$^*_0$. We answer in the negative, showing that for any characterization of the natural numbers which is provably true in WKL$^*_0$, the categoricity theorem implies $Σ^0_1$ induction. On the other hand, we show that RCA$^*_0$ does make it possible to characterize the natural numbers categorically by means of a set of second-order sentences. We also show that a certain $Π^1_2$-conservative extension of RCA$^*_0$ admits a provably categorical single-sentence characterization of the naturals, but each such characterization has to be inconsistent with WKL$^*_0$+superexp.
△ Less
Submitted 15 October, 2014; v1 submitted 14 October, 2014;
originally announced October 2014.
-
Small Stone in Pool
Authors:
Samuel R. Buss,
Leszek Aleksander Kolodziejczyk
Abstract:
The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polynomial size proofs in both pool resolution and the proof system of regular tree-like resolution with input lemmas (regRTI). Therefore, the Stone tautologies do not separate resolution from DPLL with clause learning.
The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polynomial size proofs in both pool resolution and the proof system of regular tree-like resolution with input lemmas (regRTI). Therefore, the Stone tautologies do not separate resolution from DPLL with clause learning.
△ Less
Submitted 26 June, 2014; v1 submitted 21 May, 2014;
originally announced May 2014.
