## Forthcoming

- With Marta Fiori-Carones, Leszek Kołodziejczyk and Keita Yokoyama. An isomorphism theorem for models of Weak König’s Lemma without primitive recursion. Preprint, 28 pp., December 2021.
- In this paper, we prove that every countable model of BΣ
^{0}_{1}+ exp + ¬IΣ^{0}_{1}has a unique countable ω-extension satisfying WKL_{0}^{*}up to isomorphism. The paper also contains a number of interesting consequences of this theorem, including a quantifier elimination result for WKL_{0}^{*}+ ¬IΣ^{0}_{1}almost down to the arithmetical level, an upper bound on the complexity of Π^{1}_{1}conservativity over BΣ^{0}_{n+1}+ exp + ¬IΣ^{0}_{n+1}, a reduction of the open question whether RT^{2}_{2}is Π^{1}_{1}-conservative over BΣ^{0}_{2}down to the ∀Σ^{0}_{4}level, and more. - This preprint can be downloaded by following this link to the arXiv.

- In this paper, we prove that every countable model of BΣ
- With Stephen G. Simpson. Model-theoretic characterizations of ATR
_{0}and Π^{1}_{1}-CA_{0}. Preprint, 27 pp., December 2018.- This paper contains several characterizations of countable models of ATR
_{0}and Π^{1}_{1}-CA_{0}in terms of their conservative end extensions. - This preprint is available here in pdf.

- This paper contains several characterizations of countable models of ATR

## Published

- With Leszek Kołodziejczyk and Keita Yokoyama. Ramsey’s theorem for pairs, collection, and proof size. Journal of Mathematical Logic 24:2 (2024), 2350007.
- This paper contains polynomial-time algorithms that transform
- any proof in WKL
_{0}+ RT^{2}_{2}of a ∀Σ^{0}_{2}sentence into a proof of the same sentence in RCA_{0}; and - any proof in BΣ
_{n+1}+ exp of a Π_{n+2}sentence into a proof of the same sentence in IΣ_{n}+ exp, for any`n`∈ℕ.

In contrast, this paper also gives Σ

_{1}sentences provable in RCA_{0}^{*}of which all proofs in RCA_{0}^{*}must be superexponentially longer than their shortest proofs in RCA_{0}^{*}+ RT^{2}_{2}. - any proof in WKL
- A preprint version can be downloaded by following this link to the arXiv.

- This paper contains polynomial-time algorithms that transform
- With David Belanger, C.T. Chong, Wei Wang, and Yue Yang. Where pigeonhole principles meet König lemmas. Transactions of the American Mathematical Society 374:11 (2021), pp. 8275–8303.
- This paper studies the pigeonhole principle for Σ
_{2}-definable injections whose domain is twice as large as the codomain, and the weak König lemma for Δ^{0}_{2}-definable trees in which every level has at least half of the possible nodes. We show that the latter implies the existence of 2-random reals, and is conservative over the former. We also show that the former is strictly weaker than the usual pigeonhole principle for Σ_{2}-definable injections. - A preprint version is available here in pdf.

- This paper studies the pigeonhole principle for Σ
- On Wilkie and Paris’s notion of fullness. Fundamenta Mathematicae 245 (2019), pp. 79–100.
- In their comprehensive study of the End-Extension Question, Wilkie and Paris devised a special notion of saturation called
*fullness*for models of arithmetic (Logic, Methodology and Philosophy of Science VIII, North-Holland Publishing Company, Amsterdam, 1989, pp. 143–161). In this paper, we take a closer look at their notion of fullness and refine some results in the original Wilkie–Paris paper. In particular, we characterize fullness in terms of the existence of recursively saturated end extensions. From this we see that every countable IΔ_{0}-full model of IΔ_{0}+BΣ_{1}is (IΔ_{0}+BΣ_{1})-full. - A preprint version is available here in pdf.

- In their comprehensive study of the End-Extension Question, Wilkie and Paris devised a special notion of saturation called
- With Stefan Hetzl. Some observations on the logical foundations of induction theorem proving. Logical Methods in Computer Science 13:4 (2017).
- We study the logical foundations of automated inductive theorem proving. Towards this aim, we first develop a theoretical model that is centred around the difficulty in finding induction axioms to prove a goal. Based on this model, we then analyze the following aspects: the choice of a proof shape, the choice of an induction rule, and the language of the induction formula. In particular, using simple model-theoretic techniques, we clarify the relationship between notions of inductiveness that have been considered in the literature on automated inductive theorem proving.
- This paper is published with open access. It can be downloaded free-of-charge by following this link.

