A new ultrafilter proof of Van der Waerden's theorem

2026-03-04T13:23:54Z

We present a new short proof of Van der Waerden's Theorem about the existence of arbitrarily long monochromatic arithmetic progressions. The proof uses algebra in the compact space of ultrafilters $β\N$, but contrarily to the other existing proofs, neither minimal nor idempotent ultrafilters are involved.

Non-Derivability Results in Polymorphic Dependent Type Theory

2026-03-04T12:51:39Z

In the pure Calculus of Constructions (CC) one can define data types and function over these, and there is a powerful higher order logic to reason over these functions and data types. This is due to the combination of impredicativity and dependent types, and most of these features can already be observed in polymorphic (second order) dependent type theory $λ$P2. The impredicative encoding of data types (in $λ$P2 or CC) is powerful but not fully satisfactory: for example, the induction principle is not provable. As a matter of fact, it can be shown that induction is not provable for whatever possible representation of data types. In a recent paper, Awodey, Frey and Speight show that in an extension of $λ$P2 with Sigma-types, identity types with uniqueness of identity proofs and function extensionality, it is possible to define data types for which the induction principle is provable. More recently it has been shown that in this extension of $λ$P2, also quotient types can be defined with the proper induction principle, and, using quotient types, coinductive types can be defined with the proper coinduction principle. This leaves various questions open: Are quotient types with induction principle not definable in the original $λ$P2? And how about coinductive types, is it impossible to get a strong coinduction principle in $λ$P2? Looking at it from the other side: which of the extensions used are really needed to make induction and coinduction work? In this paper, we contribute partial answers to these questions: parametric quotient types are not definable in $λ$P2 and the well-known definable stream type does not have a coinduction principle. For the latter question we show that, if we just extend $λ$P2 with Sigma-types and identity types with uniqueness of identity proofs, we still cannot prove an induction principle for the natural numbers. So function extensionality is crucial in making induction provable. We show these results by studying models of $λ$P2 where the types representing these principles are empty, so these models act as counter models to the derivability of the principles.

Robinson Splitting Theorem and $Σ_1$ Induction

2026-03-04T12:37:17Z

The Robinson Splitting Theorem states that a c.e. degree $\mathbf{b}$ splits over any low c.e. degree $\mathbf{c}<\mathbf{b}$. We prove that a weaker version of this theorem holds in models of $\mathrm{P}^-+\mathrm{I}Σ_1$, with lowness replaced by superlowness.

Parameterized D-torsors in differential Galois theory

2026-03-04T02:27:14Z

In the context of differential fields of characteristic zero with several commuting derivations, we discuss the notion of $\#$-differential equations on parameterized D-torsors and their associated Galois extensions. Using model-theoretic methods, we observe that any generalized strongly normal extension (in the sense of Pillay [14] and, more generally, León Sánchez [9]) is the Galois extension of a parameterized D-torsor. Furthermore, we prove a parameterized version of a theorem of Kolchin on differential cohomology, itself of independent interest, and use it to provide a necessary and sufficient cohomological condition for when a generalized strongly normal extension is the Galois extension for a log-differential equation on its Galois group (as a parameterized D-group). We also present general model-theoretic versions of some of the main results.

Rank and Independence of Imaginaries in Proper Pairs of ACF

2026-03-03T20:55:06Z

Let $T_P$ be the theory of beautiful pairs of algebraically closed fields of fixed characteristic. It is known that for real tuples in models of $T_P$, SU-rank coincides with Morley rank and can be computed effectively. Building on Pillay's geometric description (2007) of imaginaries in $T_P$, we define an additive rank on imaginaries of $T_P$, called the geometric rank. It takes values in $ω*\mathbb N + \mathbb Z$ and coincides with SU-rank on real tuples. It refines SU-rank and characterizes forking in $T_P^{\mathrm{eq}}$, from which we derive an explicit criterion for determining forking independence.

On an ordinary expansion of first-order Belnap-Dunn logic

2026-03-03T16:29:42Z

This paper concerns an expansion of first-order Belnap-Dunn logic whose connectives and quantifiers all have a counterpart in classical logic. The language and logical consequence relation of this paradefinite logic are defined, a sequent calculus proof system for this logic is presented, and the soundness and completeness of this proof system is established. It is shown that the defined logic distinguishes itself from the many other paradefinite logics that are usually considered equally classical by the classical laws of logical equivalence that hold for it. It is further argued that the defined logic is the most natural paradefinite logic relative to the version of classical logic with the same language. Moreover, a simple embedding of the defined logic in that version of classical logic is presented and the potential of the logic for dealing with inconsistencies and incompletenesses in inductive machine learning is discussed.

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation

2026-03-03T15:26:26Z

Craig's Interpolation theorem has a wide range of applications, from mathematical logic to computer science. Proof-theoretic techniques for establishing interpolation usually follow a method first introduced by Maehara for the Sequent Calculus and then adapted by Prawitz to Natural Deduction. The result can be strengthened to a proof-relevant version, taking proof terms into account: this was first established by Čubrić in the simply-typed lambda-calculus with sums and more recently in linear, classical and intuitionistic sequent calculi. We give a new proof of Čubrić's proof-relevant interpolation theorem by building on principles of bidirectional typing, and formalise it in Rocq.

Inner models from extended logics and the Delta-operation

2026-03-03T12:04:10Z

