Well-quasi-orders on finite trees and transfinite sequences

2026-02-10T14:37:27Z

We study the well-quasi-order (wqo) consisting of the set of finite trees with leaf labels coming from an arbitrary wqo $Q$, ordered by tree homomorphisms which respect the order on the labels. This is a variant of the usual Kruskal tree ordering without infima preservation. We calculate the precise maximal order types of this class of wqos as a function of the maximal order type of the labels $Q$. In the process, we sharpen some recent results of Friedman and Weiermann. Furthermore, we show a correspondence with indecomposable transfinite sequences with finite range, over elements of the wqo $Q$, of length less than $ω^ω$. Nash-Williams proved that arbitrary transfinite sequences with finite range are also well-quasi-ordered, but there are no known methods to extract bounds on the maximal order type from the proof. More concrete proofs for sequences of length less than $α$ for some $α< ω^ω$ were given by Erdős and Rado. Using the correspondence, we obtain precise bounds for the entire collection of transfinite sequences with finite range of length less than $ω^ω$.

A Minimal Substitution Basis for the Kalmár Elementary Functions

2026-02-10T12:29:14Z

We show that the class of Kalmár elementary functions can be inductively generated from the addition, the integer remainder, and the base-two exponentiation, hence improving previous results by Marchenkov and Mazzanti. We also prove that the substitution basis defined by these three operations is minimal. Furthermore, we discuss alternative substitution bases under arity constraints.

Paths, Ends and The Separation Problem for Infinite Graphs

2026-02-10T10:21:53Z

We introduce and study the Separation Problem for infinite graphs, which involves determining whether a connected graph splits into at least two infinite connected components after the removal of a given finite set of edges. We prove that this problem is decidable for every highly computable graph with finitely many ends. Using this result, we demonstrate that König's Infinity Lemma is effective for such graphs. We also apply it to analyze the complexity of the Eulerian Path Problem for infinite graphs, showing that much of its complexity arises from counting ends. Indeed, the Eulerian Path Problem becomes strictly easier when restricted to graphs with a fixed number of ends. Under this restriction, we provide a complete characterization of the problem. Finally, we study the Separation Problem in a uniform setting (i.e., where the graph is also part of the input) and offer a nearly complete characterization of its complexity and its relationship to counting the number of ends.

Super Black Boxes Revisited

2026-02-10T09:47:06Z

Let $ κ, θ< λ$ be cardinals, with $λ$ and $κ$ regular. Concentrating on a simple case, we say that the triple $(λ,κ,θ)$ has a Super Black Box when the following holds. For some stationary $S \subseteq \{δ< λ: cf(δ) = κ\}$ and $\overline C = \langle C_δ: δ\in S \rangle$, where $C_δ$ is a club of $δ$ of order type $κ$, for every coloring $\overline F = \langle F_δ: δ\in S \rangle$ with $F_δ: {}^{C_δ}λ\to θ$, there exists $\langle c_δ: δ\in S\rangle \in {}^S\!θ$ such that for every $f : λ\to θ$, for stationarily many $δ\in S$, we have $F_δ(f \upharpoonright C_δ) = c_δ$. In an earlier work, it was proved (along with much more) that for a class of cardinals $λ$ this holds for many pairs $(κ,θ)$. E.g.~$κ< \aleph_ω$ is large enough, and $\beth_ω(θ) < λ$. However, the most interesting cases (at least with regards to Abelian groups) are $κ= \aleph_0,\aleph_1$ (which have not been covered yet). Here we restrict ourselves to the case where $\overline F$ is a {so-called} \emph{continuous coloring}, which includes the case where $F_δ$ is computed from some $$ \big\langle F_{δ,β}'(f \upharpoonright (C_δ\cap β)) : β\in C_δ\big\rangle. $$ This covers the cases we have in mind. We mainly prove results without any other caveats: e.g. For every regular $κ$ and $θ$ there exists such a $λ$. We also deal with having multiple {$\bar C$-s}, and the existence of quite free subsets of ${}^κμ$.

Strong Completeness of Provability Logic for Uncountable Languages

2026-02-10T07:06:59Z

For an ordinal $λ>0$, we use the Erdős--Rado partition theorem to prove the failure of strong completeness for modal languages of cardinality $(2^{|λ|+\aleph_0})^{+}$ with respect to models on ordinals equipped with the generalized Icard topologies $\mathcal{I}_λ$ and ${τ_{c}}_{+λ}$. Specifically, we show that for such languages there exists a consistent set of formulas having neither $(Θ, \mathcal{I}_λ)$-model nor $(Θ, {τ_{c}}_{+λ})$-model. We also introduce a natural class of topological spaces, called $λ$-bouquet spaces, and prove that they yield strong completeness of $\mathsf{GL}$ for languages of cardinality $λ$.

