Papers

We prove that the Subcomplete Forcing Axiom is consistent with $\diamondsuit^+$.

We show that the satisfiability problem for Strategy Logic introduced by Mogavero, Murano, and Vardi is $\Pi^1_\infty$-complete, and, more strongly, computably isomorphic to true second-order arithmetic. The lower bound is established for the next-time Boolean-goal fragment of Strategy Logic. Consequently, Strategy Logic is not recursively axiomatizable, even with effectively defined $\omega$-rules.

Finite support indicates that the dependence is limited, but not how each finite context controls what can be observed. For a data symmetry G \leq Sym(A) and a finitely supported G-set X, we study the finite-dependence profile X^S = {x : Fix_G(S) fixes x}, indexed by finite contexts S \subseteq A. For relations on A^n this yields Boolean algebras B^{(n)}_{G,S} = Inv_n(Fix_G(S)), forming the invariance hierarchy. The hierarchy separates several nominal principles. Its meet law is the relation-algebra form of the Bojanczyk-Klin-Lasota least-support criterion, while level injectivity is fungibility. The independent join law governs composition across unions of contexts; it holds for locally oligomorphic automorphism groups of ultrahomogeneous structures in purely relational languages of arity at most two, but can fail for unary observations over ternary data. Freshness remains valid sort by sort, and its unrestricted some/any form characterizes full equality symmetry among closed groups. With least supports, orbit-finiteness implies finite context levels and a uniform support bound; under local oligomorphicity the converse also holds. Pointwise closure does not change the profile, and standard atomic-site presentations show that suitable ultrahomogeneous structures with the same age have equivalent action topoi, even though their material FSS universes may retain different external cardinal data. Contextual orientability gives a complementary pointed invariant whose threshold is the least support size of choice from unordered pairs. For countable omega-categorical structures with degenerate algebraic closure, the meet law is equivalent to weak elimination of imaginaries.

We show that for any henselian valued field of mixed characteristic $(0,p)$, the (existential) $\mathcal{L}_{\mathrm{val}}$-theory of the valued field is determined by the (existential) theory of the value group in $\mathcal{L}_{\mathrm{oag}}$ with a constant for $v(p)$ and the (existential) theory of the residue ring $\mathcal{O}_v/(p)$ in an expansion $\mathcal{L}_{\mathrm{Witt}}$ of the language of rings, provided $\mathcal{O}_v/(p)$ is semi perfect. We moreover show that the $\mathcal{L}_{\mathrm{Witt}}$-structure on $\mathcal{O}_v/(p)$ is $\mathcal{L}_{\mathrm{ring}}$-definable using constants, and that this is exactly the structure induced on $\mathcal{O}_v/(p)$ by the ambient valued field. As a consequence, we obtain a relative quantifier elimination result (eliminating $K$-quantifiers) in a suitable language for the theory of roughly deeply ramified henselian valued fields of mixed characteristic $(0,p)$.

The logic FOT is a team-based logic whose expressive power coincides with first-order logic at the level of both sentences and open formulas. In contrast to dependence and independence logics, which can define stronger second-order team properties, FOT is designed to capture exactly elementary team properties, modulo the empty team. In this paper we consider two modifications of FOT. First, we investigate essentially the inclusion atom free fragment of FOT. Our main result establishes quantifier elimination for the fragment in the empty signature. Second, we study an extension of FOT by the intuitionistic implication. The main conclusion is that adding this single connective increases the expressive strength so that every second-order sentence can be encoded by an open formula evaluated on the full team. Consequently, validity of formulas is equivalent to validity of full second-order logic.

This paper introduces the Higher-Order Quadripolar Argumentation Framework (HQAF), which extends bipolar frameworks by allowing attacks and three types of supports—necessary, deductive, and evidential—to interact at higher order. In HQAF, each interaction may have as its source and target an argument, an attack, or a support. We provide a 3-valued semantics via adjacent complete labellings and equational systems, and define encoded semantics directly in propositional logics, mainly Łukasiewicz three-valued logic for the 3-valued case and fuzzy logics based on continuous t-norms (Gödel, Product, Łukasiewicz) for the fuzzy case. Model equivalence between HQAF and its normal encoding is established. The fuzzy equational semantics is shown to be a specific formalism of the fuzzy encoded semantics, and ternarization connects fuzzy models to 3-valued complete labellings. The study is confined to non-set HQAF; collective interactions are reserved for future work.

