Programme

Wednesday, 16 September
10:00 – 10:30	Meet and greet
10:30 – 11:30	Ludovic Patey, Largeness and partial conservation
11:30 – 12:00	Coffee break
12:00 – 12:30	Mengzhou Sun, The cohesive and stable Ramsey theorems and proof size over a weak base theory
12:30 – 13:00	Yuzuki Kaneko, Quasi-Polish spaces and spaces of unbounded filters in reverse mathematics
13:00 – 15:00	Lunch break
15:00 – 15:30	Michał J. Gajda, Arithmetic of monotonic bounds
15:30 – 16:00	Anders Lundstedt, Finitely non-standard models of Robinson arithmetic
16:00 – 16:30	Coffee break
16:30 – 17:00	Konrad Zdanowski, A strong completeness theorem for CTL
17:00 – 18:00	Keita Yokoyama, Kazuyuki Tanaka’s work in reverse mathematics and second-order arithmetic

Thursday, 17 September
10:00 – 11:00	Neil Thapen, The dominance rule in SAT solving
11:00 – 11:30	Coffee break
11:30 – 12:30	Patrick Uftring, Reals as naive Cauchy sequences in reverse mathematics
14:00 – …	Excursion
19:00 – …	Dinner

Friday, 18 September
10:00 – 11:00	Albert Visser, The Bezboruah-Shepherdson Incompleteness Theorem
11:00 – 11:30	Mojtaba Mojtahedi, An extension of HA by sentential PEM
11:30 – 12:00	Coffee break
12:00 – 12:30	David Hofmann, Unfolding of Grzegorczyk systems
12:30 – 13:00	Carl Jacobsen, Undecidability and definability results using the coprime relation
13:00 – 15:00	Lunch break
15:00 – 16:00	Athar Abdul-Quader, Weak cuts in models of PA
16:00 – 16:30	Coffee break
16:30 – 17:00	Patryk Szlufik, On a gap in Scott spectra of IΣn + exp + ¬BΣn
17:00 – 17:30	Roman Kossak, Kotlarski’s question

Invited talks

Athar Abdul-Quader, Weak cuts in models of PA

Strong cuts play an important role in the model theory of arithmetic, dating back to work by Kirby and Paris on independence results [2] [3]. In this talk we study cuts satisfying weaker properties of cuts which have arisen in various ways. First, we study separable cuts, which arose in [1] as those cuts I in countable recursively saturated models of PA for which there exist truth predicates T that are correct for disjunctions of the form (0 = 1) for any c ∈ I. We compare these with rational and superrational cuts studied in [4] in connection with the automorphism group of models of PA. We study the arithmetical properties of these cuts, as well as those studied by Kirby and Paris in [2] and [3]. We close with some open questions about cuts definable from truth predicates in countable, recursively saturated models of PA.

[1] Abdul-Quader, Athar and Łełyk, Mateusz. Pathologies in satisfaction classes. Annals of Pure and Applied Logic, vol. 175 (February 2024), no. 2.

[2] Kirby, L.A.S. Initial segments of models of arithmetic. Ph.D. thesis. University of Manchester (1977).

[3] Kirby, L.A.S and Paris, J.B. Initial segments of models of Peano’s axioms. Lecture Notes in Mathematics vol. 619 (1977), pp. 211–216.

[4] Kossak, Roman. Models with the ω property. The Journal of Symbolic Logic vol. 54 (March 1989), no. 1, pp. 177–189.

 

Ludovic Patey, Largeness and partial conservation

Generalizing the celebrated Paris-Harringon theorem, Ketonen and Solovay [1] introduced α-largeness as a transfinite generalization of the notion of cardinality for finite sets. In particular, a finite set F ⊆ ℕ is n-large if card F ≥ n, and ω-large if card F ≥ 1 + min F.

This notion turns out to be an essential tool for proving conservation theorems for ∀Π⁰₃-sentences, where a sentence is ∀Γ if it is of the form ∀X φ(X) for some Γ-formula φ. Beyond partial conservation theorems, explicit α-largeness bounds computations for combinatorial theorems are of independent interest, as providing a finitary quantitative counterpart to countably infinite combinatorics.

In this talk, we will survey basic combinatorics of α-largeness together with its applications to ∀Π⁰₃-conservation theorems, and present a parameterized extension for ∀Π⁰₄-sentences. This is a joint work with Quentin Le Houérou and Keita Yokoyama.

[1] Ketonen, J., Solovay, R. Rapidly growing Ramsey functions. Ann. of Math. (2) 113(2), 267–314 (1981), https://doi.org/10.2307/2006985

 

Neil Thapen, The dominance rule in SAT solving

A SAT solver is an algorithm that tries to decide if a propositional CNF is satisfiable. If not, it should output a refutation of the CNF in a standard propositional proof system, as a witness to unsatisfiability. I will talk about an application of bounded arithmetic to compare two proof systems that have arisen in practice to play this role for a range of SAT solving algorithms. This is joint work with Leszek Kolodziejczyk.

 

Patrick Uftring, Reals as naive Cauchy sequences in reverse mathematics

Representing reals as fast-converging Cauchy sequences has a long history and comes with several advantages: Equality is Π⁰₁ and, e.g. in the field of reverse mathematics, finite sums and maxima can be defined without the use of Σ⁰₂-collection. Moreover, certain values such as bounds (in form of natural numbers) can be computed and signs of non-zero inputs can easily be searched for. For these and many more reasons, fast-converging Cauchy sequences are established as the preferred way to talk about reals, not only in the context of reverse mathematics (cf. [3, Sections I.4 and I.8]) but also in proof mining as well as computable analysis.