Topological Semantics for Common Inductive Knowledge

2026-02-10T03:01:26Z

Lewis' account of common knowledge in Convention describes the generation of higher-order expectations between agents as hinging upon agents' inductive standards and a shared witness. This paper attempts to draw from insights in learning theory to provide a formal account of common inductive knowledge and how it can be generated by a witness. Our language has a rather rich syntax in order to capture equally rich notions central to Lewis' account of common knowledge; for instance, we speak of an agent 'having some reason to believe' a proposition and one proposition 'indicating' to an agent that another proposition holds. A similar line of work was pursued by Cubitt & Sugden 2003; however, their account was left wanting for a corresponding semantics. Our syntax affords a novel topological semantics which, following Kelly 1996's approach in The Logic of Reliable Inquiry, takes as primitives agents' information bases. In particular, we endow each agent with a 'switching tolerance' meant to represent their personal inductive standards for learning. Curiously, when all agents are truly inductive learners (not choosing to believe only those propositions which are deductively verified), we show that the set of worlds where a proposition $P$ is common inductive knowledge is invariant of agents' switching tolerances. Contrarily, the question of whether a specific witness $W$ generates common inductive knowledge of $P$ is sensitive to changing agents' switching tolerances. After establishing soundness of our proof system with respect to this semantics, we conclude by applying our logic to solve an 'inductive' variant of the coordinated attack problem.

Stable Canonical Rules for Intuitionistic Modal Logics

2026-02-10T02:33:26Z

This paper develops stable canonical rules for intuitionistic modal logics, which were first introduced for superintuitionistic logics and transitive nor mal modal logics in [1] and [2] respectively. We first prove that every in tuitionistic modal multi-conclusion consequence relation is axiomatizable by stable canonical rules. This allows us to assume, without loss of generality, that rules considered by us are stable canonical ones. The idea turns out to be useful. In particular, using stable canonical rules, we get an alterna tive proof of the Blok-Esakia theorem for intuitionistic modal logics which was first proved in [3] and generalize it to multi-conclusion consequence re lations. We also prove the Dummett-Lemmon conjecture for intuitionistic modal multi-conclusion consequence relations, which, as far as we know, is a new result.

A Theory for Probabilistic Polynomial-Time Reasoning

2026-02-10T00:39:49Z

In this work, we propose a new bounded arithmetic theory, denoted $APX_1$, designed to formalize a broad class of probabilistic arguments commonly used in theoretical computer science. Under plausible assumptions, $APX_1$ is strictly weaker than previously proposed frameworks, such as the theory $APC_1$ introduced in the seminal work of Jerabek (2007). From a computational standpoint, $APX_1$ is closely tied to approximate counting and to the central question in derandomization, the prBPP versus prP problem, whereas $APC_1$ is linked to the dual weak pigeonhole principle and to the existence of Boolean functions with exponential circuit complexity. A key motivation for introducing $APX_1$ is that its weaker axioms expose finer proof-theoretic structure, making it a natural setting for several lines of research, including unprovability of complexity conjectures and reverse mathematics of randomized lower bounds. In particular, the framework we develop for $APX_1$ enables the formulation of precise questions concerning the provability of prBPP=prP in deterministic feasible mathematics. Since the (un)provability of P versus NP in bounded arithmetic has long served as a central theme in the field, we expect this line of investigation to be of particular interest. Our technical contributions include developing a comprehensive foundation for probabilistic reasoning from weaker axioms, formalizing non-trivial results from theoretical computer science in $APX_1$, and establishing a tailored witnessing theorem for its provably total TFNP problems. As a byproduct of our analysis of the minimal proof-theoretic strength required to formalize statements arising in theoretical computer science, we resolve an open problem regarding the provability of $AC^0$ lower bounds in $PV_1$, which was considered in earlier works by Razborov (1995), Krajicek (1995), and Muller and Pich (2020).

Impredicativity in Linear Dependent Type Theory

2026-02-09T16:12:57Z