- Models of the Weak König Lemma. Annals of the Japan Association for Philosophy of Science 25 (2017), pp. 25–34.
- This paper surveys the model-theoretic aspects of two topics initiated by Kazuyuki Tanaka related to the Weak König Lemma: self-embedding, and conservativity for sentences of the form
`∀X ∃!Y θ(X,Y)`, where`θ(X,Y)`is an arithmetical formula. It includes a few recent developments and proof sketches. - It can be downloaded free-of-charge by following this link to the journal website.
**Note**: the proof of Theorem 3.2 sketched in the paper apparently contains a gap, but it should be fixable.

- This paper surveys the model-theoretic aspects of two topics initiated by Kazuyuki Tanaka related to the Weak König Lemma: self-embedding, and conservativity for sentences of the form
- With Ali Enayat. Unifying the model theory of first-order and second-order arithmetic via WKL
_{0}^{*}. Annals of Pure and Applied Logic 168:6 (2017), pp. 1247–1283. Formerly known as Model theory of WKL_{0}^{*}.- We develop machinery to make the Arithmetized Completeness Theorem more effective in the study of many models of IΔ
_{0}+BΣ_{1}+exp, including all countable ones, by passing on to the conservative extension WKL_{0}^{*}of IΔ_{0}+BΣ_{1}+exp. Our detailed study of the model theory of WKL_{0}^{*}leads to the simplification and improvement of many results in the model theory of Peano arithmetic and its fragments about end extensions and initial segments. - A preprint version and a list of errata are available here in pdf.

- We develop machinery to make the Arithmetized Completeness Theorem more effective in the study of many models of IΔ
- With Sy David Friedman and Wei Li. Fragments of Kripke–Platek set theory and the metamathematics of α-recursion theory. Archive for Mathematical Logic 55:7 (2016), pp. 899–924.
- Versions of the Friedberg–Muchnik Theorem and the Sack Splitting Theorem are established in a weak set theory whose principal axioms are Δ
_{0}collection, Δ_{0}separation, Π_{1}foundation, and V=L. - This paper is published with open access. It can be downloaded free-of-charge by following this link.

- Versions of the Friedberg–Muchnik Theorem and the Sack Splitting Theorem are established in a weak set theory whose principal axioms are Δ
- Interpreting Weak König’s Lemma using the Arithmetized Completeness Theorem. Proceedings of the American Mathematical Society 144:9 (2016), pp. 4021–4024.
- We present a previously unpublished proof of the conservativity of WKL
_{0}over IΣ_{1}using the Arithmetized Completeness Theorem, which, in particular, constitutes an ω‑interpretation of WKL_{0}in IΣ_{1}. We also show that WKL_{0}^{*}is interpretable in IΔ_{0}+exp. - A preprint version is available here in pdf. Part of the content was presented at the Logic Colloquium in Vienna, Austria in July 2014.

- We present a previously unpublished proof of the conservativity of WKL
- Constant regions in models of arithmetic. Notre Dame Journal of Formal Logic 56:4 (2015), pp. 603–624.
- This paper introduces a new theory of
*constant regions*, which generalizes that of interstices, in nonstandard models of arithmetic. In particular, we show that two homogeneity notions introduced by Richard Kaye and me, namely*constantness*and*pregenericity*, are equivalent. This leads to some new characterizations of generic cuts in terms of existential closedness. - A preprint version is available here in pdf.

- This paper introduces a new theory of
- With Richard Kaye. The model theory of generic cuts. In Åsa Hirvonen, Juha Kontinen, Roman Kossak, and Andrés Villaveces (eds), Logic without Borders, vol. 5 in Ontos Mathematical Logic, pp. 281–295. De Gruyter, Berlin, 2015.
- This paper is an almost self-contained survey that attempts to put the recently discovered notion of
*generic cuts*into a proper model-theoretic context. The main new results are an existentially closure property and some model completeness properties. Some other known results are proven in alternative ways here. - A preprint version is available here in pdf.

- This paper is an almost self-contained survey that attempts to put the recently discovered notion of
- With Richard Kaye and Roman Kossak. Adding standardness to nonstandard arithmetic. In Patrick Cégielski, Charalampos Cornaros, and Costas Dimitracopoulos (eds), New Studies in Weak Arithmetics, no. 211 in CSLI Lecture Notes, pp. 179–197. CSLI Publications, Stanford, 2013.
- We discuss the model theory of structures
`(K,N)`that are elementarily equivalent to some`(M,ω)`where`M`is a nonstandard model of Peano Arithmetic and`ω`denotes the standard cut of`M`. We also look at slightly more general structures`(K,N)`that satisfy the common theory of all such`(M,ω)`. - A preprint version is available here in pdf.

