One-ended spanning subforests and treeability of groups

2026-03-19T17:57:28Z

We show that several new classes of groups are measure strongly treeable. In particular, finitely generated groups admitting planar Cayley graphs, elementarily free groups, and the group of isometries of the hyperbolic plane and all its closed subgroups. This provides the first examples of one-ended nonamenable groups which are measure strongly treeable. In higher dimensions, we also prove a dichotomy that the fundamental group of a closed aspherical 3-manifold is either amenable or has strong ergodic dimension 2. Our main technical tool is a method for finding measurable treeings of Borel planar graphs by constructing one-ended spanning subforests in their planar dual. Our techniques for constructing one-ended spanning subforests also give a complete classification of the locally finite pmp graphs which admit Borel a.e. one-ended spanning subforests.

Imaginaries in equicharacteristic zero henselian fields

2026-03-19T17:55:07Z

We classify the imaginaries in a large class of equicharacteristic zero henselian valued fields that contain all those with bounded inertia group, and more. To do so, we consider a mix of sorts introduced in earlier works of the two authors and prove elimination of imaginaries down to the field, the k-linear imaginaries and the imaginaries of the value group.

Foundational Analysis Of The Solvability Complexity Index: The Weihrauch-SCI Intermediate Hierarchy And A Koopman Operator Example

2026-03-19T14:24:40Z

The Solvability Complexity Index (SCI) provides an abstract notion of computing a target map $Ξ$ from finitely many oracle evaluations $Λ\subseteq \mathbb{C}$ via finite-height towers of pointwise limits. We first give a foundational analysis of what this extensional framework does and does not determine. We show that the SCI separation consistency is equivalent to a factorization of $Ξ$ through the full evaluation table, and we isolate the minimal logical role of $Λ$ as an information interface. To connect the SCI to Type-2 computability and Weihrauch reducibility, we give an effective enrichment for countable $Λ$ by viewing the evaluation table image $I_Λ\subseteq\mathbb{C}^{\mathbb{N}}$ as a represented space and factoring $Ξ$ as $\widehatΞ$. We then define the Weihrauch-SCI rank of a problem as the least number of iterated limit-oracles needed to compute it in the Weihrauch sense, i.e.\ the least $k$ such that $\widehatΞ\le_{W}\lim^{(k)}$, and prove well-posedness and representation invariance of this rank. A central negative result is that the unrestricted type-$G$ SCI model (arbitrary post-processing of finite oracle transcripts) is generally not comparable to Weihrauch/Type-2 complexity: finite-query factorizations collapse type-$G$ height, and analytic (non-Borel) decision problems yield examples with $\mathrm{SCI}_{G}=0$ but infinite Weihrauch-SCI rank. To recover a robust bridge, we introduce an intermediate SCI hierarchy by restricting the admissible base-level post-processing to regularity classes (continuous/Borel/Baire) and, optionally, to fixed-query versus adaptive-query policies. We prove that these restrictions form genuine hierarchies, and we establish comparison theorems showing what each restriction logically enforces (e.g.\ Borel towers compute only Borel targets; continuous-base towers yield finite Baire class).

On the Diophantine problem related to power circuits

2026-03-19T13:37:48Z

Myasnikov, Ushakov, and Won introduced power circuits in 2012 to construct a polynomial-time algorithm for the word problem in the Baumslag group, which has a non-elementary Dehn function. Power circuits are computational structures that support addition and the operation $(x,y) \mapsto x \cdot 2^y$ on integers. They also posed the question of decidability of the Diophantine problem over the structure $\langle \mathbb{N}_{>0}; +, x \cdot 2^y, \leq, 1 \rangle$, which is closely related to power circuits. In this paper, we prove that the Diophantine problem over this structure is undecidable.

Reverse Mathematics and Dimension of Posets

2026-03-19T11:11:32Z