There are two issues with this approach: First, fast-converging Cauchy sequences are an ad-hoc solution to the raised problems. They do not, however, appear in first year textbooks on analysis. Hence, an argument can be made that they do not accurately capture what reverse mathematics intends to analyze. Secondly, statements such as the Bolzano-Weierstraß theorem quickly reach the strength of arithmetical comprehension. Here, we may ask if it is possible to develop basic analysis strictly below this system.

In this talk, we present joint work with Anton Freund and Nicholas Pischke (cf. [1]), in which we explored a substantial amount of real analysis using reals in the form of Cauchy sequences without any restrictions on their modulus. While some statements such as the mentioned existence of finite sums or maxima slightly increase in strength, others such as the Bolzano-Weierstraß theorem now stay strictly below arithmetical comprehension (this particular example has already been discussed by Kreuzer, cf. [2]). Moreover, the usual path to arithmetical comprehension via weak Kőnig’s lemma is surprisingly shifted to weak consequences of Ramsey’s theorem such as Σ⁰₂-collection or the cohesiveness principle.

[1] A. Freund, N. Pischke, and P. Uftring, Avoiding logical strength in real analysis, submitted, arXiv:2605.15151.

[2] A. P. Kreuzer, The cohesive principle and the Bolzano-Weierstraß principle, Mathematical Logic Quarterly, vol. 57 (2011), no. 3, pp. 292–298.

[3] S. Simpson, Subsystems of Second Order Arithmetic, Perspectives in Logic, Cambridge University Press, 2009.

 

Albert Visser, The Bezboruah-Shepherdson Incompleteness Theorem

In 1976, Amala Bezboruah and John Shepherdson published an Incompleteness Theorem that was advertised as a Second Incompleteness Theorem for Q. Georg Kreisel objected that such a result was meaningless since Q could not verify basic properties of a provability predicate.

In my talk, I will discuss why the usual formulation of the result is defective. The proper statement tells us that the theory PA⁻ does not prove the consistency of a very weak theory BeSh. I will (try to) undermine Kreisel’s objection, as a supposedly philosophical insight, by arguing that there is no reason that a theory should prove meaning postulates for a provability predicate in order to talk about it.

I will discuss a new proof of the Bezboruah-Shepherdson Theorem for a different sequence coding based on ideas of Nielsen and Markov. The new proof works for PA⁻ plus all true universal sentences.

Finally, I will indicate how, even if PA⁻ does not prove the Löb Conditions, it still has an interesting provability logic. For example, in this logic, we still have uniqueness of modalised fixed points.

 

Keita Yokoyama, Kazuyuki Tanaka’s work in reverse mathematics and second-order arithmetic

This talk presents an overview of Professor Kazuyuki Tanaka’s profound and enduring contributions to mathematical logic, with a particular emphasis on his foundational work in reverse mathematics and subsystems of second-order arithmetic. In honoring his memory, we will examine several central themes of his research, illustrating how his insights elegantly bridged model theory and proof theory.

One of Tanaka’s most prominent research areas is the analysis of determinacy for finite Borel hierarchies [5, 6]. In particular, he studied determinacy axioms for the difference hierarchies of Σ⁰₁ and Σ⁰₂. From these axioms, he extracted new set existence principles that extend beyond the traditional “Big Five” subsystems. Together with many of his students, he clarified the complex structure of these determinacy systems [2]. This structural analysis was truly his lifework.

Whenever Tanaka discussed the highlights of his research, he always mentioned the conservation theorem that S. Simpson referred to as “Tanaka’s Conjecture” [4]. This theorem generalizes Harrington’s classical result by showing that WKL₀ is conservative over RCA₀ not only for Π¹₁ sentences, but also for sentences asserting unique existence (∃!). It carries many intriguing implications; for instance, it can be used to derive a proof of the Fundamental Theorem of Algebra within RCA₀.

Tanaka’s Self-Embedding Theorem for WKL₀
The core of this talk focuses on Tanaka’s celebrated 1997 self-embedding theorem [8], a key result in the model theory of second-order arithmetic. The theorem states that every countable nonstandard model (M,𝒳) of WKL₀ has a proper initial segment I ⊆_e M such that the cut I, equipped with the coded sets of M bounded in I, is isomorphic to the original model (M,𝒳). This theorem generalizes Friedman’s classical self-embedding theorem for Peano arithmetic [11] to second-order arithmetic. Through subsequent analyses by researchers such as Wong and Enayat [1, 10], this result has led to important characterizations of many models in both first-order and second-order arithmetic. Furthermore, a major application of this theorem is that it allows nonstandard analysis to be applied effectively within reverse mathematics [7]. By using this framework, we can formalize nonstandard arguments and make complex proofs much more straightforward, such as the construction of the Haar measure [9] and the proof of the Jordan Curve Theorem [3].

[1] Ali Enayat and Tin Lok Wong. Unifying the model theory of first-order and second-order arithmetic via WKL^*₀. Ann. Pure Appl. Logic, 168(6):1247–1283, 2017.

[2] MedYahya Ould MedSalem and Kazuyuki Tanaka. Δ⁰₃-determinacy, comprehension and induction. J. Symbolic Logic, 72(2):452–462, 2007.

[3] Nobuyuki Sakamoto and Keita Yokoyama. The Jordan curve theorem and the Schönflies theorem in weak second-order arithmetic. Arch. Math. Logic, 46(5-6):465–480, 2007.