The Borel distinguishing number $D_B(\mathcal{G})$ of a Borel graph $\mathcal{G}$, recently introduced by Bilge and Kaya, is the minimum number of colors required to break the symmetry of $\mathcal{G}$ in a Borel way. In this paper, we investigate the Borel distinguishing number of Schreier graphs induced by the free part of the shift action $\Gamma \curvearrowright n^\Gamma$. We prove that $D_B(\mathcal{G})\le n+1$ for $\Gamma=\mathbb{Z}^d$ equipped with the standard generators. Moreover, we show that $D_B(\mathcal{G})\ge n+1$ if $ \Gamma$ is amenable and $ \{\gamma \in \mathrm{Aut}(\mathrm{Cay}(\Gamma,S)) \mid \gamma(e) = e \}$ is non-trivial. We also show that $D_B(\mathcal{G})$ is finite if $\Gamma$ is finitely generated, and give some applications of our results. These results answer some questions raised by Bilge and Kaya.

We prove that every infinite introenumerable set contains an infinite uniformly introreducible subset, answering both parts of Question 1.7 of Greenberg, Harrison-Trainor, Patey, and Turetsky affirmatively. Moreover, a single procedure computes the original set from every infinite subset of the selected set. The proof combines the uniformization and refinement results of these authors with Ramsey-theoretic methods and a canonical reconstruction argument. We also obtain refinements controlling the ordinals and hyperjumps of the selected subsets.

We prove that the SU-rank of a supersimple theory is no greater than that of any of its supersimple expansions. A proof for finite rank theories already exists in the literature, but non-continuity presents a problem at limit ranks. We prove the non-decreasing of SU-rank in expansions type-by-type by reducing to finding, in the base theory, certain trees of forking extensions in which the formulas and dividing numbers which witness dividing have a sufficiently uniform pattern. In the case of countable ranks, we can give an especially nice description of this uniformity: for a countable ordinal $\alpha$, any type of SU-rank at least $\alpha$ in a supersimple theory has a chain of forking extensions in the reverse order type of $\alpha$.

We establish necessary and sufficient conditions under which a binary operation on a bounded trellis is a proper nullnorm. The representation combines a t-conorm on the lower interval, a t-norm on the upper interval, two order-preserving maps, and a commutative, increasing function on $I_a^3\times I_a^3$, where $I_a^3$ consists of the elements incomparable with the absorbing element $a$ that neither reach $a$ nor are reachable from $a$. Unlike earlier range-restricted constructions, this function may take values anywhere in the trellis. To preserve associativity for such unrestricted values, we introduce a mixed interaction function that evaluates every pair with at least one component in $I_a^3$. We also derive the specializations in which this region is empty or consists of a single element, including an exact description of the admissible value in the singleton case. A five-element lattice example shows that the mixed associativity condition is independent of the remaining hypotheses, while a fourteen-element nontransitive trellis example demonstrates the necessity of allowing the unrestricted range. Finally, the principal range-restricted subclasses and the bounded-lattice case are recovered as specializations of the general representation.

We study the complexity of simple semi-conditional grammars (SSCGs) in terms of the number of their terminals and non-terminals. We show that SSCGs with three non-terminals can generate all RE languages; two non-terminals suffice for linear languages; and one suffices for unary regular languages. We also determine both upper bounds and fundamental limitations of SSCGs: while certain one-non-terminal SSCGs can generate non-context-free languages, every language generated by a one-non-terminal SSCG is in non-deterministic linear space. We also prove that there exists a regular language of alphabet size at least 3 which cannot be generated by any one-non-terminal SSCG. Finally, we prove that membership testing for SSCGs of two non-terminals is already NP-hard.