If $\mathcal{L}$ is an abstract logic (a.k.a. model theoretic logic), we can define the inner model $C(\mathcal{L})$ by replacing first order logic with $\mathcal{L}$ in Gödel's definition of the inner model $L$ of constructible sets. Set theoretic properties of such inner models $C(\mathcal{L})$ have been investigated recently and a spectrum of new inner models is emerging between $L$ and $\mathrm{HOD}$. The topic of this paper is the effect on $C(\mathcal{L})$ of a slight modification of $\mathcal{L}$ i.e. how sensitive is $C(\mathcal{L})$ on the exact definition of $\mathcal{L}$? The $Δ$-extension $Δ(\mathcal{L})$ of a logic is generally considered a "mild" extension of $\mathcal{L}$. We give examples of logics $\mathcal{L}$ for which the inner model $C(\mathcal{L})$ is consistently strictly smaller than the inner model $C(Δ(\mathcal{L}))$, and in one case we show this follows from the existence of $0^{\sharp}$.

A Variant Of Chaitin's Omega function

2026-03-03T10:21:32Z

We investigate the continuous function $f$ defined by $$x\mapsto \sum_{σ\le_L x }2^{-K(σ)}$$ as a variant of Chaitin's Omega from the perspective of analysis, computability, and algorithmic randomness. Among other results, we obtain that: (i) $f$ is differentiable precisely at density random points; (ii) $f(x)$ is $x$-random if and only if $x$ is weakly low for $K$ (low for $Ω$); (iii) the range of $f$ is a null, nowhere dense, perfect $Π^0_1(\emptyset')$ class with Hausdorff dimension $1$; (iv) $f(x)\oplus x\ge_T\emptyset'$ for all $x$; (v) there are $2^{\aleph_0}$ many $x$ such that $f(x)$ is not 1-random; (vi) $f$ is not Turing invariant but is Turing invariant on the ideal of $K$-trivial reals. We also discuss the connection between $f$ and other variants of Omega.

Serre depth and local cohomology

2026-03-03T08:04:20Z

We introduce a fundamental homological invariant, called Serre depth, which stratifies Serre's conditions in the same way that depth stratifies the Cohen-Macaulay property. We study the Serre depths of modules over arbitrary Noetherian local rings and over standard graded algebras over a field, extending the polynomial ring case due to Muta and Terai. Under mild hypotheses, we show that the $r$-th Serre depth of a finitely generated module $M$ measures the deviation of $M$ from satisfying Serre's condition $(S_r)$. The main results of the paper can be summarized as follows: (i) We establish the basic properties of Serre depth and prove that it is invariant under completion. (ii) If the base ring $R$ is a homomorphic image of a Gorenstein ring, we show that a finitely generated $R$-module $M$ is equidimensional and satisfies $(S_r)$ if and only if its $r$-th Serre depth equals its Krull dimension. Analogous statements are obtained for schemes. (iii) For a homogeneous ideal in a standard graded polynomial ring over a field, we compare its Serre depths with those of its initial ideal. (iv) We characterize the Serre depths of a monomial ideal in terms of its skeletons and prove that the Serre depths of sufficiently large powers of a monomial ideal stabilize; the proof uses Presburger arithmetic.

Finite approximation of free groups II: the Theorems of Ash, Herwig-Lascar and Ribes-Zalesskii -- revisited and strengthened

2026-03-03T07:13:13Z

Relations and interactions between the theorems of Ash, Herwig--Lascar and Ribes--Zalesskii are discussed and it is shown that these three theorems are equivalent in the sense that each of them can be derived from each other one. Some strengthenings of these theorems are obtained with the use of groups provided by a construction of the third author. Evidence is given that these strengthenings are substantially stronger than the classical results. Yet, it turns out that both kinds of results can be interpreted as different instances of the same common scheme, namely as \emph{finite approximation of free groups}.

E-variables and tests of randomness for distribution classes

2026-03-03T00:49:29Z

E-variables are a relatively new approach for testing statistical hypotheses that has been experiencing major development during the last several years. In this paper we introduce the method of e-variable-approximability and use it to develop a general approximation technique allowing us to construct e-variables for popular distribution classes important for applications. E-variables were originally based on a concept of Levin's (average-bounded) randomness tests from Algorithmic Information Theory. We show that our construction of e-variables can be used to provide an explicit construction for a randomness test with respect to a class of distributions.

The barrier Ramsey theorem

2026-03-02T18:31:41Z

In this paper we study a very general finite Ramsey theorem, where both the sets being colored and the homogeneous set must satisfy some largeness notion. For the homogeneous set this has already been done using the notion of $α$-largeness, where $α$ is a countable ordinal equipped with a system of fundamental sequences. To extend this approach the more appropriate notion is barrier largeness. Since the complexity of barriers can be measured by countable ordinals, we define Ramsey ordinals and, using appropriate iterations of the Veblen functions, we are able to compute them.

Possible and impossible conditionals for team logics

2026-03-02T17:56:52Z

We study whether a logic based on team semantics can be enriched with a conditional satisfying minimal requirements--namely, preservation of the closure property of the logic, Modus Ponens, and the Deduction Theorem. We show that such well-behaved conditionals exist for downward or upward closed logics, but do not typically exist for union closed, convex or intersection closed logics. We also briefly investigate conditionals satisfying weaker requirements.

Prime Factorization in Models of PV$_1$

2026-03-02T17:20:24Z

Assuming that no family of polynomial-size Boolean circuits can factorize a constant fraction of all products of two $n$-bit primes, we show that the bounded arithmetic theory $\text{PV}_1$, even when augmented by the sharply bounded choice scheme $BB(Σ^b_0)$, cannot prove that every number has some prime divisor. By the completeness theorem, it follows that under this assumption there is a model $M$ of $\text{PV}_1$ that contains a nonstandard number $m$ which has no prime factorization.