We construct a realizability model of linear dependent type theory from a linear combinatory algebra. Our model motivates a number of additions to the type theory. In particular, we add a universe with two decoding operations: one takes codes to cartesian types and the other takes codes to linear types. The universe is impredicative in the sense that it is closed under both large cartesian dependent products and large linear dependent products. We also add a rule for injectivity of the modality turning linear terms into cartesian terms. With all of the additions, we are able to encode (linear) inductive types. As a case study, we consider the type of lists over a linear type, and demonstrate that our encoding has the relevant uniqueness principle. The construction of the realizability model is fully formalized in the proof assistant Rocq.

Partition theorems for Ketonen-Solovay largeness

2026-02-09T15:19:42Z

We develop the framework of $α$-largeness introduced by Ketonen and Solovay, by proving a partition theorem for $α$-large sets with $α< ε_0$ which generalizes theorems from Ketonen and Solovay and from Bigorajska and Kotlarski. We also prove that for every $ω^{nk+3}$-large set $X$ with $\min X \geq 18$, every coloring $f : [X]^2 \to k$ admits an $ω^n$-large $f$-homogeneous subset. This bound is tight, up to an additive constant.

Generic derivations, differential largeness, and NTP$_2$

2026-02-09T13:50:22Z

We compare Fornasiero and Terzo's framework of generic derivations on algebraically bounded structures with León Sánchez and Tressl's differentially large fields. We show in the case of a single derivation that genericity and differential largeness coincide for éz-fields, as introduced by Walsberg and Ye. We also show that an NTP$_2$ algebraically bounded structure remains NTP$_2$ after expanding by a generic derivation.

The Banach-Tarski paradox in complete discretely valued fields

2026-02-09T10:45:40Z

We prove some results related to the classical Banach--Tarski paradox in the setting of a field $\mathbb{K}$ that is complete with respect to a discrete non-Archimedean valuation (e.g., when $\mathbb{K}$ is the field $\mathbb{Q}_p$ of $p$-adic numbers for a prime $p$). Namely, the field $\mathbb{K}$, as well as all balls and spheres in $\mathbb{K}$, admit a paradoxical decomposition with respect to the isometry group of $\mathbb{K}$. Such decompositions can be realized using pieces with the Baire property if $\mathbb{K}$ is separable. Under the additional assumption of local compactness of $\mathbb{K}$ (e.g., when $\mathbb{K}=\mathbb{Q}_p$), any two bounded subsets of $\mathbb{K}$ with nonempty interiors are equidecomposable with respect to the isometry group of $\mathbb{K}$. Our results complete the study of paradoxical decompositions in the non-Archimedean setting, addressing the one-dimensional case and building on earlier work for higher-dimensional normed spaces over $\mathbb{K}$ with respect to groups of affine isometries.

Cardinality of the sets of dimension functions in ordered structures

2026-02-09T04:11:16Z

We compute the cardinality $\mathfrak n_{\dim}(\mathcal M)$ of the sets of dimension functions on the ordered structures $\mathcal M$. The inequality $\mathfrak n_{\dim}(\mathcal M) \leq 1$ holds if $\mathcal M$ is a d-minimal expansion of an ordered group. If $\mathcal M$ is o-minimal and $\mathfrak n_{\dim}(\mathcal M)<\infty$, there exists a positive integer $m$ such that $\mathfrak n_{\dim}(\mathcal M)=2^m-1$. For every positive integer $m$, there exists a weakly o-minimal expansion $\mathcal M$ of an ordered divisible Abelian group such that $\mathfrak n_{\dim}(\mathcal M)=m$.

$\star$-translation for Varsovian models

2026-02-09T01:04:00Z

The technique of $\star$-translation is important in arguments calibrating the strengths of determinacy theories against large cardinals, for example in [9] and [1] in the paper's bibliography. It has also been used in analysing the internal theory of mice, for example in [5], [3], [6]. We give a detailed development of $\star$-translation, slightly strengthening the large cardinal level in the development of [1]. We then develop a variant of $\star$-translation for Varsovian models, in which certain extenders overlapping the Woodin cardinal are total, and used to directly induce extenders on the sequence of the $\star$-translation (details for this component are missing from this draft). This variant was used in [3] and [6], where it was outlined but not developed in detail. We use the material to verify the star-translation hypothesis of [5] and deduce some self-iterability facts.

Some model theory of the Heisenberg group

2026-02-08T23:52:06Z

We show that a field $K$ is model complete (in the language of rings) if and only if the Heisenberg group $H(K)$ is model complete (in the language of groups). To show that, we extend Levchuk's result about automorphisms of $H(K)$ to the case of monomorphisms $H(K)\to H(M)$. We also show that $H(K)$ does not have quantifier elimination and discuss its (non-)bi-interpretability with $K$.