[4] Stephen G. Simpson, Kazuyuki Tanaka, and Takeshi Yamazaki. Some conservation results on weak König’s lemma. Ann. Pure Appl. Logic, 118(1-2):87–114, 2002.

[5] Kazuyuki Tanaka. Weak axioms of determinacy and subsystems of analysis. I. Δ⁰₂ games. Z. Math. Logik Grundlag. Math., 36(6):481–491, 1990.

[6] Kazuyuki Tanaka. Weak axioms of determinacy and subsystems of analysis. II. Σ⁰₂ games. Ann. Pure Appl. Logic, 52(1-2):181–193, 1991. International Symposium on Mathematical Logic and its Applications (Nagoya, 1988).

[7] Kazuyuki Tanaka. Non-standard analysis in WKL₀. Math. Logic Quart., 43(3):396–400, 1997.

[8] Kazuyuki Tanaka. The self-embedding theorem of WKL₀ and a non-standard method. Ann. Pure Appl. Logic, 84(1):41–49, 1997. Fifth Asian Logic Conference (Singapore, 1993).

[9] Kazuyuki Tanaka and Takeshi Yamazaki. A non-standard construction of Haar measure and weak König’s lemma. J. Symbolic Logic, 65(1):173–186, 2000.

[10] Tin Lok Wong. Models of the weak König lemma. Ann. Japan Assoc. Philos. Sci., 25:25–34, 2017.

[11] Keita Yokoyama. Notes on various versions of Friedman’s self-embedding theorem. In Studies in weak arithmetics. Vol. 3, volume 217 of CSLI Lecture Notes, pages 231–241. CSLI Publ., Stanford, CA, 2016.

 

Contributed talks

Michał J. Gajda, Arithmetic of monotonic bounds

We present an arithmetic of monotonic bounds with a syntax-directed, cut-free domination calculus (Definition 3). The calculus is sound for the semantic domination relation ρ ≼ σ (⟦ρ⟧ ≤ ⟦σ⟧ in every positive environment): ρ ⊴ σ ⇒ ρ ≼ σ. We prove cut-elimination and give the complete rule set. The key results are the calculus’s computational reach beyond primitive recursion [9] and its soundness. All results are mechanised in Agda.^*

Definition 1 (Term syntax).
Types and terms over the positive cone ℕ_≥ 1 = ℕ∖{0}:

𝕊 is successor, ℙ the clamped predecessor (clamped at 1), an explicit λ binder, and iteration 𝕀(f,k,a) composes the function f k times from start a: 𝕀(f,k,a) = f^k(a). Terms are intrinsically typed, so only well-typed terms are formed.

Definition 2 (Semantics).
Denotation is higher-order, given by:

Evaluation is defined by structural recursion:

where ⟦f⟧^⟦k⟧ means ⟦k⟧-fold composition. Evaluation is total (intrinsic typing ensures well-foundedness).

Iteration at type ι → ι climbs the hyperoperation hierarchy: addition, multiplication, exponentiation, tetration, and the tower tetr 2 b = 2⇈b are all single closed λ-terms derived from {𝕊,ℙ,1,𝕀,max} (Table 1). The carrier has no additive 0: multiplication iterates from 1 and overshoots by one, with ℙ correcting the offset; exponentiation iterates from 1, its genuine base a⁰ = 1.

The predicates used for the iteration rules below are:

• inflationary f: f is inflationary — x ≤ ⟦f⟧(x) for every x in every positive environment.
• monotone f: f is monotone — x ≤ y implies ⟦f⟧(x) ≤ ⟦f⟧(y).
• f ⊲ f’: strict domination — f ⊴ f’ but f’ ⋪ f.

The auxiliary judgments inflationary f and monotone f have syntactic inference rules (mechanised by structural recursion); the full calculus follows Abel [1] and Icard–Moss–Tune [5]:

The domination calculus below is cut-free (transitivity is admissible via the successor-step and max-introduction rules).

Definition 3 (Domination calculus).

The calculus is syntax-directed: the head constructor of a guides rule selection; the auxiliary judgments inflationary f, monotone f, and f ⊴ f’ for function-type terms each have their own inference systems (f ⊴ f’ for function terms is defined analogously via λ-body comparison and transitivity).

The calculus ⊴ extends the class of functions reachable beyond primitive recursion [2] while remaining deductively weaker than PRA in the sense of Schirrn and Niebergall [9]: the if-free, induction-free rule set cannot capture n+1 ≤ 2n without explicit max, a gap inherited from the prior domination inference system [4]. Unlike first-order arithmetics (Presburger [7], Skolem [10][6], Robinson Q [8], or Buss’s S¹₂ [3]), the present system is a purely syntactic calculus of term inequalities — not a theory with a model class — so questions of semantic completeness or arithmetic decidability do not directly apply.

Theorem 4 (Ackermann bound).
The closed terms fAck and Hyp (Table 1) satisfy fAck(n) ≥ ack(n,n) and Hyp(n) ≥ ack(n,n) for every n on the positive carrier.

Hence the arithmetic reaches beyond all primitive-recursive functions (Ackermann 1928).

Theorem 5 (Soundness).
Every derivation ρ ⊴ σ in the domination calculus is valid in every positive environment: ⟦ρ⟧ ≤ ⟦σ⟧ whenever the environment assigns values ≥ 1.

Theorem 6 (Transitivity elimination).
The domination calculus admits a transitivity rule: if ρ ⊴ σ and σ ⊴ τ then ρ ⊴ τ. Transitivity is not primitive — it is admissible via the sucStep, maxLI, and maxRI rules together with the syntax-directed rule set.