- We discuss the model theory of structures
- With Richard Kaye. Truth in generic cuts. Annals of Pure and Applied Logic 161:8 (2010), pp. 987–1005.
- In Generic cuts in models of arithmetic (Mathematical Logic Quarterly 54:2 (2008), pp. 129–144) Richard Kaye initiated the study of generic cuts of a model of Peano Arithmetic relative to a notion of an indicator in the model. This paper extends that work. We generalize the idea of indicator to a related
*neighbourhood system*; this allows the theory to be extended to one that includes the case of elementary cuts. Most results transfer to this more general context, and in particular we obtain the idea of a generic cut relative to a neighbourhood system, which is studied in more detail. The main new result on generic cuts presented here is a description of truth in the structure`(M,I)`, where`I`is a generic cut of a model`M`of Peano Arithmetic. The special case of elementary generic cuts provides a partial answer to a question of Kossak in Four problems concerning recursively saturated models of arithmetic, Notre Dame Journal of Formal Logic 36:4 (1995), pp. 519–530. - A preprint version is available here in pdf.

- In Generic cuts in models of arithmetic (Mathematical Logic Quarterly 54:2 (2008), pp. 129–144) Richard Kaye initiated the study of generic cuts of a model of Peano Arithmetic relative to a notion of an indicator in the model. This paper extends that work. We generalize the idea of indicator to a related
- With Richard Kaye. On interpretations of arithmetic and set theory. Notre Dame Journal of Formal Logic 48:4 (2007), pp. 497–510.
- This paper starts by investigating Ackermann’s interpretation of finite set theory in the natural numbers. We give a formal version of this interpretation from Peano arithmetic (
`PA`) to Zermelo–Fraenkel set theory with the infinity axiom negated (`ZF-inf`) and provide an inverse interpretation going the other way. In particular, we emphasize the precise axiomatization of our set theory that is required and point out the necessity of the axiom of transitive containment or (equivalently) the axiom scheme of epsilon-induction. This clarifies the nature of the equivalence of`PA`and`ZF-inf`and corrects some errors in the literature. We also survey the restrictions of the Ackermann interpretation and its inverse to subsystems of`PA`and`ZF-inf`, where full induction, replacement, or separation is not assumed. The paper concludes with a discussion on the problems one faces when the totality of exponentiation fails, or when the existence of unordered pairs or power sets is not guaranteed. - A web version is available here in pdf.

- This paper starts by investigating Ackermann’s interpretation of finite set theory in the natural numbers. We give a formal version of this interpretation from Peano arithmetic (

## Theses, notes, and others

- The consistency of arithmetic. Lecture notes, Semester 1, 2018/19.
- Model theory of arithmetic. Lecture notes, Winter Semester 2014/15.
- Initial segments and end-extensions of models of arithmetic. PhD thesis, May 2010.
- Materials in this thesis are joint work with Richard Kaye. The thesis is organized into two independent parts.
- The first part is an extension of the recent work on generic cuts by Kaye and I in the Truth in generic cuts paper listed above. The focus here is the properties of the pairs
`(M,I)`where`I`is a generic cut of a model`M`. Amongst other results, we characterize the theory of such pairs, and prove that they are existentially closed in a natural category. In the second part, we construct end-extensions of models of arithmetic that are at least as strong as ATR_{0}. Two new constructions are presented. The first one uses a variant of Födor’s Lemma in ATR_{0}to build an internally rather classless model. The second one uses some weak versions of the Galvin–Prikry Theorem in adjoining an ideal set to a model of second-order arithmetic. - My thesis is available on the University of Birmingham eThesis Repository, which can be reached by clicking here.

- Generic cuts in a general setting. MPhil (qualifying) thesis, 2008.
- Materials in this thesis are also joint work with Richard Kaye. The main part of it is reproduced in Truth in generic cuts.
- This thesis, as submitted, is available here in pdf.

- With Richard Kaye. Number of conjugacy classes of indicated cuts. March 2008.
- This is addendum to Kaye’s Generic cuts in models of arithmetic cited above. The materials are reproduced in my MPhil (qualifying) thesis and in our paper.
- This note is available here in pdf.

- Models of Peano arithmetic. MSci report, 2006.
- Materials in this thesis are also joint work with Richard Kaye. It is made up of three parts. The first part studies an interpretation between Peano arithmetic and finite set theory discovered by Ackermann. It constitute a part of the On interpretations of arithmetic and set theory paper listed above. The second part surveys the properties of some popular forms of induction, and how they relate to each other. The third part gives an overview of the analogies between large cardinals and semiregular cuts, regular cuts, and strong cuts.