Order dimension theory measures the complexity of partially ordered sets by quantifying how far they are from being linearly ordered. In this paper we study classical bounding results for order dimension within the framework of reverse mathematics. We focus on principles asserting that the dimension of a poset can be bounded in terms of the dimension of subposets obtained by removing chains or points, denoted by $\mathsf{DBi_n}$, $\mathsf{DBc_n}$, and $\mathsf{DB_p}$. We prove that, over $\mathsf{RCA}_0$, both $\mathsf{DBi_n}$ and $\mathsf{DBc_n}$ are equivalent to $\mathsf{WKL}_0$. To analyze $\mathsf{DB_p}$, we introduce a natural strengthening $\mathsf{DB^+_p}$ and show that both $\mathsf{DB_p}$ and $\mathsf{DB^+_p}$ are provable from $\mathsf{WKL}_0$ and from $\mathsf{I}Σ^0_2$, while $\mathsf{B}Σ^0_2$ does not suffice to prove $\mathsf{DB^+_p}$. The latter result is obtained by showing that the statement \lq\lq $\mathsf{DB^+_p}$ is computably true\rq\rq\ is equivalent to $\mathsf{I}Σ^0_2$.

The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification

2026-03-19T10:44:02Z

We formalize the orientation boundary for first-order step-duplicating recursors. At the schema, no measure in twelve formalized direct classes strictly orients the duplicating step uniformly. These classes include additive and transparent-compositional measures, affine and nonlinear scalar extensions, and tracked vector/pair families, together with a scalar-projection meta-theorem for the matrix side and a symbolic variable-condition barrier yielding a KBO-style impossibility corollary. To our knowledge, this is the first mechanized direct impossibility result for named termination-measure classes on a fixed terminating system. All internal proofs are formalized in Lean~4. The boundary is explanatory, not only negative: we prove an escape trichotomy for the explicit direct universe, a transparency-essentiality theorem with a concrete witness, a dependency-pair escape characterization, a generalized polynomial boundary theorem isolating failure of frozen base dominance, computable barrier-witness extractors, ablations, and SCC synchronization theorems, showing that successful methods cross the boundary only by importing structure outside the formalized direct classes. For the concrete witness calculus KO7, the guarded fragment is certified for strong normalization, confluence, a certified normalizer, decidable reachability to safe normal-form targets, an exact DM-component ordinal calibration at $ω^ω$, and a triple-lex certificate image below $ω^ω\cdot 2$. For full unguarded KO7, we prove root termination by a nonlinear polynomial witness and a KO7-specialized MPO, lift the nonlinear witness to context-closed strong normalization with an explicit derivation-length bound, expose executable classifier/witness/oracle tooling for direct-orientation attempts, and connect the Lean development to TTT2/CeTA through a checked TPDB export and verifier bridge.

Decidability of Quantum Modal Logic

2026-03-19T00:04:54Z

The decidability of a logical system refers to the existence of an algorithm that can determine whether any given formula in that system is a theorem. In this paper, Harrop's lemma is used to prove the decidability of quantum modal logic.

Hierarchies of direct powers, ultrapowers and cumulative powers

2026-03-18T21:24:10Z

In this paper we investigate cumulative hierarchies of functions on structures, or cumulative powers, and study their properties. Particularly, we show how they extend the preservation phenomena of reduced powers, direct powers and ultrapowers by offering a characterization of the fragment of first-order theory it preserves, and elucidate the connections between the three sorts of constructions. More precisely, we show how both direct powers and ultrapowers may be obtained from cumulative powers as quotients by appropriate equivalence relations. We address how embeddability lifts from generating structures to their cumulative powers, direct powers and ultrapowers, and under what conditions ultrapowers embed into corresponding cumulative powers or direct powers. We further offer an application of the framework to show a straightforward way of constructing Conway's surreal field.

Isometry groups of Polish ultrametric spaces

2026-03-18T20:09:27Z

We solve a long-standing open problem, formulated by Krasner in the 1950's, in the context of Polish (i.e. separable complete) ultrametric spaces by providing a characterization of their isometry groups using suitable forms of generalized wreath products of full permutation groups. Since our solution is developed in the finer context of topological (Polish) groups, it also solves a problem of Gao and Kechris from 2003. Furthermore, we provide an exact correspondence between the isometry groups of Polish ultrametric spaces belonging to some natural subclasses and various kinds of generalized wreath products proposed in the literature by Hall, Holland, and Malicki.

Constructive proofs for the standard translation of many-sorted to unsorted predicate logic

2026-03-18T19:02:20Z