This work generalises a prior domination inference system [4] and proves these results in Agda using a weak arithmetic.

---

---

[1] Abel, Andreas. 2006. Polarized Subtyping for Sized Types. In Computer Science – Theory and Applications (CSR 2006), 3967:381–92. LNCS. Springer. https://doi.org/10.1007/11753728_39.

[2] Ackermann, Wilhelm. 1928. Zum Hilbertschen Aufbau Der Reellen Zahlen. Mathematische Annalen 99 (1): 118–33. https://doi.org/10.1007/BF01459088.

[3] Buss, Samuel R. 1986. The Polynomial Hierarchy and Intuitionistic Bounded Arithmetic. In Structure in Complexity Theory, Proceedings of the Conference held at the University of California, Berkeley, California, USA, June 2-5, 1986, edited by Alan L. Selman, 223:77–103. Lecture Notes in Computer Science. Springer. https://doi.org/10.1007/3-540-16486-3/_91.

[4] Gajda, Michał J. 2024. Consistent Ultrafinitist Logic. In 29th International Conference on Types for Proofs and Programs (TYPES 2023), 303:5:1–20. LIPIcs. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. https://doi.org/10.4230/LIPIcs.TYPES.2023.5.

[5] Icard, Thomas, Lawrence S. Moss, and William Tune. 2017. A Monotonicity Calculus and Its Completeness. In Proceedings of the 15th Meeting on the Mathematics of Language (MoL 2017), 75–87. ACL. https://doi.org/10.18653/v1/w17-3408.

[6] Mostowski, Andrzej. 1952. On Direct Products of Theories. Journal of Symbolic Logic 17 (1): 1–31. https://doi.org/10.2307/2267454.

[7] Presburger, Mojżesz. 1930. Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In Sprawozdanie z I Kongresu Matematyków Słowiańskich, 92–101. Warsaw.

[8] Robinson, Raphael M. 1950. An Essentially Undecidable Axiom System. Proceedings of the International Congress of Mathematicians, 729–30.

[9] Schirn, Matthias, and Karl-Georg Niebergall. 2005. Finitism = PRA? On a Thesis of W. W. Tait. Reports on Mathematical Logic 39 (January): 3–24. https://rml.tcs.uj.edu.pl/rml-39/a-sch-39.htm.

[10] Skolem, Thoralf. 1930. Über gewisse Satzfunktionen in der Arithmetik. Skrifter Utgitt Av Videnskapsselskapet i Kristiania, I. Klasse, no. 7.

 

David Hofmann, Unfolding of Grzegorczyk systems

Feferman’s unfolding program asks, given a schematic system S, which operations, predicates, and principles concerning them ought to be accepted once one has accepted S (Feferman, [3]). So far, the program has investigated several foundational stances. These include but are not limited to the unfolding of non-finitist arithmetic 𝒰(NFA) (Feferman and Strahm, [4]), the unfolding of finitist arithmetic 𝒰(FA) (Feferman and Strahm [5]), and the unfolding of feasible arithmetic 𝒰(FEA) (Eberhard and Strahm, [2]). This investigation yielded the following technical results: the full unfolding of NFA is proof-theoretically equivalent to predicative analysis RA_<Γ0; the full unfolding of FA is proof-theoretically equivalent to primitive recursive arithmetic PRA; the provably total functions of the operational, the intermediate, and the full unfolding of FEA are exactly the polynomial-time computable functions.

These results occupy the predicative, finitist, and feasible limits, respectively. Between the feasible and finitist limits, however, the unfolding spectrum remains unexplored. This invites the investigation of the unfolding of a sequence of schematic systems G_n corresponding to the levels of the Grzegorczyk hierarchy. The Grzegorczyk hierarchy is the ideal candidate to fill this space since the union of its levels ℰⁿ exhausts the primitive recursive functions while maintaining strict inclusion ℰⁿ ⊊ ℰⁿ⁺¹ at every stage.

This work develops the unfolding of schematic systems G_n over the natural numbers, utilizing the methodology of Eberhard and Strahm, [2], but equipped with a growing language ℒ_n = {E₁, … , E_n} whose function symbols denote the first n hyperoperations, alongside open-ended successor induction. The reason for the choice of this formalization is to move the bounded totality requirement of FEA from binary words onto a unary successor representation. Under length induction along binary words, reaching an input β costs roughly log β steps, meaning iterated composition of a step function remains computationally low. Under a unary successor, however, it costs β steps, and β-fold composition is the mechanism allowing the ascension of the hierarchy levels. Here, the computational level is not rigidly stipulated but dynamically emerges. By accepting G_n, the unfolding process accommodates closure under E_n-bounded recursion, with the finite base language capping the available bounding terms.

The central philosophical claim of this work rests on the notion of totality in our framework. The base theory of the unfolding is a partial combinatory algebra (PCA) which provides a general fixed point combinator. Using open-ended successor induction, the operational unfolding of G_n, 𝒰₀(G_n), can prove that the fixed-point term for E_n+1 converges on every input. But the system cannot bound E_n+1 by any ℒ_n-term, since E_n+1 strictly dominates every composition of E₁, … , E_n. Consequently, dropping the bounding requirement collapses the hierarchy and the provably convergent functions of 𝒰₀(G_n) encompass all of PRA uniformly for any n. In this system the commitments are tied to the intension of “total”.

