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.

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.