We present a new approach to lower bounds on Borel rank via a connection between Borel sets and infinite circuits. We prove an infinite analog to Håstad's switching lemma called the restriction lemma, which shows that by fixing the values of some inputs, we can simultaneously reduce the complexity of one Borel function while largely maintaining the complexity of another. This result provides a purely combinatorial proof of the Borel hierarchy theorem, as well as simple proofs of various Ramsey-like properties of Borel sets and functions. We prove that the restriction lemma is sharp and also discuss counterexamples demonstrating the limitations of the restriction technique, in the context of both Borel functions and $\mathsf{AC}^0$ circuit families.

Let $M$ be a $(0,\omega_1+1)$-iterable mouse with no largest cardinal. Let $\gamma\leq\kappa$ be uncountable cardinals of $M$, with $\kappa$ regular in $M$. Then $M$ satisfies $\diamondsuit_{\kappa\gamma}^+$, and if $\kappa$ is non-ineffable in $M$ then $M$ satisfies $\diamondsuit_{\kappa\kappa}^+$. Suppose that either $\omega_1^M=\omega_1$ or $M$ satisfies "I am $(0,\omega_1+1)$-iterable". Let $\kappa\geq\omega_1^M$ be a cardinal of $M$. Then $M$ satisfies $\diamondsuit^*_{\kappa\omega_1^M}$.

In 1929, Banach and Kuratowski proved under CH a combinatorial theorem, which implies that there is not a non-vanishing $\sigma$-additive finite measure on $\mathbb{R}$ which is defined for every set of reals. In 2003 Bartoszyński and Halbeisen proved that Banach and Kuratowski theorem is equivalent to the existence of a K-Lusin set of the cardinality continuum an the existence of such sets is independent of $ZFC + \neg CH$. On the other hand in 1965 Efimov introduced the strong sequences method which used to prove some well-known theorems in dyadic spaces. The aim of this paper is to show that all this notions can be generalized, i.e. considered in the generalized Baire space and to show some equivalences among them. Moreover, some applications in the direction of calibres, boundedness and partitions relations are also shown.

We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.

A finite object is called probabilistically random if it is an algorithmically random element of a finite set whose Kolmogorov complexity is relatively small. This note studies the amount of probabilistically nonrandom objects (those that are not probabilistically random) as gauged by the universal measure and without assuming any structure on the objects. The main results imply that the universal measure of probabilistically nonrandom objects is vanishingly small and establish the dependence of their universal measure on the required degree of probabilistic randomness.

We show that Medvedev's logic of finite problems, a well-known superintuitionistic logic, is undecidable. The key method is a reduction from the periodic tiling problem to non-theoremhood in Medvedev's logic. This settles a longstanding open problem. Using similar techniques, but reducing instead to the ordinary tiling problem, we likewise obtain undecidability of Skvortsov's logic of infinite problems, and the fact that the two logics are distinct – in fact, they are separated by any aperiodic tiling of the plane. Due to the fact that Medvedev's logic figures in so many different areas, these results have implications for several fields – for example, the study of schematic fragments of logics such as propositional dependence logic, or the study of internal logics of toposes. The core idea and technical work of the undecidability proof were obtained using ChatGPT Sol 5.6, and formally verified in Lean by Claude Opus 5. A detailed methodology section outlines how such results were obtained.

We show that maximal abelian C*-subalgebras (masas) of the Calkin algebra (the algebra of all bounded operators on the separable Hilbert space modulo compact operators) may consistently have their densities strictly less than continuum and we describe many isomorphism types of such masas. Specifically, we prove that after adding any number of Cohen reals to a model of CH the algebra $C(K_{\mathcal A})$ of all complex-valued continuous functions on the Stone space $K_{\mathcal A}$ of a Boolean algebra $\mathcal A$ of cardinality $\omega_1$ is $*$-isomorphic to a masa of the Calkin algebra if and only if $\mathcal A$ does not admit a countably generated ultrafilter. Moreover, for every such Boolean algebra we obtain $\omega_2$ pairwise unitarily non-equivalent such masas, none of which has a commutative lift. We also show in ZFC that if a C*-algebra of the form $C(K)$ for any compact Hausdorff $K$ is $*$-isomorphic to a masa of the Calkin algebra, then no point of $K$ may have character smaller than $\mathfrak p$. Therefore, consistently, there may not be any masa of the Calkin algebra of density less than continuum.