This offers a new insight into the debate on the implicit commitment thesis (ICT), especially on the notion of epistemic stability introduced by Dean, [1]. ICT is mostly discussed in the context of meta-mathematical reflection and consistency (Łełyk and Nicolai, [7]; Głowacki and Zicchetti, [6]), whereas we investigate it through the notion of unfolding of an open-ended schematic system. In our proposed framework, epistemic stability is achieved by a strict notion of bounded totality, while an unbounded notion of totality leads to an epistemically unstable theory. We do not claim totality as the source of stability in general; stability is relative to the notion of commitment a stance is tested against, and reflection-based notions yield their own boundaries. But for stances whose formal explication is a closure condition on functions the constitutively appropriate notion of commitment is totality.

[1] Dean, Walter (2015). Arithmetical Reflection and the Provability of Soundness. In: Philosophia Mathematica 23.1, pp. 31–64. doi: 10.1093/philmat/nku026.

[2] Eberhard, Sebastian and Thomas Strahm (2015). Unfolding Feasible Arithmetic and Weak Truth. In: Unifying the philosophy of truth. Springer, pp. 153–167.

[3] Feferman, Solomon (1996). Gödel’s program for new axioms: Why, where, how and what? In: Gödel ’96. Ed. by P. Hájek. Vol. 6. Lecture Notes in Logic. Springer, pp. 3–22.

[4] Feferman, Solomon and Thomas Strahm (2000). The unfolding of non-finitist arithmetic. In: Annals of Pure and Applied Logic 104.1-3, pp. 75–96. doi: 10.1016/S0168-0072(00)00008-7.

[5] — (2010). Unfolding Finitist Arithmetic. In: The Review of Symbolic Logic 3.4, pp. 665–689. doi: 10.1017/S1755020310000183.

[6] Głowacki, Maciej and Matteo Zicchetti (2025). Implicit Commitments, Epistemic Stability, and the Acceptability of Consistency. In: Erkenntnis, pp. 1–24.

[7] Łełyk, Mateusz and Carlo Nicolai (2022). A theory of implicit commitment. In: Synthese 200.4, p. 284.

 

Carl Jacobsen, Undecidability and definability results using the coprime relation

We study undecidability and definability for certain extensions of ⟨ℕ; ⊥⟩, where ⊥ denotes the coprime relation. This is done in first-order logic without a logical symbol for equality.

Undecidability
Let S be the successor function. Woods proved in [3] that Th(ℕ; ⊥, S) is undecidable. We generalize his arguments to show that, for an extension of ⟨ℕ; ⊥⟩, a weak form of the independence property implies undecidability. Consequently, the following structures have undecidable theories:

• ⟨ℕ; ⊥, n ↦ |L(n)|⟩ for L ∈ ℤ[X] not a monomial
• ⟨ℕ; ⊥, n ↦ aⁿ-1⟩ for a > 1
• ⟨ℕ; ⊥, n ↦ ⌊an/b⌋⟩ for a, b ∈ ℕ with a ⊥ b, b ≥ 2.

Definability
Define m ∼ n if m and n have the same prime divisors. Another result of Woods [3] is that addition and multiplication are definable in ⟨ℕ; ⊥, S⟩ iff there is some k ∈ ℕ such that for all m, n ∈ ℕ we have

The last claim is the Erdős–Woods conjecture. With m, n restricted to the set of prime powers Π, the conjecture has been proven. Using this Richard proved for any arithmetic A ⊆ ℕ^N that  ∩ Π^N is definable in ⟨ℕ; ⊥, S⟩ [2].

The main theorem combines and generalizes these results. For certain extensions ℳ of ⟨ℕ; ⊥⟩, it shows that an arithmetic relation is definable in ℳ iff it satisfies a number-theoretic condition.

Let A ⊆ ℕ^N denote an arithmetic relation. We obtain the following, where the last result builds on Bès and Richard’s paper [1].

• A is definable in ⟨ℕ; ⊥, S⟩ iff there is some k ∈ ℕ such that for all m ∈ A, n ∈ ℕ^N we have .
• Let ω(n) be the number of prime divisors of n. Then A is definable in ⟨ℕ; ⊥, ω⟩ iff for all m ∈ A, n ∈ ℕ^N we have .
• For a ≥ 3 let P_a be the set of primes and a-th powers of primes and <_Pa be the restriction of < to P_a. Then A ∩ P^N_a is definable in ⟨ℕ; ⊥, <_Pa⟩.

[1] Alexis Bès and Denis Richard. Undecidable extensions of skolem arithmetic. The Journal of Symbolic Logic, 63(2):379–401, 1998.

[2] Denis Richard. All arithmetical sets of powers of primes are first-order definable in terms of the successor function and the coprimeness predicate. Discrete Mathematics, 53:221–247, 1985.

[3] Alan Woods. Some problems in logic and number theory and their connections. Ph. D. Thesis, Univ. of Manchester, 1981.

 

Roman Kossak, Kotlarski’s question

In the 1980s, Henryk Kotlarski published two papers devoted to the rich theory of elementary cuts in countable recursively saturated models of PA, [4, 5]. Let M be such a model. In both papers Kotlarski asked: What is the structure of the lattice of elementary substructures of M? In particular, does it depend on M?

For a model M, is the lattice of elementary submodels of M under inclusion, and Lt₀(M) is the ∨-subsemilattice of Lt(M) consisting of finitely generated elementary submodels of M. A partial answer to Kotlarski’s question is the following theorem.

Theorem 1. ([2]) Let M and N be countable arithmetically saturated models of the same completion of PA. The following are equivalent:

(1) M ≅ N;
(2) Lt(M) ≅ Lt(N);
(3) Lt₀(M) ≅ Lt₀(N).