It is well known that many-sorted logic can be reduced to unsorted first-order logic by adding predicates for each sort, relativizing quantifiers to these predicates, and adding appropriate axioms governing their behavior. Existing constructive proofs for the correctness of this translation break down when the many-sorted language includes equality and the unsorted target calculus includes the usual rules/axioms for equality. We give two constructive proofs. The first repairs a known gap in Herbrand's original proof for the equality-free case from his 1930 dissertation. This results in a proof that is conceptually simpler than the later proofs by Schmidt and Wang. The second proof establishes the same result, but also applies to languages with equality and can handle relation and function symbols that allow more than one combination of sorts in their argument places. Both proofs work for both classical and intuitionistic logic. As an application, we use the second proof to give a fully syntactic justification of van Dalen's translation of second-order logic into unsorted first-order logic.

A correspondence problem for mathematical proof

2026-03-18T18:50:10Z

Mathematical proofs are often said to justify their conclusions by indicating the existence of a corresponding formal derivation. We argue that this widespread view relies on an under-examined notion of correspondence, or what it means for a particular derivation to ''correspond'' to a particular proof. Mere existence of a formalization is not enough, and a substantive account of the required correspondence resolves into two criteria -- adequate representation (of the original theorem) and tracking (of the steps in the original proof). An examination of the actually-existing formalization systems we have today shows the variety of quasi-empirical ways we establish these criteria, and points towards new burdens that may be placed on the future evolution of mathematics itself.

Homogeneous forcing

2026-03-18T17:20:55Z

Assume $κ= κ^{< κ}$ (usually $\aleph_0$ or an inaccessible). We shall deal with iterated forcings preserving ${}^{κ>}{\rm Ord}$ and not collapsing cardinals along a linear order $L$. A sufficient condition for this, which we will focus on, is for the forcings to have support $<κ$ and the $κ^+$-cc, and be strategically $<κ$-complete. The aim is to have homogeneous forcings, so that the iteration has many automorphisms. In addition to the inherent interest, such iterations are helpful for considering some natural ideals on ${}^\kappa2$, in order to get a model of ${\rm ZF} + {\rm DC}_κ +$ ``modulo this ideal, every set is equivalent to a $κ$-Borel one." But here we only have many automorphisms of the index set $L$ and therefore of the iteration of iterands $\mathbb{Q} $; we do not necessarily have homogeneity of $\mathbb{Q} $, and we do not have automorphisms mapping other names of $\mathbb{Q} $-reals onto each other. %\notemgrimes{What are the other names? Where do they come from?} However, for some reasonable forcing notions, there are no other $\mathbb{Q} $-reals! This was the reason for introducing and investigating saccharinity in earlier works with Jakob Kellner and with Haim Horowitz.

Measuring the Complexity of Countable Presburger Models

2026-03-18T15:46:28Z

We take two approaches to classifying the complexity of Presburger models: Scott analysis and degree spectra. In particular, we investigate the possible Scott sentence complexities and possible degree spectra of models of Presburger arithmetic. Many of our results will be achieved by showing how given a linear order $\mathcal{L}$, we can construct a Presburger group $P_\mathcal{L}$ that maintains much of the structure of $\mathcal{L}$.

More on modal logics and deduction

2026-03-18T13:43:15Z

We study the relation between additivity and deduction theorems in the algebraic semantics of congruential modal logic. Additivity of the modal operator is well-known to imply the local deduction-detachment theorem. Our main theme is that deduction properties of modal logic persist far beyond the additive setting. We introduce the notion of a strongly non-additive variety, and then we prove that there are continuum many strongly non-additive minimal discriminator varieties of Boolean frames; equivalently, continuum many strongly non-additive maximal congruential modal logics with deduction-detachment theorem. Moreover, every normal modal logic can be transformed, in an injective way, into a strongly non-additive one while preserving the (local) deduction theorem. Finally, we show that neither the class of congruential modal logics with the local deduction theorem nor its complement is elementary.

Calligraphy Concerning Casually Compiled Cardinal Characteristic Comparisons

2026-03-18T10:32:58Z

The paper establishes several inequalities between cardinal characteristics of the continuum. In particular, it is shown that the partition splitting number is not larger than the uniformity of the meagre ideal; not all sets of reals having the cardinality of an the $\varepsilon$-almost bisecting number are of strong measure zero; no fewer sets of strong measure zero than indicated by the statistically reaping number suffice to cover the reals; the pair-splitting number is not smaller than the evasion number; and the subseries number is neither smaller than the pair-splitting number nor than the minimum of the unbounding number and the unbisecting number. Moreover, a diagram putting these results into context is provided and a brief historical account is given.