Proof by Mechanization: Cubic Diophantine Equation Satisfiability is $Σ^0_1$-Complete

2026-03-06T00:32:07Z

We prove that satisfiability of a single Diophantine equation of total degree $\le 3$ over $\mathbb{N}$, with the number of variables encoded in the input instance, is $Σ^0_1$-complete and hence undecidable. Concretely, we give a uniform primitive recursive compiler mapping arithmetic sentence codes to cubic Diophantine constraint systems such that provability in $\mathrm{I}Δ_0+\mathrm{B}Σ_1$ (restricted to $\mathcal{L}_{\mathsf{RA}}$) is equivalent to solvability of the emitted constraints. Degree control is local: all syntactic checks and inference verification compile to equations of degree $\le 2$, and the only degree-$3$ terms occur when a linear selector activates a quadratic obligation. The resulting finite system is then collapsed to a single cubic equation by a degree-preserving aggregation construction. We further internalize the compiler into a fixed four-instruction register kernel with bounded deterministic trace unrolling and a two-level aggregation layout, yielding a single explicit universal cubic polynomial in a fixed number of variables. The concrete coefficient table and a kernel-checked degree certificate are mechanized in $\textsf{Rocq}$; the semantic bridge relating arithmetic theoremhood to solvability of the pinned polynomial is proved in a separate layer without normalizing the coefficient table. Undecidability follows by diagonalization.

Constraint satisfaction problems, compactness and non-measurable sets

2026-03-06T00:11:49Z

A finite relational structure A is called compact if for any infinite relational structure B of the same type, the existence of a homomorphism from B to A is equivalent to the existence of homomorphisms from all finite substructures of B to A. We show that if A has width one, then the compactness of A can be proved in the axiom system of Zermelo and Fraenkel, but otherwise, the compactness of A implies the existence of non-measurable sets in 3-space.

Independence questions in a finite axiom-schematization of first-order logic

2026-03-06T00:00:35Z

We review some independence results in a finite axiom-schematization of classical first-order logic introduced by Norman Megill. We also prove that a certain axiom scheme of this system is independent although all of its instances are provable from the other axiom schemes.

Corrigendum & Addendum to "Categoricity-like Properties in the First Order Realm"

2026-03-05T20:02:16Z

This note complements our paper "Categoricity-like properties in the first order realm" (Journal for the Philosophy of Mathematics, 2024).

On actions and split extensions in varieties of hoops: the case of strong section

2026-03-05T19:38:12Z

The aim of this article is to investigate internal actions and split extensions in the variety of hoops. We provide a characterization of split extensions with strong section in terms of strong external actions. Beyond the general setting of hoops, the study is extended to the subvarieties of basic hoops, Wajsberg hoops, Gödel hoops and product hoops. Within the setting of basic hoops and their bounded counterparts, BL-algebras, the double negation yields a significant example of split extension with strong section, thus motivating our approach. A connection between strong external actions of hoops and the semidirect product construction introduced by W. Rump in the cateogory of L-algebras is established.

Capturing dual team properties with inclusion atoms

2026-03-05T18:59:24Z

We introduce propositional team-based logics expressively complete for (quasi) downward and (quasi) upward closed properties in a syntactically dual way, by using variants of the inclusion atom. In particular, the variants of the primitive inclusion atoms used in the (quasi) upward closed setting have equivalent formulas using variants of the might modality. The duality is visible in the logics' normal forms, mirroring the duality between the (quasi) upward and downward closed settings, where the quasi variants take special care of the empty and full team. Furthermore, we defined sound and complete natural deduction systems for each logic.

$T$-convexity, Weakly Immediate Types, and $T$-$λ$-Spherical Completions of o-minimal Structures

2026-03-05T15:51:51Z

It is well known that ordered exponential fields with a compatible non-trivial valuation cannot be spherically complete, but there are some that are ``complete enough''. This paper gives analogues of Kaplansky's theorem on maximally valued fields that hold for a suitable class of elementary extensions of some ordered exponential fields with a compatible valuation. More precisely it does so for models of any theory $T_{\text{convex}}$ given by the expansion of a fixed complete o-minimal theory of ordered fields $T$, by a predicate $\mathcal{O}$ for a non-trivial $T$-convex valuation ring. For $λ$ an uncountable cardinal, say that a unary type $p(x)$ over a model of $T_{\text{convex}}$ is \emph{$λ$-bounded weakly immediate} if its cut is defined by an empty intersection of fewer than $λ$ many nested valuation balls. Call an elementary extension \emph{$λ$-bounded wim-constructible} if it is obtained as a transfinite composition of extensions each generated by one element whose type is $λ$-bounded weakly immediate. I show that $λ$-bounded wim-constructible extensions do not extend the residue-field sort and that any two wim-constructible extensions can be amalgamated in an extension which is again $λ$-bounded wim-constructible over both. A consequence of this is that given an uncountable cardinal $λ$, every model of $T_{\text{convex}}$ has a unique-up-to-isomorphism $λ$-spherically complete $λ$-bounded wim-constructible extension providing an analogue of Kaplansky's theorem. I call this extension the $T$-$λ$-spherical completion. Another consequence is that $T_{\mathrm{convex}}$ is \emph{definably spherically complete}. When $T$ is power bounded wim-constructible extensions are just the immediate extensions. I discuss the example of power bounded theories expanded by $\exp$ (\emph{simply exponential} theories).

The Complexity of the Constructive Master Modality

2026-03-05T12:59:47Z