The proof of (3)→(1) is based on an intricate coding of the standard system of a countable arithmetically saturated model M of PA in Lt(M) using particular facts about finitely generated submodels of M. Arithmetic saturation plays a crucial role. It is open whether the result holds for recursively saturated models that are not arithmetically saturated. Many other open questions remain. I propose two generalizations of Kotlarski’s question and I will present some partial answers based of some results from [3], [6], and the survey paper [1].

[1] Athar Abdul-Quader and Roman Kossak. The lattice problem for models of PA. Bull. Symb. Log., 32(2):259–286, 2026.

[2] Roman Kossak and James H. Schmerl. Arithmetically saturated models of arithmetic. Notre Dame J. Formal Logic, 36(4):531–546, 1995. Special Issue: Models of arithmetic.

[3] Roman Kossak and James H. Schmerl. On cofinal submodels and elementary interstices. Notre Dame J. Form. Log., 53(3):267–287, 2012.

[4] Henryk Kotlarski. On elementary cuts in models of arithmetic. Fund. Math., 115(1):27–31, 1983.

[5] Henryk Kotlarski. On elementary cuts in recursively saturated models of Peano arithmetic. Fund. Math., 120(3):205–222, 1984.

[6] James H. Schmerl. The diversity of minimal cofinal extensions. Notre Dame J. Form. Log., 63(4):493–514, 2022.

 

Anders Lundstedt, Finitely non-standard models of Robinson arithmetic

To the best of my knowledge, there is no systematic study of finitely non-standard models of Robinson arithmetic^*—that is, there is no systematic study of those models of Robinson arithmetic that have a non-empty finite set of non-standard numbers. I have made a modest attempt at such a systematic study (Lundstedt, [2]).

The main results are that for each such finitely non-standard model:

• The successor function is a permutation of the set of non-standard numbers (this follows trivially from the axioms). As is well-known, each permutation of a finite set has a unique decomposition into cycles on disjoint orbits.

• The restriction of addition to

  {⟨a, n⟩  :  a non-standard, n standard}

  is “tame”, in the sense that this restriction is determined already by the permutation given by the successor function:

  a+n = the result of starting at a and taking n steps in its cycle.

• The restriction of addition to

  {⟨α, a⟩  :  α standard or non-standard, a non-standard}

  is “wild”. Contrary to the previous restriction, this one is not determined by the successor function, but subject to some constraints—in particular, its range may only consist of non-standard numbers.

• Similar to the case of addition, the restriction of multiplication to
  

  {⟨a, n⟩  :  a non-standard, n standard}

  is determined by the successor function and addition, whereas the restriction of multiplication to
  

  {⟨α, a⟩  :  α standard or non-standard, a non-standard}

  is not uniquely determined (by the successor function and addition), but subject to some constraints.

---

---

[1] Robinson, Raphael M. (1950): An essentially undecidable axiom system. In: Proceedings of the International Congress of Mathematicians, volume I; pages 729–730; American Mathematical Society; Providence 1952.

[2] Lundstedt, Anders E.V. (2025): Finitely non-standard models of Robinson arithmetic; version 2025-06-10. In: Natural induction (a model-theoretic study); PhD thesis in preparation. URL: https://anderslundstedt.com/research/#induction-drafts

 

Mojtaba Mojtahedi (j.w.w. Mohammad Ardeshir), An extension of HA by sentential PEM

Intermediate arithmetic, is an arithmetic in between Heyting Arithmetic HA and Peano Arithmetic PA. Intermediate arithmetics are well-studied in the literature [1]. For example, [1] shows that all intermediate arithmetics over propositional logics with finite model property, has the so called de Jongh property.

An intermediate arithmetic IA, usually is constructed on the basis of some propositional axiom scheme φ(p₁, …, p_n) in the following way. IA is HA plus the universal closure of φ(A₁, …, A_n) for A_i being arbitrary formulas. Also recently, a heirarchy of such intermediate arithmetics have been considered by restriction of the substituted formulas to some Σ⁰_n or Π⁰_n-formulas [4, 3, 2]. However, an important variant is missing in such heirarchies: the sentential fragment of such intermediate arithmetics. In this study, in particular, we consider the extension of Heyting arithmetic by all instances of the Principle of Excluded Middle PEM by arithmetical sentences, called HA+PEM^s. We investigate the basic properties of HA+PEM^s. Among other things, we show that such intermediate arithmetic, has the same provability logic of PA.

[1] de Jongh, D., Verbrugge, R., and Visser, A. (2011). Intermediate logics and the de jongh property. Archive for Mathematical Logic, 50:197–213.

[2] Fujiwara, M. (2026). On the hierarchy of linearity axioms. Archive for Mathematical Logic, 65(3):319–331.

[3] Fujiwara, M., Ishihara, H., Nemoto, T., Suzuki, N.-Y., and Yokoyama, K. (2023). Extended frames and separations of logical principles. Bulletin of Symbolic Logic, 29(3):311–353.

[4] Fujiwara, M. and Kurahashi, T. (2022). Refining the arithmetical hierarchy of classical principles. Mathematical Logic Quarterly, 68(3):318–345.

 

Mengzhou Sun, The cohesive and stable Ramsey theorems and proof size over a weak base theory

