We settle the long-standing open question whether there exists a $3$-ladder of cardinality $\aleph_2$. Given a positive integer $n$, an $n$-ladder is a lower finite lattice whose elements have at most $n$ lower covers. In 1984, Ditor proved that every $n$-ladder has cardinality at most $\aleph_{n-1}$, and that this cardinal bound is sharp for $n = 1,2$. He then raised the question of whether the bound is attained for $n\ge 3$ as well. An affirmative answer is known to be consistent with $\mathsf{ZFC}$. We prove, relative to the consistency of a Mahlo cardinal, that the question is independent of $\mathsf{ZFC}$. More precisely, we show that the nonexistence of a $3$-ladder of cardinality $\aleph_2$ is equiconsistent with a Mahlo cardinal.
Hilbert space, Urysohn space and generic hypergraphs appear as the canonical objects k-trace definable in real closed fields or vector space
abstractclick to expand
Motivated by the "composition theorems" of Chernikov-Hempel and Abd Aldaim-Conant-Terry we introduce $k$-trace definability between first order theories. Any theory which is $k$-trace definable in a NIP theory is $k$-NIP and any theory which is $2$-trace definable in a stable theory is $2$-NFOP. All known examples of $k$-NIP theories are $k$-trace definable in NIP theories. We show that for several of the main examples of $k$-NIP theories $T$ there is a NIP theory $T^*$ such that $T$ is the (unique up to a certain notion of equivalence) universal theory which is $k$-trace definable in $T^*$. For example the theory of Hilbert space is the universal theory which is $2$-trace definable in RCF, the theory of the generic class $k$ nilpotent Lie algebra over $\mathbb{F}_p$ is the universal theory which is $k$-trace definable in the theory of infinite $\mathbb{F}_p$-vector spaces, the theory of the generic $k$-hypergraph is the universal theory which is $k$-trace definable in the theory of a set with two elements, and the theory of Uryshon space is the universal theory which is $2$-trace definable in the theory of $(\mathbb{R}; +, <)$. We construct the universal theory $D_k(T)$ which is $k$-trace definable in an arbitrary theory $T$.
Real-valued logics have seen a renewed interest in verification for probabilistic and quantitative systems, in particular machine learning models, where they can be used to directly integrate specifications in the training objective. To do so effectively one has to strike a balance between the logical properties of the connectives and their semantics. A major hurdle in this sense is to give ``soft'' (i.e. differentiable) semantics to additive connectives -- in linear and fuzzy logics, additives are necessarily ``hard'' lattice operations.
In this paper, we solve this problem by combining an accurate analysis of the properties of sum and product on the reals with a significant revision of sequent calculus. We introduce `quantitative sequent calculi', which simultaneously generalize hypersequent calculi of fuzzy logics and deep inference, and in which validity of a proof and provability of a sequent are real-valued quantities. We present a family of calculi, pQLL, indexed by a hardness degree $p$, prove cut-elimination theorem for them, and show completeness for enriched residuated `soft' lattices. For $p = \infty$, pQLL reduces to MALL, with provability in pQLL converging to provability in MALL when $p \to \infty$.
Fragments satisfying the duality embed conservatively into geometric logic; coherent, regular and disjunctive logics are shown to qualify.
abstractclick to expand
We explore the notion of conceptual completeness for a fragment of geometric logic in the framework developed by the first and third author. Unlike its traditional interpretation as a reconstruction of syntax from semantics, in this paper we characterise conceptual completeness of a fixed fragment in terms of a duality between theories and topoi. We then show that conceptually complete fragments are conservatively embedded in full geometric logic, thus casting conceptual completeness in a new proof-theoretic light. We give a new proof of conceptual completeness for coherent logic, and we also show that regular, disjunctive, and essentially algebraic logic with falsum are conceptually complete. Finally, we show that our notion is equivalent to a traditional reconstruction result under the assumption of completeness with respect to set-based models: in the coherent case, we thus recover Makkai's original reconstruction theorem via ultracategories.
Formalization shows the modal equivalence requires arithmetical comprehension; semantic van Benthem does not.
abstractclick to expand
This paper investigates the logical strength of two theorems in modal propositional logic - the Hennessy-Milner theorem and the van Benthem characterization theorem - within the framework of second-order arithmetic. We demonstrate that the Hennessy-Milner theorem is equivalent to $\mathrm{ACA}_0$ over $\mathrm{RCA}_0$. For the van Benthem characterization theorem, we introduce three variants: the semantic, syntactic, and hybrid forms. We show that the semantic form is provable in $\mathrm{RCA}_0$, the syntactic form is provable in $\mathrm{PRA}$, and the hybrid form is equivalent to the weak completeness theorem for first-order logic over $\mathrm{RCA}_0$.
Custom structures for q-Pochhammer symbols and Bailey's lemma produce computer-checked proofs of the classical identities.
abstractclick to expand
The theory of $q$-series and basic hypergeometric series plays a crucial role at the intersection of combinatorics, number theory, and representation theory. From the classical partition identities of Euler and Jacobi to modern developments in class field theory, vertex operator algebras, and the Monstrous Moonshine conjecture, $q$-series provide the analytic framework for a wide range of profound applications. In this paper, we discuss the formalization of this theory in the Lean proof assistant, a process that requires careful design of scalable and versatile structures to reconcile formal algebraic identities with analytic convergence properties. We address these foundational challenges by focusing on the construction of $q$-Pochhammer symbols, $q$-binomial coefficients, Bailey's Lemma and similar primitives. To demonstrate the utility of this work, we provide fully verified proofs of the Jacobi Triple Product formula and the celebrated Rogers-Ramanujan identities, which serve as both historical and technical benchmarks for the field. This work establishes a rigorous computational foundation for the future formalization of mock theta functions, modular forms, and the diverse algebraic structures that underpin their applications across mathematics and physics.
A theorem on maps to inverse limits of torsion groups implies this continuity result and ties the Grigorchuk group to measurable cardinals.
abstractclick to expand
We prove a general theorem giving constraints on maps from certain topological groups to inverse limits of bounded torsion groups. From this we obtain some automatic continuity and ultraproduct results. For example, every homomorphism from a Polish group to a countable torsion-free residually finite group has open kernel. Also, the Grigorchuk group is a homomorphic image of a nonprincipal ultraproduct of groups if and only if there exists a measurable cardinal.
We study the expressive power of the simplest modal-temporal language, obtained by adding Prior's temporal operators \(G\) and \(H\) to the basic modal language with \(\Box\). This language is the standard bimodal combination of modal and tense logic; under its functional interpretation it is denoted \(L_{T\times W}\). To analyse its definability across five order types, we consider two semantic readings of the temporal operators: the standard reading (\(G,H\)), which includes the current instant, and the strict reading (\(G^{\ast},H^{\ast}\)), which always excludes it.
We examine nine functional properties -- totality, non-totality, injectivity, surjectivity, monotonicity, strict monotonicity, antitonicity, strict antitonicity, and constancy -- over preorders, strict preorders, partial orders, linear orders, and strict linear orders. Our analysis reveals two different levels of expressive power. In the original multiflow setting, the language is quite weak and the two readings coincide. When we restrict the semantics to minimal functional frames (the \(O^{2}\) family), many properties become definable, and the choice of reading becomes crucial: the strict reading can define properties such as injectivity even in reflexive orders.
The same definability patterns appear with indexed languages and with the Uniform Domain condition on the semantics of \(L_{T\times W}\). That three such different ways of controlling functional multiplicity lead to identical definability patterns indicates that the expressive limitations of the original framework come from the uncontrolled multiplicity of functions, not from any weakness of the operators. Even after controlling functional multiplicity, a set of properties remains undefinable in all non-linear orders, showing that the lack of connectivity is a fundamental obstacle.
Equiconsistency settles consistency questions and bounds size of Lindelöf Q-spaces with weight at most the continuum.
abstractclick to expand
A topological space \(X\) is called a \(Q\)-space if every subset of \(X\) is a \(G_\delta\)-set, and \(X\) is a \(\Delta\)-space if for any decreasing sequence \(\{D_n : n \in\omega\}\) of subsets of \(X\) with empty intersection there is a decreasing sequence \(\{U_n : n \in \omega\}\) of open sets with empty intersection such that \(D_n \subseteq U_n\) for all \(n \in\omega\).
Our main result shows that the following statements are equiconsistent:
(1) There exists a measurable cardinal;
(2) There exists a crowded Baire \(T_1\) \(\Delta\)-space;
(3) There exists a crowded Baire \(T_4\) \(Q\)-space;
(4) There exists a \(T_1\) \(\Delta\)-space admitting a strictly positive probability measure vanishing on points;
(5) There exists a \(T_3\) \(Q\)-space admitting a strictly positive probability measure vanishing on points.
This provides complete answers to some problems and partial answers to other problems that have recently appeared in the literature.
We also prove a new result concerning Lindel\"of \(Q\)-spaces: if \(X\) is a \(T_3\) Lindel\"of \(Q\)-space with \(w(X)\leq \mathfrak c\), then \(|X|<\operatorname{cf}(\mathfrak c)\). This yields a number of nonexistence results for large Lindel\"of, locally compact, compact, and countably compact \(Q\)-spaces.
It is well known that if a diophantine equation turns out not to have a solution over the integers modulo p, for some p, then it does not have a solution over the integers per se. This is because the integers modulo p are a homomorphic image of the integers. However, the integers modulo p are of little use when faced with diophantine inequalities, as the homomorphic image of the less-than-relation is trivial. The purpose of the present paper is to introduce a way of gereralising a particular representation of the integers modulo p. The generalizations, novel to this paper, are in the form of decidable Lindenbaum-algebras, and allow for deciding whether given positive first-order formulas in the language of first-order arithmetic are solvable. Crucially if a system of diophantine inequalities turns out not to be solvable in one of the Lindenbaum-algebras, then it is not solvable over the standard integers.
Let \(\vec F(2^{\mathbb Z^2})\) be the directed Schreier graph on the free part of the Bernoulli shift \(\mathbb Z^2\curvearrowright 2^{\mathbb Z^2}\), with arcs in the two coordinate directions. We prove that the continuous oriented chromatic number of it is 7, that is, there is a tournament on 7 vertices receiving a continuous graph homomorphism from $\vec F(2^{\mathbb Z^2})$ and there is no continuous graph homomorphism from $\vec F(2^{\mathbb Z^2})$ to any tournament on 6 vertices.
The resulting operator satisfies axiom 4 without separation axioms and yields completeness of K4 for all infinite spaces.
abstractclick to expand
In nonstandard analysis the halo of a point in a topological space is the intersection of the nonstandard extensions of all its open neighbourhoods. We define a parametric family of modal operators from the halo by varying which elements of the nonstandard extension are admitted as witnesses, and identify four canonical instances. Two recover well-known modalities: the topological closure and the Cantor derivative. A third reduces to Kripke semantics over the specialisation preorder. The fourth, purely nonstandard instance admits only nonstandard witnesses. The Transfer Principle forces it to coincide with the $\omega$-accumulation point operator, a classical topological notion not previously studied in modal logic. Unlike the Cantor derivative, the $\omega$-accumulation operator maps arbitrary sets to closed sets without any separation axiom, yielding an $\omega$-Cantor-Bendixson decomposition on all topological spaces. Axiom 4 holds universally, again without separation conditions. We prove that K4 is the complete logic over infinite spaces, and GL over infinite $\omega$-scattered spaces.
We develop translations from relevant logics into normal modal logics, and use them to clarify structural connections between relevant and modal logic, obtain a few corollary results, and raise questions for future work.
IK formulas are exactly those first-order properties preserved under the defined IK-bisimulations on relational models.
abstractclick to expand
We define the notion of IK-bisimulation between the relational semantics for the intuitionistic modal logic IK, and prove that IK arises as the IK-bisimulation-invariant fragment of intuitionistic first-order logic. En route, we provide an intrinsic characterisation result of this logic by way of a Hennessy-Milner-style theorem and develop some intuitionistic first-order model theory, including intuitionistic analogues of Los's Theorem, elementary embeddings and countable saturation.
We study interpretations of modal logics in one another where the Boolean connectives are interpreted identically and the modal operator diamond is interpreted by an arbitrary formula A(p). Clearly, such a formula A(p) defines an interpretation of a normal modal logic whenever A(p) is additive (that is, preserves disjunction) and normal (that is, preserves bottom) in the target logic. In the present paper, we provide a complete description of all additive and normal formulas in five prominent modal logics: K, GL, Grz, S4, and S5. For K, GL, and S5, we also describe all additive and normal formulas with parameters.
We study the recently introduced intuitionistic monotone modal logic IM. We first provide a semantic characterisation for a family of natural extensions of IM in terms of constructive neighbourhood models. We then present a calculus for IM and its extensions, obtained by adapting a structured calculus for the classical monotone modal logic M. Based on the calculus, we prove some preliminary results for IM, including its decidability. Our calculus also reveals an interesting analogy between constructive and intuitionistic variants of M and the corresponding variants of K, thereby further justifying IM as a faithful intuitionistic variant of M.
We study structural completeness in the infinitary sense (strong structural completeness) in an algebraic setting. A variety is structurally complete (SCpl) if it is generated, as a quasivariety, by its free algebras, and it is strongly structurally complete (SSCpl) if it is generated, as a prevariety, by its free algebras. A quasivariety is SSCpl if it is generated, as a prevariety, by its free algebras.
We prove that every quasivariety of finite type with the CEP that is generated by finite algebras and contains an infinite irreducible algebra is not SSCpl. Moreover, every congruence meet-semidistributive variety of finite type generated by finite algebras is SSCpl if and only if it is tabular. Thus, Dummett's and Medvedev's logics are SCpl but not SSCpl.
A variety is primitive if it is SCpl and all its subvarieties are SCpl; it is strongly primitive if it is SSCpl and all its subvarieties are SSCpl. We prove that in primitive congruence-distributive varieties of finite type, the tabular subvarieties, and only those, are strongly primitive. This observation also yields a criterion for strong primitivity.
The result equips logics with countable operations for use in measure theory and ergodic theory with a sound and complete semantics.
abstractclick to expand
We investigate a modal extension of the infinitary classical logic with countable meets and joins, formulated with an eye toward measure-theoretic work in dynamical systems and in point-free ergodic theory. We define a modal formalism in this language, which we call modal measurable logics. We also introduce a Kripke-like semantics for these logics in measurable spaces taking a designated modal sigma-ideal into consideration. Using a restriction of Jonsson-Tarski duality and a modal extension of the Loomis-Sikorski theorem, we prove completeness of modal measurable logics with respect to this new semantics.
Any extension arises by independent choice of one intermediate logic and one orthomodular logic.
abstractclick to expand
We investigate logics that generalize both intuitionistic logic and quantum logic. In earlier work, we introduced Ex-logic, an extension of Holliday's fundamental logic that coincides with the intersection of orthologic and the implication-free fragment of intuitionistic logic. In this paper, we add an implication connective to Ex-logic and axiomatize iEx-logic, the intersection of full intuitionistic logic and orthomodular logic with the implication connective interpreted as the Sasaki hook. As a consequence, we obtain a characterization of the lattice of logics extending iEx-logic as the product of the lattice of intermediate logics and the lattice of orthomodular logics. We also explore the robustness of our algebraic approach by briefly discussing extensions of iEx-logic with modal operators.
We present MINT, a dynamic-precision CNN inference accelerator based on left-to-right (LR) arithmetic. LR arithmetic computes in most-significant-digit-first manner and exposes useful partial results early so that the computation can be terminated once the desired precision is achieved. At the core, there is a MSDF serial-parallel inner-product unit, which uses redundant signed-digit representation to compute each convolution window. A budget-constrained greedy search profiles all convolution layers from INT2 to INT7 and selects the lowest precision per layer while constraining total accuracy loss to within 2\% of the INT8 baseline for VGG-16 and ResNet-18 networks. The design is synthesized on a Xilinx Zynq-7020 at \SI{200}{\mega\hertz}, and uses 5.64 average bits for VGG-16 and 6.04 for ResNet-18, while achieving 19.86 GOPS and 29.51 GOPS/W on VGG-16, and 18.86 GOPS and 26.40 GOPS/W on ResNet-18. This corresponds to 32.6\% and 26.0\% higher throughput and 82.10\% and 62.90\% higher energy efficiency than INT8 with only 1.81\% and 1.96\% drops relative to the INT8 baseline. Compared with representative prior FPGA CNN accelerators considered in this study, MINT delivers the highest energy efficiency among the listed VGG-16 and ResNet-18 designs on Zynq-7020 platform.
Extends surface classification to orbifolds with torsion and yields homogeneity for certain ergodic actions.
abstractclick to expand
In their recent paper, Bergfalk and Smythe prove that the isometry equivalence relation on hyperbolic surfaces with finitely-generated fundamental group is concretely classifiable, and ask whether the same result holds true for 2-dimensional hyperbolic orbifolds, or equivalently, whether the action of $\text{PSL}_2(\mathbb{R})$ on its space of finitely-generated discrete subgroups is concretely classifiable. In this note we answer this question in the affirmative. We then use the result to prove that a nonsingular ergodic $\text{PSL}_2(\mathbb{R})$-space with nonelementary finitely-generated stabilizers is homogeneous, in similarity with a result of Stuck-Zimmer for lattices in semisimple lie groups. The main ingredients of our proof are Selberg's lemma and a result of Greenberg on commensurators.
This paper investigates recovery operators in quasi-Nelson logic, the algebraizable logical counterpart of quasi-Nelson algebras. These form a variety of three-potent, distributive, but not necessarily involutive residuated lattices that may be regarded as a common generalization of Nelson and Heyting algebras. We consider both consistency and determinedness operators, with a particular focus on logics and algebras that satisfy the prelinearity condition, which is well-known in the area of mathematical fuzzy logics. We show that, essentially, all algebraic and logical results already proved for (prelinear, distributive) involutive residuated lattice-based LFIs/LFUs can be recovered in the quasi-Nelson setting, where one dispenses with the involutivity assumption. In this setting, consistency and undeterminedness operators are no longer duals of one another, and hence call for a more fine-grained algebraic and logical formalization.
Non-trivial elements achieve maximal displacement of 1 under iteration for comeager many such subgroups.
abstractclick to expand
The isometry group of the bounded Urysohn space, $G = \mathrm{Iso}(\U{1})$ is a central object in the study of Polish groups and topological dynamics. It is known that generic sequences in $G$ generate algebraically free dense subgroups. In this paper, we show that such generic free subgroups exhibit strong geometric rigidity. Specifically, we prove that for a comeager set of sequences generating dense free subgroups $F\leq G$, every non-trivial element $h\in F$ acts with maximal metric displacement, satisfying $\sup_{n\in \N} d(h^n(x),x) = 1$ for every $x \in \U{1}$. As a consequence, these generic subgroups satisfy the \emph{no small subgroup} ($\nss$) property. We note that the method naturally extends to the full isometry group $\mathrm{Iso}(\mathbb{U})$ of the classical Urysohn space.
We study binary classification problems whose decision sets are given by definable sets in o-minimal expansions of the real field. Motivated by cell decomposition of definable sets, we introduce traceable sets as a classical proxy for definable decision regions and analyze their approximation by ReLU neural networks. Under uniform bounds on the number of connected components and suitable $C^m$ extensions for the boundary functions, we prove that characteristic functions of traceable subsets of $[-1/2,1/2]^n$ can be approximated in $L^p$ to accuracy $\varepsilon>0$ by ReLU neural networks of size $\mathcal{O}(\varepsilon^{-p(n-1)/m})$, with depth independent of $\varepsilon$ and polynomially bounded weights. This establishes quantitative approximation rates for certain definable collections in o-minimal structures using ReLU neural networks. The same approach also yields the stated approximation rates for a subclass of definable maps $[-1/2,1/2]^n \to \mathbb{R}$. We then combine the approximation capabilities with entropy estimates for ReLU neural network classes to obtain statistical learning rates for empirical risk minimization with hinge loss. For $N$ uniformly distributed samples, the resulting classifiers achieve expected misclassification error of order $N^{-m/(m+pn-p)}$ up to an arbitrarily small polynomial loss.
A bound on the Turing jump needed for a low-color copy shows the statement is equivalent to ACA0' over RCA0
abstractclick to expand
Let $\mathbb{H}_{n+1}$ denote a computable copy of the $(n+1)$-clique free universal homogeneous Henson graph, $G$ denote a finite subgraph of $\mathbb{H}_{n+1}$, and $k(G,n)$ denote the big Ramsey degree of $G$ in $\mathbb{H}_{n+1}$. We prove that for any computable coloring $\chi$ of the copies of $G$ in $\mathbb{H}_{n+1}$, there is a copy $\mathbb{H}'$ of $\mathbb{H}_{n+1}$ that is computable from $0^{(2\delta(G,n)-1)}$ in which $\chi$ takes no more than $k(G,n)$ colors, where $\delta(G,n)$ denotes the maximum number of levels of a diary for $G$ in $\mathbb{H}_{n+1}$ (this is a finite number). It follows that the statement, ``Henson graphs have finite big Ramsey degrees," is provable in ACA$_0'$. Combining this with a recent result of Cholak, Dobrinen, and McCoy \cite{CDM} yields the equivalence of the statement with ACA$_0'$ over RCA$_0$.
Machine-checked proofs cover the 43 results establishing a model for the untyped lambda calculus.
abstractclick to expand
We present a complete machine-checked formalization of Dana Scott's landmark 1972 paper \emph{Continuous Lattices} \textbf{[Sco72]}, carried out in Lean 4 against mathlib and including the March 1972 Milner correction in \textbf{[Sco72]} (pp.~135--136).
Scott's paper develops a model for \(\lambda\)-calculus from a topological starting point. He defines \emph{injective} \(T_0\)-spaces -- those with a strong extension property for continuous maps -- and shows that they are exactly the \emph{continuous lattices}: complete lattices whose Scott topology is determined by the order via the way-below relation (\(\ll\)). On this foundation he studies projections, retractions, products, function spaces, and inverse limits. The capstone (Theorem 4.4) constructs an inverse limit \(D_\infty\) of function-space approximants and proves \(D_\infty \cong [D_\infty \to D_\infty]\), yielding a purely mathematical model for Church's untyped \(\lambda\)-calculus.
Our development formalizes \textbf{43 numbered results} from Scott's Sections 1--4 (Propositions, Corollaries, Lemmas, and Theorems), each as a sorry-free Lean theorem, together with supporting infrastructure (step functions, the \(\Uparrow a\) basis of Scott opens, Milner's coarser-than-Scott hypothesis, the function-space tower, and the \(i_\infty\)/\(j_\infty\) pair). The formalization is \textbf{classical} (uses \texttt{Classical.choice} transitively) and follows Scott's proof dependency order. Where the Lean proof required choices not visible in the original -- or where dead ends were encountered -- we record detailed notes in Section 5. All proofs check with the standard footprint \(\texttt{[propext, Classical.choice, Quot.sound]}\).
A minimal set of equations defines the variety, shown complete and independent by technical proofs and examples.
abstractclick to expand
In this manuscript, we provide an independent equational basis for the variety of reflexive Nelson algebras, a generalization of the variety of SNA-algebras. The proof of this result relies on a substantial number of technical arguments and computational examples. The result complements a broader study of reflexive Nelson algebras by showing that the variety admits an independent equational axiomatization.
Bi-neighborhood semantics for CLoN extensions supports deontic logics that accommodate dilemmas without trivialization.
abstractclick to expand
In this paper we will present neighborhood semantics for non-normal modal extensions of $\clon$, which is a sublogic of {\sf FDE}. Our framework is built upon earlier work on {\sf FDE}-based non-normal modal logics and employs two different neighborhood functions for each modal operator. Despite being a logic with a very weak negation operator, we will show that with the right definition of the rejection sets of the modal operators, we can validate non-trivial axioms that contain the weak negation operator. The philosophical aim of our approach is to construct the basis for deontic logics that are able to accommodate both the usual deontic principles and moral dilemmas, without resulting in trivialization of the system.
Fundamental logic is a non-classical logic based only on the introduction and elimination rules for conjunction, disjunction, negation, and the quantifiers in a Fitch-style natural deduction system. In this paper, we attempt to obtain a better understanding of fundamental logic and its semantics through the lens of modality. Using modal logic, we develop means of mutual understanding between the fundamental logician, on the one hand, and the orthologician and intuitionistic logician, on the other: we prove that the G\"odel-McKinsey-Tarski (GMT) translation of intuitionistic logic into the classical modal logic $\mathsf{S4}$ is a full and faithful embedding of fundamental logic into the orthological version of $\mathsf{S4}$; that the Goldblatt translation of orthologic into the classical modal logic $\mathsf{KTB}$ is a full and faithful embedding of fundamental logic into an intuitionistic version of $\mathsf{KTB}$; and that the GMT translation is a full and faithful embedding of intuitionistic logic into a modal extension of fundamental logic.
Unified argument extends Gödel's second incompleteness theorem to ω-models and β_n-models while tying definability to soundness via inductio
abstractclick to expand
In this note, we give some generalizations of G\"{o}del's second incompleteness theorem and study their surroundings. We revisit it from two perspectives. One perspective is the relationship between the definable complexity of a theory and unprovability of its soundness. We clarify the relationship between this perspective and induction axioms. We also determine the logical strength of Craig's trick, which is important for studying the definability of a theory, from the point of view of reverse mathematics. The other perspective is semantic incompleteness. The second incompleteness theorem may be seen as the unprovability of the existence of a model. It is known that `model' is replaced with `$\omega$-model' or `$\beta_n$-model'. We give a new and unified proof of the $\omega$-model and $\beta_n$-model versions of the incompleteness theorem.
The solutions of algebraic differential equations in certain valued differential fields, including the differential field of transseries, can be analyzed using a Newton diagram method. In this paper, we show that (eventual) equalizers, a crucial part of this process, can be obtained uniformly and definably from the coefficients of the input differential polynomials. We also obtain similar definability results for a certain compositional conjugation which is used repeatedly as an intermediate simplification step.
A modified Mitchell construction using random algebra shows the new pattern is compatible with Rado's Conjecture.
abstractclick to expand
Rado's Conjecture (RC) is a compactness principle for a certain class of partial orders, namely trees $T$ of height $\omega_1$ without cofinal branches, postulating that a partial order $P$ from this class can be decomposed into at most countably many antichains if and only if all its suborders of size $\omega_1$ can be decomposed into at most countably many antichains. Rado's Conjecture is thus an uncountable version of Mirsky's theorem asserting that for every natural number $n$, every infinite partial order $P$ can be decomposed into at most $n$ many antichains if and only if all its finite suborders can be decomposed into at most $n$ many antichains. Todorcevic showed that RC is consistent modulo a strongly compact cardinal. RC implies $2^\omega \le \omega_2$, and has powerful consequences such as the Singular Cardinal Hypothesis, the failure of $\square(\kappa)$ for every regular $\kappa \ge \omega_2$ (and hence in particular the Projective Determinacy), and the Strong Chang Conjecture. It is also known that it is incompatible with Martin Axiom. We show that RC is consistent with $2^\omega = \omega_2$ and the cardinal invariants in Cichon diagram corresponding to forcing with the random algebra, i.e., $\mathfrak{d} = \omega_1$, $\mathrm{cov}(\mathcal{N}) = \omega_2$, $\mathrm{non}(\mathcal{N}) = \omega_1$. This provides a new pattern of cardinal invariants known to be consistent with RC. To prove the theorem, we first observe that random algebras do not specialize non-special trees of height $\omega_1$ without cofinal branches. Then we use the random algebra $\mathcal{B}_\kappa$ for a strongly compact $\kappa$ to define a new version of Mitchell forcing which yields the required result.
The edge set of the random bipartite graph supplies a simple ℵ₀-categorical counterexample.
abstractclick to expand
Casanovas and Potier proved that algebraic quantification preserves stability of formulas. They also gave a nonsimple example, answering a question of Laskowski, showing that the algebraicity hypothesis cannot simply be replaced by NFCP, and asked whether a similar example exists in a simple theory. We give such an example in elementary form. The edge-set structure of the random bipartite graph has two definable equivalence relations, both stable and NFCP, whose relational composition has the order property. The resulting theory is simple and $\aleph_0$-categorical. We also prove a formal sharpness observation: every formula in every first-order theory is an existential composition of two stable NFCP formulas algebraic in the two outer variables. Consequently, closure of stable NFCP formulas under this composition characterizes stability of the whole theory.
The containment and implication are proved using cycle-removal on classes defined by finitely many forbidden weakly embedded substructures.
abstractclick to expand
We give applications of the properties $\mathrm{NSOP}_{r}$ for non-integer values of $r$ to problems on the original hierarchy $\mathrm{NSOP}_{n}$ for integer values of $n$.
We first show that the properties $\mathrm{NSOP}_{r}$, previously defined for real values $r \geq 3$, are even well-defined for real values $r \geq 2$, showing that $\mathrm{NSOP}_{2} \subseteq \mathrm{NSOP}_{r}$ for our original definition of $\mathrm{NSOP}_{r}$ even when $2 < r < 3$. As a consequence, newness of all of the well-defined properties $\mathrm{NSOP}_{r}$ for non-integer $r$ would negatively resolve the problem of whether $\mathrm{NSOP}_{2}$ is equal to $\mathrm{NSOP}_{3}$.
We then prove an approximate alternative between two possibilities: (1) that in extending Shelah's original $\mathrm{NSOP}_{n}$ hierarchy for integers $n \geq 3$ to the $\mathrm{NSOP}_{r}$ hierarchy for reals $r > 2$, we really did introduce new classification-theoretic properties, and (2) that $\mathrm{NSOP}_{n+1} \cap \mathrm{NTP}_{2} = \mathrm{NSOP}_{n} \cap \mathrm{NTP}_{2}$ for integers $n \geq 3$, which would resolve a central open problem in classification theory. More precisely, we give a rigorous sense in which (1) can fail on particularly general grounds, and then show that if (1) fails for these general reasons, (2) must be true.
Finally, we apply cycle-removal techniques from the theory of the properties $\mathrm{NSOP}_{r}$ for real-values of $r$ to make progress on the question of whether $\mathrm{NSOP}_{2}$ is equal to $\mathrm{NSOP}_{3}$. We (a) show that if $\mathcal{H}$ is a hereditary class of structures defined by finitely many forbidden weakly embedded substructures, if every theory whose models have age $\mathcal{H}$ has $\mathrm{SOP}_{2}$, then every theory whose models have age $\mathcal{H}$ has $\mathrm{SOP}_{3}$, and (b) observe that we cannot replace $\mathrm{SOP}_{2}$ with $\mathrm{TP}$ here.
Kalman-style functors equate their categories to the hyper algebras of each logic, with hyper swap structures as representatives.
abstractclick to expand
In a previous paper, we introduced the notion of hyper swap structures, a novel class of hyperalgebras that naturally generalizes swap structures semantics. In this paper we introduce the concept of hyper Boolean algebras based on Morgado hyperlattices, proving some basic properties. From this, we show that several paraconsistent logics in the hierarchy of Logics of Formal Inconsistency (LFIs) can be naturally characterized in terms of hyper swap structures semantics generated by hyper Boolean algebras. Finally, for each of these LFIs we obtain a Kalman-style functor which establishes an equivalence between the category of hyper Boolean algebras and a category of hyper algebras for the corresponding LFI having the hyper swap structures as representative objects.
In this partially expository paper, we present a novel construction of differentially closed fields of characteristic $0$: Let $\mathcal{K}_{\mathrm{dense}}$ be the differential ring of all meromorphic functions whose domain is a (not necessarily connected) dense open subset of $\mathbb{C}$ modulo agreement on dense open sets (i.e., $f$ and $g$ are considered equal if there is a dense open $U \subseteq \mathbb{C}$ such that $f|_U = g|_U$). We show that every ring ideal of $\mathcal{K}_{\mathrm{dense}}$ is a differential ideal and that for every maximal ideal $\mathfrak{m}$, the quotient $\mathcal{K}_{\mathrm{dense}}/\mathfrak{m}$ is a differentially closed field. We also show that $\mathcal{K}_{\mathrm{dense}}/\mathfrak{m}$ is saturated and has cardinality of the continuum, implying that any two such quotients are isomorphic as differential fields.
We then discuss how to motivate this construction in terms of set-theoretic forcing, Boolean-valued models, and $\neg\neg$-sheaves on $\mathbb{C}$, taking the opportunity to present an impressionistic expository account of these ideas.
Finally, we discuss some immediate generalizations of this construction involving the real and $p$-adic numbers and ask some questions about them.
The axiom of choice has divided the foundations of mathematics for over a century, but the distinction between classical and constructive proofs has remained a philosophical and methodological one. We use Lean 4's kernel-level tracking of axiom dependence to show that the axiom of choice has a measurable geometric correlate in proof space that obeys a one-parameter mixture law and has operational consequences for neural theorem provers. To do this, we partition $471{,}260$ declarations of Mathlib by transitive dependence on the axiom of choice and represent a filtered population of $42{,}355$ traced theorems by their sequences of tactic invocations. We use the constructive proofs in this dataset to train a self-supervised proof encoder and show that when using it to measure classical proofs, three complementary measurements (anomaly score, reconstruction loss, and density-superlevel containment) exhibit a common decline with the proof's distance from the axiom in the dependency graph, from sharp separation at the shallow boundary (AUC $0.847$ at distance $2$) to indistinguishability at distance~$9{+}$. Robustness controls show that the signature survives length, file, author, and topic controls, and replicates under full-source encoders trained on normalised proof source. Operationally, we show that on an evaluation sample of $251$ Mathlib theorems, Lean's \texttt{aesop} tactic solves constructive theorems at $13\times$ the rate of classical ones, and a neural-guided hybrid using the ReProver tactic generator compresses the gap to $5\times$. The geometric anomaly score predicts \texttt{aesop} failure beyond proof length, providing an operational link between the geometric signature and prover performance.
A transfer principle turns oracle-uniform lower bounds into exact bounds on infinitary orbit definability for rank-(m+1) trees.
abstractclick to expand
In earlier work we constructed, for each computable ordinal $\alpha$, a computable tree of rank $\alpha+1$ whose strong degree of categoricity is $\mathbf{0}^{(2\alpha)}$ for finite $\alpha$ (and $\mathbf{0}^{(2\alpha+1)}$ for infinite $\alpha$), and showed these degrees are optimal. Those results are lightface: they concern computable copies and Turing degrees of isomorphisms. In this paper we determine the boldface content of the construction. We isolate a simple transfer principle showing that a degree-of-categoricity lower bound which holds \emph{uniformly relative to every oracle} defeats $L_{\omega_1\omega}$-definability of automorphism orbits outright, and we verify that our construction has this uniformity. Writing $\A_{m+1}$ for the isomorphism type of our rank-$(m+1)$ trees ($m\geq 1$ finite), we conclude that $\A_{m+1}$ has Scott rank exactly $2m+1$ in the sense of Montalb\'an, and that its Scott sentence complexity is one of $\Sin{2m+1}$, $\dSin{2m+1}$, or $\Pin{2m+2}$. For rank $2$ we carry out a complete Scott analysis: the orbit of the level-one nodes of infinite degree is $\Pin{2}$- but not $\Sin{2}$-definable, and $\SSC(\A_2)=\Pin{4}$ exactly, witnessed by a computable $\Pc{4}$ Scott sentence. We conjecture $\SSC(\A_{m+1})=\Pin{2m+2}$ for all finite $m$ and reduce the conjecture to a single back-and-forth substitution lemma. These results begin a classification of the Scott sentence complexities of trees, in analogy with the Gonzalez--Rossegger analysis of linear orders, and connect the $2\alpha$-jump phenomenon in degrees of categoricity to Scott spectral gap questions of Harrison-Trainor and Kim.
Extends Lenstra's ε_0 result by showing the full sequence forms the next quadratic closures before the first transcendental ordinal.
abstractclick to expand
In 1976, J. H. Conway introduced Nim arithmetic which establishes an algebraically closed field structure over the class of ordinals and proved that the first transcendental ordinal is $\omega^{\omega^\omega}$. The problem of finding the next transcendental ordinal is still open. Two years later, H. Lenstra proved that $\varepsilon_0$ is the next quadratically closed field ordinal. In this paper, we prove that $\{\varepsilon_\alpha \mid \alpha \leq \omega^{\omega^\omega} \}$ are the next quadratically closed field ordinals.
For every k a maximal frame exists whose shortest coherence violation has length exactly 2k+2, so no bounded fragment suffices.
abstractclick to expand
This theoretical note studies the finite axiomatizability of strict majority reasoning in finite social decision frames. Moss and Pedersen (2026) <doi: 10.48550/arXiv.2606.23853> introduce a coherence criterion that characterizes exactly when qualitative majority judgments are representable by a finitely additive measure. The question addressed here is whether that coherence criterion can be replaced, in the finite setting, by any bounded finite fragment. We prove that it cannot. For every $k\ge 1$, we construct a maximal standard frame whose shortest coherence violation has length exactly $2k+2$. Hence there is no uniform finite bound on the incoherence index of social decision frames, resolving Conjecture 5.7 stated by Moss and Pedersen (2026). The construction is geometric, in the sense that it proceeds via orthogonality and dimension in rational vector spaces, and self-contained: it isolates a symmetric family of half-sized voting blocs and extends it to a maximal frame in which every shorter balanced obstruction is excluded. Along the explicit infinite sequence of universe sizes obtained in the construction, this also establishes the middle-layer family predicted by Conjecture B.25 by Moss and Pedersen (2026). Together with the soundness and completeness theorem for the Moss-Pedersen minimal logic for strict majorities, this establishes that measurable social decision frames are not finitely axiomatizable in that language.
In algebras with full closure the recursion realizes that small cardinals stay cardinals while allowing uncountable choice fragments.
abstractclick to expand
This work presents a transfinite version of the bar-recursion in the context of classical realizability models for set theory. Bar-recursion has been previously used to obtain realizability interpretations of countable choice and dependent choice, and was employed by Krivine to realize the continuum hypothesis in classical realizability. In this paper, we introduce a transfinite variant of bar-recursion and use it to construct realizability models validating uncountable fragments of the Axiom of Choice. Moreover, our construction reveals that this generalized bar-recursion is related to preservation of cardinals. To show this, we define an analogue of the forcing notion of $\kappa$-closure for classical realizability algebras that we call $\kappa$-fully-closed. We show that, in realizability algebras satisfying the $\kappa$-full-closure property, generalized bar-recursion realizes that any cardinal up to $\kappa$ admits a representative in the realizability model which remains a cardinal.
Galvin ideals are introduced as the intermediate step between Ramsey ideals and semiselective ideals on infinite sets.
abstractclick to expand
We primarily study several combinatorial properties of Ramsey-type ideals on countably infinite sets. Specifically, we show new combinatorial characterizations of Ramsey ideals through various partition and convergence properties. Furthermore, we analyze ideal versions of some relevant high-dimensional Ramsey-type theorems, in order to research ideals related to finite colorings of barriers on the natural numbers as well as ideals associated with finite partitions of any family of finite subsets of the natural numbers. In particular, Galvin ideals are introduced as an intermediate combinatorial concept between Ramsey ideals and semiselective ideals.
The link improves earlier results on generalized probability functions and raises new questions.
abstractclick to expand
We establish a connection between the part-whole principle and the quantity $\text{ded }\kappa$ -- a generalized cardinal characteristic related to the number of Dedekind cuts of a linear order. As consequences, we improve a result of Mancosu and Massas on generalized probability functions and propose some questions.
The correspondence yields characterizations of substructures via lattice preorders and of congruences via closed dual sets.
abstractclick to expand
It is well known that, in Boolean algebras, the notions of precontact relation, quasi-modal operator, and subordination relation are interdefinable. In contrast, within the setting of distributive lattices, this equivalence holds only between quasi-modal operators and subordination relations, but not with precontact relations. In this paper, we study the class of bounded distributive lattices equipped with a precontact relation, referred to as precontact lattices. We also examine how conditions imposed on the precontact relation correspond to first-order properties in the Priestley dual. In addition, we characterize precontact substructures and strong precontact sublattices of precontact lattices in terms of a suitable lattice preorder. Finally, we introduce a notion of precontact congruence and identify the corresponding closed sets in the dual space.
Results link Ax's field theory and monadic stability in groups to efficient algorithms for logical properties.
abstractclick to expand
We prove the following results.
1. First order model checking is fixed-parameter tractable on the class of finite fields, as a corollary of results of Ax on the theory of (pseudo)finite fields.
2. Every hereditary graph class first order definable in the class of finite groups is monadically stable, and thus has fixed-parameter tractable first order model checking.
3. Monadic second order model checking is not slicewise polynomial on the class of cyclic groups of prime-power order, unless E = NE.
We show that if a group $G$ admits an action with no algebraicity then all of its mixed identities are singular. Previously, such groups were only known to be lawless by a theorem of Ab\'ert. Our result confirms, in particular, a conjecture of Bodirsky, Schneider, and Thom for a large class of oligomorphic permutation groups. It thereby not only subsumes numerous results from the literature in a simple uniform theorem, but also settles the question for prominent groups for which the conjecture was an open problem, such as the automorphism group of $(\mathbb{Q}; <)$. Outside the oligomorphic context, it moreover applies to much-investigated groups, e.g. to Thompson's groups $F$, $T$, and $V$, to Grigorchuk's group, and to the homeomorphism groups of any manifold of dimension $\geq 1$. More generally, we prove that all mixed identities of a group $G$ are singular as long as $G$ has an action satisfying certain geometric conditions. This additionally covers the infinite-dimensional general and projective linear groups, recovering e.g. results of Bradford, Schneider, and Thom.
The equivalence lets Gandy selection deliver uniform indices for recursive unions of feedback semi-computable sets and supports effective ch
abstractclick to expand
We give an account of Kleene's Type 2 recursion theory modelled on Turing machines. We apply this account to observe that the feedback computation of \cite{AFL2020} is an example of Kleene Recursion in $^2\mathsf{E}$. An application of Gandy Selection in the feedback setting solves questions there raised on uniformly finding indices for recursive unions {\em etc.} of feedback semi-computable sets; further it allows for effective choice and other principles.
This places it at the complexity of complete sets from infinite game determinacy, all inside analysis.
abstractclick to expand
We outline a theory of type 2 recursion for Infinite Time Turing Machines {\em \`a la Kleene}. We establish a connection between classical descriptive set theory and ittm theory, by calculating the complexity of its halting problem as exactly that of a complete $\Game \Sigma^0_3$ (or $G_{\delta\sigma}$) set. This mirrors exactly what Kleene, Moschovakis {\em et al.} achieved for Kleene's type 2 recursion and $\Sigma^0_1$ (or Open) Determinacy.} We ascertain the least ordinal which is not generalised recursive in this sense, and its characterisation {\via}a concept of {\em infinite nestings} in G\"odel's constructible hierarchy. The results do not require large cardinal axioms, and are all provable within analysis.
We study the ring of Puiseux polynomials with integer coefficients. We prove notably that the order given by the leading coefficient is definable without parameters in the language of rings. This answers a question of R. Robinson.
A new characterization supplies an explicit procedure that works inside Bishop-style constructive mathematics.
abstractclick to expand
In this work we study two classical problems of (numerical) linear algebra: (i) solving linear systems and (ii) computing eigenvectors, within a constructive framework. Numerical accuracy and indeterminacy are naturally incorporated through Bishop-style constructive mathematics. Our contributions include new results on Gauss-Jordan elimination and on approximating the rank of a matrix. Additionally, we introduce a novel method for constructing approximate eigenvectors, based on a previously unexplored characterization of singular matrices.
Khovanskii's theorem gives a Bezout-type upper bound for the number of isolated real solutions of a system of $n$ Pfaffian equations in $n$ variables in terms of three complexity parameters: the chain-degree $\alpha$, the degrees $\beta_i$ of the Pfaffian functions, and the order $s$ of the underlying Pfaffian chain. Despite its fundamental role in Pfaffian geometry and o-minimality, little is known about the sharpness of this bound.
We investigate the theorem from a parameter-by-parameter perspective. We show that its dependence on the chain-degree $\alpha$ is asymptotically sharp by constructing, for every $\alpha,s \in \mathbb{N}$, a Pfaffian function of format $(\alpha,1,s)$ with at least $\alpha^s$ nondegenerate real zeros. We also show that its dependence on the degrees $\beta_i$ is asymptotically sharp: for fixed $n$ and $s$, we construct Pfaffian systems having $\Omega_{n,s}(\beta^{n+s})$ regular common zeros, matching the order of growth predicted by Khovanskii's theorem as $\beta\to\infty$.
Frame insensitivity and canonical model maps let simpler languages borrow results from richer normal modal logics without re-proving accessi
abstractclick to expand
We develop general strategies for transferring soundness and completeness from more expressive modal languages to less expressive ones, unifying several existing notions of operator definability along the way. For soundness, we exploit semantic insensitivity: if a less expressive language is insensitive to a frame operation, soundness extends to the operation's closure of the original frame class. For completeness, restricting to relational semantics and languages with a single operator, we present strategies for relating the target logic's canonical model to that of a normal modal logic via a truth-preserving translation. Three of those dispense entirely with specifying an accessibility condition for the target logic, inheriting it from a normal modal logic instead.
Algebraic properties of these groups control which parts of the axiom of choice hold inside the associated permutation models.
abstractclick to expand
We prove several novel connections between properties of nonarchimedean groups and fragments of the axiom of choice which hold in their associated permutation model.
Weak scatter sentences evaluate more efficiently than standard ones, aiding bounded merge-width graphs.
abstractclick to expand
We prove a rank-preserving locality theorem for a syntactic variant of first-order logic, in the spirit of Gaifman's locality theorem and the rank-preserving locality theorem of Grohe, Kreutzer, and Siebertz. Our result allows for a weak form of scatter sentences, which can be evaluated more efficiently than usual scatter sentences considered in prior work. This is crucial in our application to graphs of bounded merge-width.
Inductive proofs can be represented by proof schemata, a formalism that represents infinite sequences of proofs by recursive definitions. Since proof schemata avoid the explicit application of induction rules, they admit novel applications, one of which is the realization of Herbrand's theorem in the presence of induction. In this paper, we develop a new type of proof schema based on point transition systems. For skolemized proof schemata without quantified cuts, so-called Herbrand systems, that is, schemata of Herbrand instances of quantified formulas, can be computed. Herbrand systems also allow the representation of schemata of Herbrand sequents, thereby realizing Herbrand's theorem for proof schemata. We compare proof schemata with cyclic proofs and define a transformation from a large class of cyclic proofs to proof schemata. Finally, we show that proof schemata based on point transition systems are capable of proving the 2-Hydra statement, a well-known example that is provable by the cyclic proof system CLKID\omega but not in LKID.
Its second-order language does not give it more power than first-order set theory.
abstractclick to expand
We argue that second order logic is a weaker form of set theory, despite the fact that the former is formalized in a second order langauge and the latter in a first order language. Along the way, we review the history of interactions between second order logic and set theory, as well as some modern trends.
UKN1 and UKN2 reinterpret a value as not known yet to create systems different from FDE and FDEe.
abstractclick to expand
Inspired by Nuel Belnap's "How a computer should think," which gave rise to the four-valued logic FDE, we contemplate, in this article, how a computer might think if we add a fifth value for unknowable or cannot be known. We devise two new five-valued logics, UKN1 and UKN2, called the logics of the unknowable. These are different from the five-valued logic FDEe of the FDE-family. The main difference is in the number of designated truth values. While FDEe takes two designated values, UKN1 and UKN2 have three. The four-valued reducts of these logics are also different from FDE. This is due to the fact that instead of taking one of the non-designated values as neither true nor false, as in FDE, we have interpreted this as not known yet. This value although denoted by the same letter $n$, behaves differently from its namesake in FDE.
Extending the two constraints to Henkin models produces low-level definability for natural language quantifiers via Feferman's theorem.
abstractclick to expand
This paper studies the definability of natural language generalized quantifiers. The semantics of generalized quantifiers are provided by a collection of subsets of the underlying domain. However, the generalized quantifiers appearing in natural language are definable either by first-order quantification or by cardinality notions. This paper provides an explanation for this observed phenomenon. The explanation is that the famous constraints of domain independence and conservativity, when extended to Henkin models, suffice to ensure low-level definability, namely $\Delta^1_1$-definability or at least $\Sigma^1_1$-definability; and in most cases this definability can be made to be bounded. This is basically a consequence of Feferman's Preservation Theorem, which Marker has provided a short model-theoretic proof of. Further, we verify that the paradigmatic cardinality quantifiers are indeed $\Delta^1_1$-definable for a reasonable choice of background theory. Finally, in many other cases, we show that this definability can be lowered to first-order definability.
We answer some questions regarding the mean value theorem and related results in constructive mathematics. The answers to these questions reveal interesting properties of the Mean Value Theorem, Law of Bounded Change, and Constancy Principle. We see that, in contrast to the Intermediate Value Theorem whose approximate analogue was shown to hold constructively by Frank, the natural approximate versions of these theorems fail to hold in neutral constructive mathematics. Our proof of this makes use of the existence of a topos in which the real numbers are in bijection with the naturals, which was shown by Bauer and the second author. Using Booij's notion of locators, we show that the aforementioned approximate analogues do hold in the presence of a small amount of countable choice, and also under suitable locator lifting hypotheses. We also show that an even weaker approximate analogue of the Mean Value Theorem holds in neutral constructive mathematics.
Belief revision is a process in which an agent begins to believe in something she previously did not. I begin the paper by presenting, based on (G\"ardenfors, 1998; Hansson, 1999), postulates for belief revision that constitute the basis of the AGM theory. I will then briefly show the semantics of a modal logic introduced in (van Ditmarsch, 2005), which I call `$P$'. This logic formalizes static epistemic states and has greater expressive power than AGM in doing so because it captures the quantitative notion of "degrees of conviction". The third step is to introduce revision operators on $P$ and, mostly following (van Ditmarsch, 2005), obtain the Dynamic Epistemic Logic (DEL) I call `$P*$'. It models processes of belief revision in several ways. Original results are presented in the following two sections. The first one of these sections revolves around a formalization of AGM postulates within $P*$ by proving some theorems related to the satisfaction of those postulates by revisions defined in $P*$. The last section features an analysis of $P*$'s revisions that go beyond the mere satisfaction of postulates. I compare their formal behavior with respect to some philosophical criteria. At last, I conclude that the functions presented in (van Ditmarsch, 2005) are not good formalizations of the philosophical intuition behind AGM. Instead, it is captured by the function $*^0$ originally defined in this paper (but highly inspired by (van Benthem, 2007)). An implementation of this function is also provided.
Equivalence via projective Fraïssé limits shows the universal pseudo-solenoid homeomorphism group has non-metrizable universal minimal flow.
abstractclick to expand
We define a combinatorial property of a projective Fraisse category which we call the \emph{approximate Ramsey property}. Let $F$ be a continuum, $G$ a closed subgroup of the homeomorphism group of $F$, and $\mathbb{F}$ the limit of projective Fraisse category $\mathcal{F}$ such that $\textrm{Aut}(\mathbb{F})$ is dense in $G$. We prove that $\mathcal{F}$ has the approximate Ramsey property if and only if $G$ is extremely amenable. We prove that the group of homeomorphisms of the universal pseudo-solenoid has non-metrizable universal minimal flow.
Expanding products of modal logics are bimodal logics obtained from the combination of a `horizontal component' logic and a `vertical component' logic, lying between the fusion and the Cartesian product of the two logics. Gabelaia et al. showed that expanding products are often decidable when the first component is Noetherian, although their methods are semantical and do not yield complete axiomatisations. They do, however, propose a candidate, dubbed the expanding commutator of the two logics and known to be complete in many `non-Noetherian' cases. In this paper, we consider various expanding products of modal logics whose vertical component is $\sf GL$. We show that the standard axiomatisation is complete when the horizontal component is either $ {\sf K4}$ or $ {\sf GL} $, but incomplete when it is ${\sf Grz}$ or any logic between ${\sf K4.3}$ and ${\sf Grz.3}$, thus yielding a partial solution to a question posed by Gabelaia et al. more than two decades ago.
Wild automorphism conjecture holds for dynamics built from self-trivialising equivariant fibrations.
abstractclick to expand
Inspired by the model theory of difference fields in characteristic zero, a class of automorphisms of an algebraic variety, here called compound fundamental isotrivial, is introduced. These are algebraic dynamical systems that are built up via a finite sequence of equivariant fibrations from (possibly nonautonomous) algebraic dynamics which trivialise after base extension over themselves. Every wild automorphism of an abelian variety is compound fundamental isotrivial. Conversely, it is shown that the only irreducible projective varieties admitting a wild automorphism that is compound fundamental isotrivial are the abelian varieties. That is, the wild automorphism conjecture of Reichstein, Rogalski, and Zhang is here proven for compound fundamental isotrivial dynamics. Along the way, a counterexample to the naive generalisation of the conjecture to the nonautonomous setting of $\sigma$-varieties is provided.
We present a machine-checked completeness theorem, in Lean 4, for the hybrid logic $L(\forall)$: propositional modal logic with nominals, the satisfaction-style binder $\forall$, and the box modality. (Machine-checked completeness for basic hybrid logic, without binders, was pioneered by Asta Halkj\ae r From in Isabelle/HOL.) We build on Alex Oltean's 2023 Lean 4 formalization, which mechanized the syntax, semantics, Hilbert-style proof system, and soundness following Blackburn's Hybrid Completeness (1998), but left completeness unfinished. Finishing it requires manufacturing fresh names at two structurally different points, and our central finding is that they call for two different tools. (1) The root witnessed maximal consistent set, built by an extended Lindenbaum construction, needs at each step a nominal fresh for the whole set; the right tool is structural freshness: extend the language so an infinite supply of nominals is reserved by construction. We survey the design space (Oltean's odd/even encoding inside $\mathbb{N}$, the disjoint-sum $N \oplus \mathbb{N}$ parameterization suggested by Bud Mishra, and From's synthetic-completeness frameworks) and explain the encoding we adopt. (2) The witnessed $\Diamond$-successor of a maximal consistent set cannot be obtained this way: its canonical box-reduct provably mentions every nominal, so no reserved name is fresh. Here the right tool is one Oltean chose but left incomplete: an existence-lemma Henkin construction drawing each witness from the predecessor's witnessedness through a fresh state variable; we complete it with a data-carrying witness accumulator and a compactness argument. The theorem $\Gamma \models \varphi \to \Gamma \vdash \varphi$ is fully formalized: the development is sorry-free, and #print axioms reports only propext, Classical.choice, and Quot.sound. We port the development to Lean v4.30.0 / mathlib v4.30.0.
The predicate jst Pp derives consequences that match the Brouwer-Heyting-Kolmogorov reading of intuitionistic axioms under stated restrictio
abstractclick to expand
Working within Constructive Morse Set Theory (CMST), we introduce axioms for a new notion, jst Pp, intended to capture what it means for P to prove, or justify, p under the BHK interpretation of intuitionistic logic. Since it makes no distinction between terms and formulae -- every term is also a formula, and vice versa -- CMST is well suited to our axiomatic development of justification theory within set theory itself. After stating our axioms for jst Pp, we derive many consequences thereof. In particular, we show that (with certain restrictions) our axioms for jst Pp align with the intended BHK interpretations of the axioms of intuitionistic logic.
A definable Birkhoff representation decides which Heyting algebra equations hold on maximal subsets.
abstractclick to expand
We investigate distributive lattices and Heyting algebras definable in o-minimal structures. We give a complete description of one-dimensional bounded distributive lattices definable over an o-minimal structure expanding a real-closed field, and prove a definable analogue of Birkhoff representation, which we use to classify all one-variable equations in the language of Heyting algebras with respect to whether they can be satisfied in a maximal-dimension subset of a given algebra.
Effective decomposition turns higher-arity relations into binary ones by viewing them as multivalued function graphs.
abstractclick to expand
We give a new and elementary construction of primitive positive decomposition of higher arity relations into binary relations on finite domains. Such decompositions come up in applications to constraint satisfaction problems, clone theory and relational databases. The construction exploits functional completeness of 2-input functions in many-valued logic by interpreting relations as graphs of partially defined multivalued 'functions'. The 'functions' are then composed from ordinary functions in the usual sense. The construction is computationally effective and relies on well-developed methods of functional decomposition, but reduces relations only to ternary relations. An additional construction then decomposes ternary into binary relations, also effectively, by converting certain disjunctions into existential quantifications. The result gives a uniform proof of Peirce's reduction thesis on finite domains, and shows that the graph of any Sheffer function composes all relations there.
The weak equivalence class of the quasi-regular representation then determines the subgroup up to conjugacy among self-commensurating ones.
abstractclick to expand
If $\Lambda$ is a non-amenable bi-exact group and $\Lambda \hookrightarrow \Gamma$ is an existential embedding, then each of the intersections $\Lambda \cap g \Lambda g^{-1}$ for $g$ a member of $\Gamma \backslash \Lambda$ is amenable. This in conjunction with work of Bekka and Kalantar demonstrates that in this situation, the weak equivalence class of the quasi-regular representation $\lambda_{\Gamma/\Lambda}$ determines $\Lambda$ up to conjugacy among the self-commensurating subgroups of $\Gamma$.
The lazy log-tensor monad delivers differentiable training that beats LTN and DeepProbLog on MNIST addition while keeping the framework para
abstractclick to expand
Neurosymbolic semantics is fragmented: classical, fuzzy, probabilistic and neural systems each define truth by their own inductive rules. NeSyCat, extending ULLER, subsumes them under a single inductive definition of truth, parametric in a strong monad and an aggregation structure on truth-values. NeSyCat has so far lacked an account of predicates and functions learned by neural networks.
We provide NeSyCat Torch as the missing link and interpret computational symbols via neural networks, implementing the framework in probabilistic programming and tensor-based backends. We use the distribution monad for reference semantics and metric evaluation, and complement it by a monad for numerically stable, differentiable training: the lazy log-tensor monad over the log-semiring. For efficient training in batches, we furthermore employ a batch monad. The axioms are the source code: written once in monad-based do-notation, monadic bind performs marginalisation, lazily pruning unneeded branches.
On MNIST addition, our HaskTorch, JAX, and PyTorch implementations outperform LTN and DeepProbLog in speed and accuracy, while achieving nearly the accuracy of DeepStochLog. However, unlike DeepStochLog, we stay in a uniform framework that applies to many first-order NeSy approaches. Namely, the construction is parametric in the monad; instantiating it with, e.g., the Giry monad extends the approach to continuous probability (working out a neural representation here is left for future work).
We study monadic dependence of binary relational structures including at least one antisymmetric relation.
Our cornerstone result gives sufficient conditions for proving that a structure is monadically dependent by only considering some of its reducts, assuming they are structurally well-behaved and compatible enough. As an application, we consider some reorientation rules preserving monadic dependence of binary structures, as well as replacement of one antisymmetric relation with bounded independence number by another. Then, we apply our main (technical) result to the study of twin-width in two ways.
First, generalizing the fact that twin-width boundedness is equivalent to being expandable by a linear order into a monadically dependent class, we prove that it is also equivalent to being expandable by an oriented graph with bounded independence number (for instance by a poset with bounded width or by a tournament), and that FO-model checking is fixed-parameter tractable on such an expansion.
Second, we show delineation by twin-width for some new classes of oriented graphs, including oriented split graphs and local tournaments. In all these cases, we also obtain fixed-parameter tractability of FO-model checking.
This article establishes the completeness of an axiomatization for the robust safety of dynamical systems with polynomial differential equations on bounded time horizons. Safety properties of robust systems are uniformly reduced to a sound axiomatization of polynomial invariants, resulting in reliable logical proofs of correctness. Approximate decidability results are also established: there is a computable algorithm such that, given any perturbation parameter $\delta$, it either produces a symbolic proof of robust safety (hence correctly decides the dynamical system to be robustly safe), or correctly decides that the system is not robustly safe under a perturbation of level $\delta$. In contrast to earlier works, this article crucially leverages results from subanalytic geometry to retain a level of exactness, thereby establishing positive results of provability/decidability allowing for arbitrary bounded (semialgebraic) initial/post conditions even without positive separation at their (topological) boundaries. This enables the generation of proofs of inductive safety beyond finite time horizons for general hybrid dynamical systems.
The result finishes classifying all classical model-theoretic dividing lines under straight and poset definability.
abstractclick to expand
Different kinds of definable patterns in the models of a first-order theory, such as the order property, the tree property, or the ($n$-)strict order property, allow us to distinguish theories according to their logical complexity. The complexity distinctions given by these definable patterns play a central role in model theory. However, a rigorous definition of the notion of a model-theoretic patterning property has yet to be established.
We start by discussing different proposals from the literature for making the notion of a model-theoretic patterning property rigorous. Some examples will include the straight definability of Shelah, which will describe properties definable by a pattern of consistency and inconsistency in a formula and its negation, and the poset definability of Garcia and Mennuni, covering properties definable by interpreting a partial order embedding a given poset. We will also introduce a higher-arity version of straight definability.
In our first main result, we will answer open questions of Bailetti and Garcia-Mennuni, showing that the $n$-strict order property $\mathrm{SOP}_{n}$ is straightly definable and poset definable even for integers $n \geq 4$. This will complete the categorization of all of the classical classification-theoretic properties as straightly definable.
Our other main result will concern properties that are straightly definable without negation: the positively straightly definable properties defined by Bailetti. We will show using Saracino's theorem and results of Bodirsky, Bodor and Marimon that, in any countably categorical theory, implications between positively straightly definable properties must be exhibited at the level of $\exists\forall$-formulas. This will have special consequences under the assumption that $\mathrm{SOP}_{2}$ is equal to $\mathrm{SOP}_{3}$.
Kuratowski's pair is one case of a uniform construction that stays inside typed sets.
abstractclick to expand
In 1921, Kuratowski gave the now-standard definition of ordered pair in the context of set theory. This paper studies the problem of defining ordered tuples as sets in the hierarchy of simple types, of which Kuratowski's construction is a special case.
Non-algebraic examples with finite Morley rank would serve as counterexamples to the algebraicity claim for simple groups
abstractclick to expand
We review the current state of the Cherlin-Zilber Algebraicity Conjecture on simple groups of finite Morley rank, which states that every such group is the group of $K$-rational points of an algebraic group for some algebraically closed field $K$. We will explain the relevance of sharply 2-transitive groups as a potential source of counterexamples and how the Burnside problem necessarily comes into the picture.
n-productive maximal eventually different families separate distinct levels of maximality in ZFC and forcing extensions.
abstractclick to expand
A maximal eventually different family is called $n$-productive if the product family $\mathcal{F}^n$ is still maximal. We construct closed $n$-productive families separating these strengthenings of maximality at every $n \geq 1$. Furthermore, we show how to force and construct an even stronger type of $\mathcal{I}_0$-productive family and discuss the relation of productivity to Van Douwen families.
A Markov Logic Network (MLN) is a probabilistic relational model used in Statistical Relational Artificial Intelligence for defining a probability distribution on the set of possible worlds with domain $D$ for an arbitrary finite domain $D$. An MLN consists of soft constraints with associated weights which are nonnegative real numbers. In this study we consider a language speaking about a property $P(x)$ and a relation $R(x, y)$. We consider an MLN for which every Boolean combination of $P(x)$ and $R(x, y)$ is a soft constraint (with associated weight). Let $n$ denote the size (cardinality) of the domain. We show that, for every choice of weights, if the weights are scaled by $1/n$ then, for every first-order sentence $\varphi$, the probability that $\varphi$ holds tends to either 0 or 1 as $n \to \infty$; that is, a 0-1 law for first-order logic holds. Morover, the limit probability does {\em not} depend on the weights. If we instead use the standard semantics of MLNs, in the case of which the weights are {\em not} scaled, then the limit behaviour is more complicated and {\em depends} on the weights. With unscaled weights we get 7 qualitatively different cases which depend on the weights. In some cases we have a 0-1 law for first-order logic, in some cases not, but we may still have a convergence law. The influence of the weights on the asymptotic probability of a first-order sentence may be in the form of a sudden ``phase transition'' from one of the 7 cases to another. The presence of a convergence law has positive implications for inference on large domains.
Mutual interpretability with WT, WD and R shows the new string theories are essentially undecidable.
abstractclick to expand
We introduce several very weak first-order theories of unary concatenation of dyadic strings and investigate their relationships to other previously studied veey weak first-order theories, namely the theory WT of binary trees of Kristiansen and Murwanashyaka, the theory WD of binary concatenation of Murwanashyaka, and Robinson's very weak arithmetic R. We prove that all these theories are mutually formally interpretable with the theories of unary concatenation studied in the paper, thus establishing essential undecidability of the latter. In the process we show that binary concatenation is first-order definable from unary concatenation modulo the presence of the initial segment relation plus either the end segment relation or the inverse operation on words, thus giving a positive solution to a problem posed by Karlov.
full image