We bound the eventual order types of Skolem functions below finite exponential towers. Writing $E_0(u)=u$, $E_{n+1}(u)=2^{E_n(u)}$, and $\omega_0=1$, $\omega_{k+1}=\omega^{\omega_k}$, the argument gives \[ |\Sk_{<E_n(x^m)}|<\omega_{r_n},\qquad r_n=2+\frac{n(n+3)}2\quad(n\ge1,\ m\ge2\text{ fixed}). \] For triple towers we obtain the sharper bound $|\Sk_{<E_3(x^m)}|<\omega_{10}$ for every fixed $m\ge1$. The proof combines comparisons of asymptotic expansions with finite recursive decompositions and ordinal estimates for ordered sums and products. The analytic part is developed in the classical field of logarithmic-exponential series. We prove the required discreteness, support and truncation statements in this setting. The external inputs are the series construction of van den Dries–Macintyre–Marker and the order and ordinal estimates recalled from Berarducci–Mamino. These bounds imply $|\Sk|=\varepsilon_0$.

We exhibit a well-ordering principle that is equivalent to a theory of partial impredicativity. The latter goes back to Towsner and relates to recent work of Suzuki and Yokoyama. Together with part I of the present paper, this yields a combinatorial upper bound on the axiomatic strength of Fraïssé's conjecture.

We prove several necessary and sufficient conditions under which a point satisfies the Poincaré Recurrence Theorem for all computable (ergodic) measure-preserving transformations and all sets of a particular complexity. The necessary conditions are obtained by constructing specific measure-preserving transformations which violate recurrence. While some of these conditions pertain to standard notions of algorithmic randomness, others involve new notions of genericity developed in the context of a computable probability space, which we call $\Pi^0_n$-genericity and quasi-$\Pi^0_n$-genericity. We also provide conditions under which points recur at a positive frequency in sets containing them, regarding both simple and multiple recurrence.

We study fifteen properties of binary relations that have established uses in modal logic, order and preference theory, and relation algebra. The organising question is pragmatic: once some properties of a relation are known, which further properties follow, which combinations force degeneracy, and which properties remain independent? We give a proved Horn basis of elementary and compound entailments, explicit countermodels for non-entailments, and a relation-algebraic translation of all fifteen properties. The modal discussion includes the usual Scott–Lemmon correspondences and the logic of transitive dense frames studied by Ghilardi and Mints. Exhaustive finite enumeration and targeted model search are used for discovery, while the catalogue is certified in Lean. A kernel-checked coverage calculation ranges over all 2^15 = 32,768 antecedent sets and all fifteen possible consequents. Its 51-rule Horn manifest is coupled definitionally to Lean proofs of semantic soundness, and its 49 witness rows are coupled definitionally to Lean-certified finite or infinite relations. Consequently, over non-empty domains, the Horn closure is complete for positive entailment among the fifteen selected properties, and the consistency classification is complete for their positive combinations.

We prove that conjugacy of minimal homeomorphisms of the Cantor space is Borel bireducible with isomorphism of countable graphs, answering the Cantor minimal case of a question of Foreman. We obtain the lower bound by encoding countably based profinite groups. Finite quotient homomorphisms are represented by factor maps between a common family of minimal subshifts. Amalgamation makes the resulting inverse limit independent, up to conjugacy, of the quotient presentation. Conversely, finite-stage factorization recovers the group from any conjugacy of these inverse limits.

For any infinite cardinal $\kappa$, we give an example of a centerless group $G$ of cardinality $\kappa$ whose automorphism tower terminates after $\kappa^+$ steps, answering a question of Simon Thomas. The work on this paper was assisted by AI.