Over the weak base theory RCA^*₀, most typical Ramsey-theoretic statements are ∀Π⁰₃-conservative, but they differ in terms of the effect on proof size for ∀Π⁰₃ sentences. The usual Ramsey’s theorem for pairs and two colours, RT²₂, induces iterated exponential proof speedup over RCA^*₀, even for very simple sentences [1]. In contrast, Kowalik [2] recently showed that the chain-antichain principle CAC can be polynomially simulated by RCA^*₀. Whether the combinatorial principles discussed above yield significant proof speedup over RCA^*₀ depends on the kind of closure properties they imply for the definable cut I⁰₁, which is the intersection of all Σ⁰₁-definable cuts.

In the present work, we show that RCA^*₀ + CRT²₂, where CRT²₂ is the cohesive Ramsey’s theorem for pairs, implies exponential closure I⁰₁. Consequences include iterated exponential proof speedup of RCA^*₀ + CRT²₂ over RCA^*₀ for Π₁ sentences and the unprovability of CRT²₂ in RCA^*₀ + CAC. On the other hand, we show that proofs of ∀Π⁰₃ sentences in RCA^*₀ + SRT²₂, where SRT²₂ is stable Ramsey’s theorem for pairs, can be polynomially simulated by RCA^*₀. Nevertheless, SRT²₂ also implies a nontrivial property of I⁰₁, specifically closure under functions of quasipolynomial growth rate.

This is a joint work with Leszek Kołodziejczyk.

[1] Kołodziejczyk, Leszek Aleksander and Wong, Tin Lok and Yokoyama, Keita, Ramsey’s theorem for pairs, collection, and proof size, Journal of Mathematical Logic, vol. 24 (2024), no. 2, pp.2350007.

[2] Kowalik, Katarzyna W., A non-speedup result for the chain-antichain principle over a weak base theory, arXiv:2510.00323.

 

Patryk Szlufik, On a gap in Scott spectra of IΣ_n + exp + ¬BΣ_n

By a classical result of Scott, for every countable structure M there is a sentence of ℒ_ω1,ω — an extension of first-order logic with countable conjunctions and disjunctions — in the signature of M, which is satisfied by a countable structure N if and only if N and M happen to be isomorphic. We call such a sentence a Scott sentence of M. Furthermore, formulas in L_ω1,ω admit a hierarchy similar to the arithmetical one, starting with quantifier-free formulas denoted as Σⁱⁿ₀ = Πⁱⁿ₀. We then say that a formula is Σⁱⁿ_α if and only if it is of the form ⋁∃x̄_iφ_i(x̄_i,ȳ), where each φ_i is Πⁱⁿ_β for some β < α. The Π steps of the hierarchy are built accordingly. We then define the Scott rank of a model M as the least ordinal α such that every automorphic orbit of a tuple of elements of M is definable with a Σⁱⁿ_α formula. Equivalently, by the result [2] of Montalbán, we can define it as the least ordinal α such that M has a Πⁱⁿ_α+1 Scott sentence. Additionally, for a theory T, one can consider its Scott spectrum, i.e. the set of ordinals α such that some M ⊨ T has Scott rank α.

In the work [3], Montalbán and Rossegger initiated the Scott analysis of models of Peano Arithmetic. They characterized the Scott spectra of completions of PA, showing in particular that the only model M ⊨ PA of finite Scott rank is the standard model. This was further extended in [1].

In a joint work with Leszek Kołodziejczyk and Mateusz Łełyk [5], we have conducted a similar analysis for subsystems of PA, in most cases ones extending IΔ₀ + exp such as IΣ_n + exp or BΣ_n + exp. Among others, we have shown that for each n the Scott spectrum of IΣ_n + exp + ¬BΣ_n+1 consists of n+1 and all countable ordinals from n+3 onward. The methods used seem to fail irreparably in addressing the issue of models of IΣ_n + exp + ¬BΣ_n+1 of Scott rank n+2.

A part of recent result by Wei Wang [6] about Kaye’s cardinality scheme for coded ultrapowers introduced by Paris [4], coupled with the refinements of previously obtained results and a particular construction of an ultrapower, allowed us to obtain a class of models of IΣ_n + exp + ¬BΣ_n+1, all with Scott rank n+2. We will explore the proof, emphasizing yet another kind of construction and methods which can be used in the Scott analysis of weak systems of arithmetic.

[1] D. Gonzalez, M. Łełyk, D. Rossegger, and P. Szłufik. Classifying the complexity of models of arithmetic. 2025. arXiv 2507.12025 [math.LO].

[2] A. Montalbán. A robuster Scott rank. In Proceedings of the American Mathematical Society 143.12 (2015), pp. 5427–5436.

[3] A. Montalbán and D. Rossegger. The structural complexity of models of arithmetic. In The Journal of Symbolic Logic 89.4 (2024), pp. 1703–1719.

[4] J. B. Paris. Some conservation results for fragments of arithmetic. In Model Theory and Arithmetic. Ed. by C. Berline, K. McAloon, and J.-P. Ressayre. Vol. 890. Lecture Notes in Mathematics. Berlin Springer, 1981, pp. 251–262.

[5] P. Szłufik. Scott ranks of models of elementary arithmetic (Sept. 10, 2025). Talk at JAF44, joint work with Leszek Kołodziejczyk and Mateusz Łełyk.

[6] W. Wang. Finite Combinatorics and Fragments of Arithmetic. 2025. arXiv 2506.17943 [math.LO].

 

Yuzuki Kaneko, Quasi-Polish spaces and spaces of unbounded filters in reverse mathematics

The properties of separable complete metric spaces, also known as Polish spaces, have been well studied in reverse mathematics [1]. To study non-metrizable spaces in reverse mathematics, we need to formalize them in second-order arithmetic. In this talk, we formalize quasi-Polish spaces as a generalization of Polish spaces and study their properties.

