Source author record

Leszek Aleksander Kołodziejczyk

Explore this author’s publications, collaborators and research topics. This catalog record has not been claimed by its author.

ResearcherUnclaimed source record

math.LO Formal Languages and Automata Theory Logic in Computer Science math.CO

Catalog footprint

Research overview

7works

4topics

4close collaborators

Actions

Is this your work?

Open graph Browse papers

preprint2022arXiv

An isomorphism theorem for models of Weak König's Lemma without primitive recursion

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.

preprint2021arXiv

How strong is Ramsey's theorem if infinity can be weak?

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$ .

preprint2021arXiv

Ramsey's theorem for pairs, collection, and proof size

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.

preprint2017arXiv

New bounds on the strength of some restrictions of Hindman's Theorem

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.

preprint2015arXiv

How unprovable is Rabin's decidability theorem?

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.

preprint2014arXiv

Categorical characterizations of the natural numbers require primitive recursion

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.

preprint2014arXiv

End-extensions of models of weak arithmetic from complexity-theoretic containments

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.

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.