We answer in the negative the question of Thomas, recorded by Conley, Conley–Marks–Unger, and Conley–Tamuz, of whether every locally finite Borel graph admits a Borel unfriendly partition. Our counterexample has unbounded degree and is closed on a zero-dimensional Polish space; its connectedness relation is hyperfinite, and its components are bipartite and one-ended. Every unfriendly colouring is proper. Together with a parity obstruction, this rigidity rules out Baire measurable colourings that are unfriendly on a comeager set, and measurable colourings that are unfriendly almost everywhere for a quasi-invariant probability of finite average degree. In the positive direction, a Borel graph of maximum degree at most four admits a Borel unfriendly colouring whenever each component contains a cycle or a vertex of degree at most two. This reduces the Borel problem in maximum degree three to cubic forests and, with a theorem of Conley–Marks–Unger, gives Baire measurable unfriendly colourings for all Borel graphs of maximum degree at most four.

We provide a proof, free of ultrafilters and almost reduction, that every subset of a topological Ramsey space is Ramsey in the Solovay model.

This project began as an attempt to prove that Medvedev logic is decidable with the help of generative AI systems. The author (as well as the generative AI systems, or at least they claim to be since I have asked them) was surprised by its eventual conclusion. We prove that Medvedev logic ML, the intermediate logic of finite problems, is Pi-01-complete under computable many-one reductions. Consequently, ML is not recursively enumerable, a fortiori undecidable, and admits no recursively enumerable sound and complete proof calculus. The proof connects the periodic domino problem with intuitionistic formulas through a shared intermediate structure that we call a Wang-Medvedev pair. Such a pair consists of a finite partially ordered set of roles together with demands. Demands define the interaction between roles. A realization labels nonempty subsets of a finite set with these roles, respecting the order and satisfying the demands. We associate a pair with each finite Wang system and show that it has a realization iff the system tiles a finite torus. We then construct an intuitionistic formula that fails on some finite Medvedev frame iff the same pair is realizable. Realizability thus provides the link between periodic tilings and the countermodels.

In this article, we have introduced a new possibilistic logic on a logic of formal inconsistency with the aim of developing a possibility theoretic framework to deal with uncertainty and inconsistency meaningfully without leading to a system collapse. We have discussed the syntax and semantics for this logic and have proved the soundness and completeness theorems. A set of new measures of consistency, contradictoriness, and triviality of a set of formulas have been defined. These have then been put to use in an example to show that this framework can provide better means of machine reasoning.

We ask whether it can be certified algorithmically that a self-modifying program keeps a behavioural property, a safety property in the motivating case, after its next rewrite (preservation) and along its whole evolution (persistence). When the rewrite depends only on behaviour, preservation is a behavioural property and Rice's theorem applies. When the rewrite reads the code, preservation is no longer behavioural; yet, under a uniform disruption condition, the s-m-n reduction that proves Rice's theorem works inside a single class of behaviourally identical programs, and preservation inherits the degree of the halting problem. One step never exceeds the degree of the property, while persistence can climb one level of the arithmetical hierarchy. We then isolate the mechanism shared by rewriting, supervision and system comparison, the elevation operator, and prove a normal form: the preserving set is determined by a single finite trigger and a polarity, and the Rice-Shapiro theorem restricts the polarity to the arithmetical class of the property. Runtime monitors, consistency supervision, conformance to a reference and observational equivalence are instances, and no sound theory covers the preserving systems.

We prove, in $\mathsf{ZFC}$, that the $\lambda$-terraced cube relation fails whenever $\lambda$ is an uncountable cardinal. The corresponding terraced relation for quadruples fails for every $\lambda$. If $\lambda$ is $\aleph_0$ then the pretinent terraced relation has consistency strength of at least one Woodin cardinal. We prove positive polarized relations at a successor and a double successor from wondrous ideals. We show, however, that there are no such ideals over two consecutive cardinals simultaneously.