In [2], we introduced a syntactically defined and highly general class of calculi known as semi-analytic. We then demonstrated that any sufficiently strong (modal) substructural logic with a semi-analytic calculus must satisfy the Craig interpolation property. In this paper, we show that if the calculus is also terminating in a certain formal sense, then its logic has the Uniform Interpolation Property (UIP). This result has significant applications. On the positive side, it provides a uniform and modular method for proving UIP for various logics, including FLe, FLew, CFLe, CFLew, and their K, D, and T-type modal extensions, as well as CPC, K, and KD. However, its more striking consequence lies in the negative direction. It extends the negative results of [2] to logics with CIP but without UIP. In particular, it shows that the modal logics K4 and S4 do not have a terminating semi-analytic calculus.
Motivated by team semantics and existential second-order logic, we develop a model-theoretic framework for studying second-order objects such as sets and relations. We introduce the notion of an abstract elementary team category that generalizes the standard notion of an abstract elementary class, and show that it is an example of an accessible category. We apply our framework to show that the logic FOT introduced by Kontinen and Yang [19] satisfies a version of Lindström's Theorem. Finally, we consider the problem of transferring categoricity between different cardinalities for complete theories in existential second-order logic (or independence logic) and prove both a downwards and an upwards categoricity transfer result.
How do we randomly sample an infinite sequence from a first order structure? What properties might hold on almost all random sequences? Which kinds of probabilistic processes can be meaningfully applied and studied in the model theory context? This paper takes these questions seriously and advances a plausible framework to engage with probabilistic phenomena. The central object of this paper is a probability space. The underlying set of our space is a standard model theoretic object, i.e. the space of types in countably many variables over a monster model. Our probability measure is the iterated Morley product of a fixed Borel-definable Keisler measure. Choosing a point randomly in this space with respect to our distribution yields a "random generic type" in countably many variables. We are interested in which events hold for almost all random generic types. We consider two different flavors of model theoretic events: (1) When is the induced structure on almost all random generic types isomorphic to a fixed structure? (2) For a fixed formula which is unstable, IP, sOP, etc., what is the probability that a random generic type witnesses this dividing line? For (1), we show that if our measure satisfies a particular extension axiom, then there exists a structure N such that the induced structure on almost all random generic types is isomorphic to N. The proof echos a celebrated result of Glebskii et al. and Fagin concerning the existence of almost sure theories. We also provide examples where no such model exists. For (2), we show that if our initial distribution is fim, then almost no random generic types witness instability, IP, or sOP. In the local NIP context, we use results from combinatorics to prove that for any Borel-definable measure, the "average value of witnessing k-instability" across all permutations converges to 0. Some examples are provided.
If kappa is an infinite cardinal, the boldface GCH at kappa is the statement that kappa(+) does not inject into P(kappa). It will be shown here that omega(1) -> (omega(1))(2)(omega 1) (the strong partition property at w1) and j(mu 1 omega 1) (omega(1)) = omega(2) (the ultrapower of w(1) by the club filter on omega(1) is omega(2)) imply that the boldface GCH holds at wn for all n < w using combinatorial arguments. In particular, AD implies the boldface GCH holds at omega(n) for all n < omega. (c) 2026 The Author(s). Published by Elsevier B.V.
We study the compressibility of enumerations in the context of Kolmogorov complexity, focusing on strong and weak forms of compression and their gain: the amount of auxiliary information embedded in the compressed enumeration. The existence of strong compression and weak gainless compression is shown for any computably enumerable (c.e.) set. The density problem of c.e. sets with respect to their prefix complexity is reduced to the question of whether every c.e. set is well-compressible, which we study via enumeration games. (c) 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
This work contributes to the studies on the computational complexity of game trees under different distributions. Suzuki and Niida (2015) [20] showed that for any uniform binary AND-OR tree, if an independent distribution d maximizes the tree evaluation cost over all optimal algorithms, then it is an independent and identical distribution. Peng et al. (2017) [16] extended this result to balanced multi-branching trees under the assumption that the probability r of the root being 0 is fixed and satisfies 0 < r < 1. Whether this restrictive condition can be removed has remained an open problem. In the present work, we provide a positive answer to this question. In addition, Okisaka et al. (2017) [14] investigated the uniqueness of the eigen-distribution for multi-branching trees weighted with (a, b) under correlated distributions, which is a weak version of Saks and Wigderson's weighted trees. One might naturally expect that the eigen-distribution is primarily determined by the values of a and b, but we show that this intuition is misleading. Specifically, we show that for any a, b, the eigen distribution is an E-1-distribution with respect to the class of deterministic algorithms for any AND-OR trees weighted with (a, b) of sufficiently large height. Finally, we explore applications of game trees in the analysis of series-parallel systems. (c) 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
We define the first nontrivial proof system for the complement of quantum satisfiability (QSAT). The system uses left-ideal rules in the ring of linear operators on an n-qubit register. Implicational completeness is given by a matricial version of Hilbert's Nullstellensatz. We prove two distinct forms of the system to be equivalent respectively to Resolution and Polynomial Calculus with Resolution in the classical subcase. The systems are efficiently verifiable by a classical TM. We also discuss the matter of quantum proof systems for QSAT. (c) 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
This paper presents a proof of strong normalization of natural deduction for minimal propositional logic, inspired by the syntax-directed inductive techniques of [20]. While this avenue bypasses semantic models, like computability predicates, and provides a short proof by embedding the reduction relation into syntactic rules, it operates within the framework of the lambda calculus, with almost no reference to the methods of Structural Proof Theory. Instead, we conciliate both methodologies by reinterpreting their arguments to provide an explanatory and syntax-directed proof in the context of natural deduction, emphasizing the diagrammatic manipulation of derivations, the combinatorial behavior of proof-trees and the usefulness of an enhanced syntax of lambda calculus to codify diagrams, thus putting the Curry-Howard correspondence at work. Our approach not only bridges the gap between the algebraic reasoning of the lambda calculus and the diagrammatic intuition of natural deduction but also aligns with the increasingly tangible ideal of producing computer-assisted formalizations of nontrivial mathematical results. (c) 2026 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY-NC-ND license (http:// creativecommons.org/licenses/by-nc-nd/4.0/).
Given a Polish group G, let E(G) be the right coset equivalence relation G(omega)/c(G), where c(G) is the group of all convergent sequences in G. In this article, we use the tool of the forcing method to prove a rigid theorem for the wreath product Lambda(sic)Theta: Let Lambda, Gamma, Theta, Theta ' be four nontrivial countable discrete groups. Suppose Lambda has no finite subgroup. Then E(Lambda(sic)Theta) <=(B) E(Gamma (sic) Theta ') if and only if there is a group isomorphism phi : Lambda -> (Gamma) over tilde/Delta, where (Gamma) over tilde is a subgroup of Gamma, Delta is normal in (Gamma) over tilde. A direct corollary is that, there are continuum many non-archimedean Polish groups (G(r))(r is an element of R) such that these E(G(r))'s are pairwise Borel incomparable. Using the technique developed in this article, we also prove (1) E(Z (sic) Z(2))<(B) E(Z (sic) Z(2)(omega)). (2) E(Z (sic) Z(2))<(B) E(Z (sic) Z(2))(2)
In this paper we prove that interpolation holds in conditional equational logic. Our proof will be proof-theoretic, based on the representation of conditionals by functions. This representation enables the deployment of function properties like monotonicity and continuity, and function operators like fixpoint constructors. The conditionals we represent by functions are Horn formulas. We intend to demonstrate that this representation leads to succinct descriptions of provability and its properties. This may inspire to use this representation also for other conditionals like sequents and proof rules. (c) 2026 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY license (http://creativecommons.org/licenses/by/4.0/).
We study the definable topological dynamics (C, SG(M)) of a definable group C acting on its type space SG(M), where M is a structure in which C is defined. In [11], Newelski raised the question whether weakly generic types coincide with almost periodic types in (C, SG(M)). The question is restated in [2] in the special case when C is a definably amenable NIP group. In [26], we introduced the notion of stationarity and showed that the answer to the question above is positive when C is a stationary definably amenable group definable over the field of p-adic numbers or an o-minimal expansion of a real closed field. In this paper, we continue the work of [26], focusing on the case where C is a definably amenable group definable over the field of p-adic numbers, and show that weakly generic types coincide with almost periodic types if and only if C is either dfg or stationary. (c) 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
Emmons [5] proved the existence of a Lindahl equilibrium in a general equilibrium model with public goods and a hyperfinite Loeb space of agents. While Emmons allows incomplete and intransitive preferences, he assumes that preferences are monotone and that production satisfies free disposal, which exclude the presence of private bads. In this paper, we extend his analysis to economies with both public goods and private bads. We relax the monotonicity assumption by requiring that preferences be monotone only in public goods. Following Emmons, we model the agent space using a hyperfinite Loeb space and our proof relies on nonstandard analysis and Loeb measure theory. (c) 2026 The Authors. Published by Elsevier B.V. This is an open access article under the CC BY-NC-ND license (http:// creativecommons.org/licenses/by-nc-nd/4.0/).
We introduce a new method for constructing ideals on countable sets. As an application, we prove the existence of a Sigma 0 expressible as a countable union of hereditary G delta sets, thereby answering a question similar to 3 ideal of compact sets that is not posed by & Eacute;. Matheron and M. Zelen & yacute;. Furthermore, we apply this construction to investigate Farah's conjecture, obtaining several new partial results. (c) 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
We show how to construct an aleph 1-Suslin tree which is indestructible under forcing with a given c.c.c. poset of size aleph 1, in L(x) for any real x. This answers a recent question of Woodin. More generally we do this at any regular uncountable cardinal which is not weakly compact, and the construction can be carried out in any model satisfying standard condensation properties. (c) 2025 Published by Elsevier B.V.
In this paper, we demonstrate the existence of reasonable non-classical set theories in which the Axiom of Choice, Zorn's Lemma, and the Well-Ordering Theorem are equivalent, using the framework of algebra-valued model construction of set theories. We also investigate the non-classical behavior of well-ordering with respect to belongingness. (c) 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.
This paper develops stable canonical rules for intuitionistic modal logics, which were first introduced for superintuitionistic logics and transitive normal modal logics in [9] and [8] respectively. We first prove that every intuitionistic modal multi-conclusion consequence relation is axiomatizable by stable canonical rules. This allows us to assume, without loss of generality, that rules considered by us are stable canonical ones. The idea turns out to be useful. In particular, using stable canonical rules, we get an alternative proof of the Blok-Esakia theorem for intuitionistic modal logics which was first proved in [35] and generalize it to multi-conclusion consequence relations. We also prove the Dummett-Lemmon conjecture for intuitionistic modal multi-conclusion consequence relations, which, as far as we know, is a new result. (c) 2026 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY-NC license (http://creativecommons.org/licenses/by-nc/4.0/).
It is known that, in univalent mathematics, type universes, the type of n-types in a universe, reflective subuniverses, and the underlying type of any algebra of the lifting monad are all (algebraically) injective. Here, we further show that the type of ordinals, the type of iterative (multi)sets, the underlying type of any pointed directed complete poset, as well as the types of (small) ∞-magmas, monoids, and groups are all injective, among other examples. Not all types of mathematical structures are injective in general. For example, the type of inhabited types is injective if and only if all propositions are projective. In contrast, the type of pointed types and the type of non-empty types are always injective. The injectivity of the type of two-element types implies Fourman and Ščedrov's world's simplest axiom of choice. We also show that there are no nontrivial small injective types unless a weak propositional resizing principle holds. Other counterexamples include the type of booleans, the simple types, the type of Dedekind reals, and the type of conatural numbers, whose injectivity implies weak excluded middle. More generally, any type with an apartness relation and two points apart cannot be injective unless weak excluded middle holds. Finally, we show that injective types have no non-trivial decidable properties, unless weak excluded middle holds, which amounts to a Rice-like theorem for injective types.