In classical mathematics, quasi-Polish spaces provide a useful class when considering non-metrizable spaces, since every second-countable T₀ space is embeddable as a subspace of a quasi-Polish space. It is also known that quasi-Polish spaces are identical to Π⁰₂-subspaces of the countable power of the Sierpiński space (S^ℕ), as shown by de Brecht [2].

We first show that quasi-Polish spaces are equivalent to spaces of unbounded filters (UF spaces) and spaces of non-principal filters (NP spaces). This equivalence answers an open question from Mummert and Stephan [4], showing that the class of second-countable UF spaces is closed under countable products. Furthermore, these equivalences show why quasi-Polish spaces are important. For example, this class generalizes countable domains, making it important in computability theory. From the perspective of point-free topology, it can also be represented as the class of countably presented frames, as shown by Heckmann [5]. Moreover, in UF spaces, the reverse mathematical strength of classic topological theorems, such as Urysohn’s metrization theorem, has been analyzed by Mummert [3].

We analyze the necessary and sufficient axioms to prove that a space under one representation is homeomorphic to the same space under a different representation. In other words, we show the reverse mathematical strength needed to switch between these different representations. As illustrated below, while some implications are provable over the base system RCA₀, we show that the converses require the strong subsystem Π¹₁–CA₀:

Besides the differences in space representations, there are two different ways to represent elements in these spaces, and they have different logical strengths. For example, an element of a quasi-Polish space can be represented by either a left-Cauchy sequence or d̂-Cauchy sequence. In UF spaces, we can view a filter as a decreasing sequence or as a set. The second approach implies the first over RCA₀, but the converse requires ACA₀, as shown by Mummert [3]. This does not happen in metric spaces.

Furthermore, based on this setting, we can obtain some examples of reverse mathematical results on the classification of topological spaces, such as the Hurewicz theorem.

[1] Stephen G. Simpson. Subsystems of second order arithmetic. Perspectives in Logic, second edition. Cambridge University Press, Cambridge, 2009.

[2] Matthew de Brecht. Quasi-Polish spaces. Ann. Pure Appl. Logic, 164(3):356–381, 2013.

[3] Carl Mummert. On the reverse mathematics of general topology. The Pennsylvania State University, 2005.

[4] Carl Mummert and Frank Stephan. Topological aspects of poset spaces. Michigan Mathematical Journal, 59(1):3–24, 2010.

[5] Reinhold Heckmann. Spatiality of countably presentable locales (proved with the Baire category theorem). Mathematical Structures in Computer Science, 25(7):1607–1625, 2015.

 

Konrad Zdanowski (j.w.w. Kordula Świętorzecka), A strong completeness theorem for CTL

Starting from A. Prior [3] modal logics of discrete time are used in the philosophical investigations of time and determinism. Logics LTL and CTL are modal logics of infinite descrete linear and branching time, respectively. They are also widely used in the model theoretic verification of programs where the finite state program is presented as a Kripke model and the properties of all possible computations are expressed by formulas of LTL or CTL. The logic LTL is interpreted in the frames of ω-type ordering while the logic CTL is interpreted in the frames being infinite trees with no finite branches.

The set of tautologies of LTL were axiomatized in [2]. An axiomatization of tautologies of CTL was given in [1]. When axiomatizing the set of tautologies of the above logics there is no need to use infinite rules of inferences. However, when one is interested in systems with the strong completeness property, the infinitary systems are needed. This is so, because logics in questions are not compact. Indeed, the set of formulas {p, Xp, X²p, …} ∪ {¬Gp} is not satisfiable while any of its finite subsets is satisfiable.

The system is strongly complete for a logic L if it is complete with respect to any theory T in L. Then, the deductive system with strong completeness property for LTL was given by [5], see also [4].

It has been an open problem to construct an axiomatic system for CTL with strong completeness property. We present such a system strongly complete within a class of infinite finitely branching trees. Like Sundholm, we use a proper finitization of rules resulting with formulas of the form QG and QF, where Q ∈ {∀, ∃}. The restriction of semantics to finitely branching trees, due to Weak König Lemma, ensures that the rules for ∃G are sound. Moreover, we add continuum many rules to ensure the inconsistency of theories which forces infinite branching of their models. To finitize these type of rules we consider two types of inferences: ⊢_f and ⊢_ω, where the former is a finitary version of the latter. According to ⊢_f, if a theory forces at a tree level n more than f(n) nodes, it is inconsistent.

[1] E. A. Emerson and J. Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time, Proceedings of the Fourteenth Annual ACM Symposium on Theory of Computing – STOC ’82. Association for Computing Machinery, 1982, pp. 169–180.

[2] D. Gabbay, A. Pnueli, S. Shelah, and J. Stavi, On the temporal analysis of fairness, In: Proceedings of the 7th ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages (POPL ’80), Las Vegas, Nevada, pp. 163–173, 1980. Association for Computing Machinery, New York. DOI: 10.1145/567446.567462.

[3] A. N. Prior, Time and Modality, Oxford University Press, Oxford, 1957.

[4] K. Segerberg, Von Wright’s Tense Logic, In: P. A. Schilpp and L. E. Hahn (eds.), The Philosophy of Georg Henrik von Wright, Library of Living Philosophers, Vol. 19, Open Court, 1989, pp. 603–635. Written in 1974.

[5] G. Sundholm, A Completeness Proof for an Infinitary Tense-Logic, Theoria, 43(1):47–51, 1977. DOI: 10.1111/j.1755-2567.1977.tb00778.x.