https://arxiv.org/api/EyUkKT8/nUaadBRvDDBriCt5jBI2026-04-04T15:26:09Z1533733015http://arxiv.org/abs/2405.06961v3Dimensionality and randomness2026-02-17T19:04:56ZArranging the bits of a random string or real into k columns of a two-dimensional array or higher dimensional structure is typically accompanied with loss in the Kolmogorov complexity of the columns, which depends on k. We quantify and characterize this phenomenon for arrays and trees and its relationship to negligible classes.2024-05-11T09:12:45ZGeorge BarmpaliasXiaoyan Zhanghttp://arxiv.org/abs/2602.15812v1Separable C*-algebras Without the Countable Axiom of Choice2026-02-17T18:49:36ZThe goal of this paper is twofold. In addition to the results stated in the next paragraph, we present some classical results on absoluteness relevant to functional analysis that are well known to logicians but not nearly as well advertised as they should be. We show that the theory of separable C*-algebras can be developed in ZF (that is, without using any Choice). This includes proving the Gelfand-Naimark representation theorems as well as the Spectral Mapping Theorem for polynomials and developing continuous functional calculus for commuting normal elements. Some of our proofs are modifications of the standard ones, obtained by avoiding the use of Choice. Some other proofs require new ideas in order to avoid the use of Choice. Yet another batch of proofs proceeds by using the set-theoretic Shoenfield Absoluteness Theorem. This result (well known to logicians but regrettably not as well advertised as it deserves) implies that statements about standard Borel spaces of low quantifier complexity that are provable in ZFC, or even ZFC together with the Continuum Hypothesis are provable in ZF. One of the main objectives of this paper is to present these results in a convenient form that can be utilized by analysts not familiar with set theory. We also show that in the absence of Choice (more precisely, assuming the existence of a Russell set) there is a concretely representable unital commutative \cstar-algebra that is not isomorphic to C(X) for any compact Hausdorff space X. Finally, from the model-theoretic point of view, while the property of having a tracial state is provably axiomatizable in ZFC, it is not provably axiomatizable in ZF+DC.2026-02-17T18:49:36Z30 pages, comments welcomeBruce BlackadarIlijas Farahhttp://arxiv.org/abs/2602.06877v2Non-computability of $K$-theory for computably presented C*-algebras2026-02-17T18:20:08ZWe give an example of a unital C*-algebra $\mathbf{A}$ with a computable presentation and for which neither $K_0(\mathbf{A})$ nor $K_1(\mathbf{A})$ has a computable presentation.2026-02-06T17:02:56ZSecond draft; the question left open at the end of the previous version has now been solved. 6 pages; comments welcome!Christopher J. EagleIsaac GoldbringTimothy H. McNichollRussell Millerhttp://arxiv.org/abs/2504.03460v4Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives2026-02-17T15:41:57ZThis article revisits standard theorems from elementary number theory from a constructive, algorithmic, and proof-theoretic perspective, framed within the theory of computable functionals TCF. Key examples include Bézout's identity, the fundamental theorem of arithmetic, and Fermat's factorisation method. All definitions and theorems are fully formalised in the proof assistant Minlog, laying the foundation for a comprehensive formal framework for number theory within Minlog.
While formalisation guarantees correctness, the primary emphasis is on the computational content of proofs. Leveraging Minlog's built-in program extraction, we obtain executable terms and export them as Haskell code.
The efficiency of the extracted programs plays a central role. We show how performance considerations influence even the original formulation of theorems and proofs. In particular, we compare formalisations based on binary encodings of natural numbers with those using the traditional unary (successor-based) representation.
We present several core proofs in detail and reflect on the challenges that arise from formalisation in contrast to informal reasoning. The complete formalisation is available online and linked throughout. Minlog's tactic scripts are designed to follow the structure of natural-language proofs, allowing each derivation step to be traced precisely and thereby bridging the gap between formal and classical mathematical reasoning.2025-04-04T14:10:00Z56 pages, 6 figuresFranziskus Wiesnethttp://arxiv.org/abs/2602.15542v1Homeomorphisms between compact subsets of real numbers2026-02-17T12:48:32ZA reduction of properties (invariants) of compact sets of real numbers to properties of countable orders is presented here. Discussed here is also an embedding property of some compact sets that are called t$\mathbb R$-sets. Among others, it is proved that there are exactly $ω_1$ many non-homeomorphic t$\mathbb R$-sets.2026-02-17T12:48:32ZComments are welcomeSławomir KusińskiSzymon Plewikhttp://arxiv.org/abs/2602.15221v1Irreducible distinguishing colourings and the Axiom of Choice2026-02-16T22:05:14ZWe say that a vertex or edge colouring of a graph is distinguishing if the only automorphism that preserves this colouring is the identity. A (proper) distinguishing colouring is irreducible if there is no possibility of merging two non-empty classes of colours to obtain a (proper) distinguishing colouring. We show that every graph has an irreducible (proper) distinguishing vertex colouring and that every graph without isolated edge and with at most one isolated vertex has an irreducible (proper) distinguishing edge colouring. Moreover, we show that the existence of any of these colourings for every connected graph (not isomorphic to $K_2$) is equivalent to the Axiom of Choice.2026-02-16T22:05:14ZMarcin Stawiskihttp://arxiv.org/abs/2509.02766v5Reduction Complexities in Set Theory2026-02-16T20:55:09ZIn \cite{Ca2016} and \cite{Ca2018}, we introduced a notion of effective reducibility between set-theoretical $Π_{2}$-statements; in \cite{Ca2025}, this was extended to statements of arbitrary (potentially even infinite) quantifier complexity. We also considered a corresponding notion of Weihrauch reducibility, which allows only one call to the effectivizer of $ψ$ in a reduction of $φ$ to $ψ$. In this paper, we obtain a considerably refined analysis through interpolating between these two notions: Namely, we ask how many calls to an effectivizer for $ψ$ are required for effectivizing $φ$. This allows us to make formally precise questions such as ``how many ordinals does one need to check for being cardinals in order to compute the cardinality of a given ordinal?'' and (partially) answer many of them. Many of these anwers turn out to be independent of ZFC.2025-09-02T19:13:19ZMerlin Carlhttp://arxiv.org/abs/2602.02211v2The Cofinality of Generating Familes2026-02-16T20:15:10ZThe topology of a separable metrizable space $M$ is \emph{generated} by a family $\mathcal{C}$ of its subsets provided that a set $A\subseteq M$ is closed in $M$ if and only if $A\cap C$ is closed in $C$ for each $C\in \mathcal{C}$. The \emph{sequentiality number}, $\mathop{seq}(M)$, and \emph{$k$-ness number}, $\mathop{k}(M)$, of $M$, are the minimum size of a generating family of convergent sequences, respectively compact subsets.
Let $\mathfrak{b}$ be the minimum size of an unbounded set in $ω^ω$ with the mod finite order. For a cardinal $κ$, the \emph{covering number}, $\mathop{cov}(κ)$, is the minimum size of a family of countable subsets of $κ$ so that every countable subset of $κ$ is contained in an element of the family. It is shown using the Tukey order on relations that (1) $\mathop{seq}(M)=\mathop{cov}(|M|)\cdot \mathfrak{b}$, unless $M$ is locally small (every point of $M$ has a neighborhood of size strictly less than $|M|$) in which case $\mathop{seq}(M)=\lim_{μ<|M|} \mathop{cov}(μ)\cdot \mathfrak{b}$ and (2) $k(M)$ is in the interval $[kc(M)\cdot\mathfrak{b},\mathop{cov}(kc(M))\cdot \mathfrak{b}]$, where $kc(M)$ is the minimum number of compact sets that cover $M$.
Solutions to problems of van Douwen's on the $k$-ness number of analytic and of co-analytic spaces are deduced.2026-02-02T15:17:43ZThanks to Will Brian for his input on an earlier draftPaul GartsideThomas Giltonhttp://arxiv.org/abs/2602.15158v1da Costa and Tarski meet Goguen and Carnap: a novel approach for ontological heterogeneity based on consequence systems2026-02-16T19:58:35ZThis paper presents a novel approach for ontological heterogeneity that draws heavily from Carnapian-Goguenism, as presented by Kutz, Mossakowski and Lücke (2010). The approach is provisionally designated da Costian-Tarskianism, named after da Costa's Principle of Tolerance in Mathematics and after Alfred Tarski's work on the concept of a consequence operator. The approach is based on the machinery of consequence systems, as developed by Carnielli et al. (2008) and Citkin and Muravitsky (2022), and it introduces the idea of an extended consequence system, which is a consequence system extended with ontological axioms. The paper also defines the concept of an extended development graph, which is a graph structure that allows ontologies to be related via morphisms of extended consequence systems, and additionally via other operations such as fibring and splitting. Finally, we discuss the implications of this approach for the field of applied ontology and suggest directions for future research.2026-02-16T19:58:35Z22 pages, 5 figures, 1 tableGabriel Rochahttp://arxiv.org/abs/2602.15081v1Corrigendum & Addendum to: Variations on a Visserian theme2026-02-16T10:27:15ZWe revisit the proof of solidity of KM (Kelley-Morse theory of classes), as presented in the 2016 paper "Variations on a Visserian theme", so as to indicate the role of the scheme of class collection in the proof.2026-02-16T10:27:15Z7 pages; corrigendum and addendum to arXiv:1702.07093Ali Enayathttp://arxiv.org/abs/2304.05477v3Categorical structure in coherent theory of arithmetic2026-02-16T09:13:48ZIn this paper we provide a semantic and syntactic analysis of parametrised natural numbers object in coherent categories, or pr-coherent categories. Semantically, we show the definable functions in the initial pr-coherent category are exactly given by primitive recursive functions. We also show that any pr-coherent category supports the construction of bounded universal quantifications, which are absent in an arbitrary coherent category. Under these semantic consideration, we construct a coherent theory of arithmetic and we show its syntactic category is equivalent to the initial pr-coherent category. From a logical perspective, we also show that this theory can be identified as the Σ1-fragment of IΣ1. Thus as an application, we provide a structural proof of the classical result in proof theory that the strongly Σ1-representable functions in IΣ1 are exactly primitive recursive functions.2023-04-11T20:11:27ZTo appear in "Theoretical Computer Science"Lingyuan Yehttp://arxiv.org/abs/2112.00651v4Beautiful pairs2026-02-16T07:23:08ZWe introduce an abstract framework to study certain classes of stably embedded pairs of models of a complete $\mathcal{L}$-theory $T$, called \textit{beautiful pairs}, which comprises Poizat's belles paires of stable structures and van den Dries-Lewenberg's tame pairs of o-minimal structures. Using an amalgamation construction, we relate several properties of beautiful pairs with properties analogous to properties in Fraïssé classes.
After characterizing beautiful pairs of various theories of ordered abelian groups and valued fields, including the theories of algebraically closed, $p$-adically closed and real closed valued fields, we show an Ax-Kochen-Ershov type result for beautiful pairs of henselian valued fields. As an application, we derive strict pro-definability of particular classes of definable types. When $T$ is one of the theories of valued fields mentioned above, the corresponding classes of types are related to classical geometric spaces and our main result specializes to their strict pro-definability. Most notably, we exhibit the strict pro-definability of a natural space of types associated to Huber's analytification. In this way, we also recover a result of Hrushovski-Loeser on the strict pro-definability of stably dominated types in algebraically closed valued fields, which corresponds to Berkovich's analytification.2021-12-01T16:57:12Z44 pagesPablo Cubides KovacsicsMartin HilsJinhe Yehttp://arxiv.org/abs/2004.00174v2On a question of Slaman and Steel2026-02-16T06:46:17ZWe consider an old question of Slaman and Steel: whether Turing equivalence is an increasing union of Borel equivalence relations none of which contain a uniformly computable infinite sequence. We show this question is deeply connected to problems surrounding Martin's conjecture, and also in countable Borel equivalence relations. In particular, if Slaman and Steel's question has a positive answer, it implies there is a universal countable Borel equivalence which is not uniformly universal, and that there is a $(\equiv_T,\equiv_m)$-invariant function which is not uniformly invariant on any pointed perfect set.2020-04-01T00:15:00ZAdam DayAndrew Markshttp://arxiv.org/abs/2602.14373v1Square-bracket operations clubs2026-02-16T00:49:51ZThis paper continues the investigation of the three square-bracket operations $[\cdot\cdot]$ from chapter 5 of \cite{Walks}. \ We say that a square-bracket operation $[\cdot\cdot]$ has the \emph{Ramsey club property} if for every club $C\subseteqω_{1}$, there is an uncountable subset $W$ $\subseteq ω_{1}$ such that $\left[ αβ\right] \in C$ for every $α,β\in W.$ \ The second author proved that the Proper Forcing Axiom\textsf{ }implies that all the square-bracket operations induced by Aronszajn trees have this property. We extend this result to the other two classes. We conclude that each of the statements \textquotedblleft all square-bracket operations have the Ramsey club property\textquotedblright\ and \textquotedblleft No square-bracket operation has the Ramsey club property\textquotedblright\ are consistent with \textsf{ZFC. }In other words, \textsf{ZFC }is unable to decide the status of the Ramsey club property for any square-bracket operation. Furthermore, we analyze the status of the Ramsey club property for square-bracket operations under Martin's Axiom and the Continuum Hypothesis.2026-02-16T00:49:51ZOsvaldo GuzmanStevo Todorcevichttp://arxiv.org/abs/2602.14332v1$2$-dimensional Lawvere theories: commutativity and lax phenomena2026-02-15T22:58:48ZThe aim of this paper is to study categorified algebraic structures and their pseudo- and lax homomorphisms using the framework of Lawvere $2$-theories, and more generally, (enhanced) $2$-dimensional sketches. The key notion we focus on is that of $2$-dimensional commutativity. As one of the main results, we prove that if a Lawvere $2$-theory $\mathbb{T}$ is equipped with such a structure, then the $2$-category $\mathsf{Mod}_l(\mathbb{T},\mathbf{Cat})$ of $\mathbb{T}$-models, lax homomorphisms, and modifications admits a natural structure of a closed $2$-multicategory. From this, we deduce a generalization of Fox's theorem. We also discuss the analogue in the higher setting for Lawvere $(\infty,2)$-theories. As a result of independent interest, we construct a multicategory (or $\infty$-operad) structure on the hom-category $\mathsf{Hom}_{\mathbb{V}}(\mathcal{M},\mathcal{N})$, where $\mathbb{V}$ is a monoidal $(\infty,2)$-category and $\mathcal{M},\mathcal{N}$ are monoids therein.2026-02-15T22:58:48Z64 pages. Comments welcome!Tomáš Perutka