We introduce the semantically-defined constructive master-modality logics $\sf CK^*$ and $\sf WK^*$, extending the basic constructive modal logic $\sf CK$ and the Wijesekera-style logic $\sf WK$ obtained by impossing infallibility. Using translations between our logics and fragments of $\sf PDL$, we show that both $\sf CK^*$ and $\sf WK^*$ are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celoni, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed $\sf CS4$ and $\sf WS4$ into the master-modality logics, showing that their validity problems are in EXPTIME.

Modal Fragments

2026-03-05T11:07:28Z

We survey systematic approaches to basis-restricted fragments of propositional logic and modal logics, with an emphasis on how expressive power and computational complexity depend on the allowed operators. The propositional case is well-established and serves as a conceptual template: Post's lattice organizes fragments via Boolean clones and supports complexity classifications for standard reasoning tasks. For modal fragments, we then bring together two historically independent lines of investigation: a general framework where modal fragments are parameterized by a basis of "connectives" defined by arbitrary modal formulas (initially proposed and studied by logicians such as Kuznetsov and Ratsa in the 1970s), and the more tractable class of what we call simple modal fragments parameterized by Boolean functions plus selected modal operators, where Post-lattice methods enable systematic decidability and dichotomy results. Along the way, we collect and extend results on teachability and exact learnability from examples for both propositional fragments and simple modal fragments, and we conclude by identifying several open problems.

More on setwise climbability properties

2026-03-05T08:04:29Z

We introduce two types of variations of setwise climbability properties, which have been introduced by the second author as fragments of Jensen's square principles. We show that variations of the first type are equivalent to known principles and that they are consistent with the Proper Forcing Axiom(PFA). On the other hand, those of the second type can be characterized as Martin-type axioms for some classes of posets defined in terms of a new variation of generalized Banach-Mazur games, and they are no longer consistent with PFA. We also study how large fragments of PFA are consistent with these principles.

The Conjugacy Relation on One-sided Subshifts is Non-treeable

2026-03-05T03:46:41Z

In this paper we study the conjugacy relation on one-sided subshifts in the viewpoint of descriptive set theory. We show the conjugacy relation on one sided subshifts with the alphabet set $\{0,1\}$ is non-treeable and non-amenable.

On regulated partitions

2026-03-05T00:14:46Z

This paper considers the combinatorics of continuous and Borel rectangular partitions of free actions of $\mathbb{Z}^n$ on $0$-dimensional Polish spaces, specifically the free part $F(2^{\mathbb{Z}^n})$ of the shift action of $\mathbb{Z}^n$ on the space $2^{\mathbb{Z}^n}$. This is done through the study of a corresponding notion of regulated partitions of $\mathbb{R}^n$. The main concepts studied are the continuous and Borel {\em regulation} numbers of the partition. This is defined as the maximum number of rectangles in the corresponding regulated partition that can intersect in a point. The continuous and Borel regulation numbers $γ_c$, $γ_B$ are the minimum possible values of these numbers as we range over continuous (respectively Borel) rectangular partitions of $F(2^{\mathbb{Z}^n})$. It is shown that for $n=2$ that $γ_c=γ_B=3$, and for $n \geq 3$ that $n+2\leq γ_B \leq γ_c \leq 3\cdot 2^{n-2}$. For $n=3$ we improve this to $γ_c=γ_B=5$. This shows a striking difference between the Borel combinatorics of dimension $n=2$ and dimensions $n>2$.

Escaping Tennenbaum's Theorem and a Strong Jump Inversion Theorem

2026-03-04T20:56:02Z

Tennenbaum's theorem states that PA does not admit any nonstandard computable model. In 2022, Pakhomov proved that this theorem is fragile in regards to how PA is expressed, by constructing a theory that is definitionally equivalent to PA (roughly: "it's PA but with a different choice of signature") for which there is a computable nonstandard model. He showed that this fragility does not extend to true arithmetic (any nonstandard model of a theory definitionally equivalent to $\mathrm{Th}(\mathbb{N})$ is not computable), but the question of whether this fragility extends to fragments of PA of intermediate strength was left open. We show that it does, by constructing a sequence of theories $T^n$ which are definitionally equivalent to: "PA plus all $Π^0_n$ truths", all of which admit computable nonstandard models. In the process, we produce a general-purpose theorem for strong jump inversion. Besides applying this theorem to obtain our novel result, we show that several known results from the literature can be seen as direct applications of our theorem.

No universal group in a cardinal

2026-03-04T17:22:26Z

For many classes of models, there are universal members in any cardinal $λ$ which "essentially satisfies GCH", i.e. $λ= 2^{< λ}$, in particular for the class of a complete first order $T$ (well, if at least $λ> |T|$). But if the class is "complicated enough", e.g. the class of linear orders, we know that if $λ$ is "regular and not so close to satisfying GCH" then there is no universal member. Here we find new sufficient conditions (which we call the olive property), not covered by earlier cases (i.e. fail the so-called SOP$_4$). The advantage of those conditions is witnessed by proving that the class of groups satisfies one of those conditions.

The Construction Principle and superstability of free objects in varieties of algebras

2026-03-04T13:43:27Z

We investigate the relationship between the Eklof-Mekler-Shelah Construction Principle for a variety of algebras $\mathbf{V}$ and the question of superstability of the free objects in $\mathbf{V}$, denoted as $\mathcal{F}_\mathbf{V}$. We consider this question in the general setting of AEC-coverings of $\mathcal{F}_\mathbf{V}$, with applications to first-order logic and beyond. Our main result is that if a strong form of the Construction Principle is satisfied, then almost all AEC-covering of $\mathcal{F}_\mathbf{V}$ are unsuperstable. Concrete applications to $R$-modules and varieties of groups are also considered.