We develop a selective filtration technique for the monadic Grzegorczyk and Gödel–Löb logics with the monadic Barcan formula, yielding that these logics have the finite model property. As a consequence, we obtain that $\mathbf {GL} \times \mathbf {S5}$ is product matching, and that $\mathbf {Grz} \times \mathbf {S5}$ is axiomatized by adding to the commutator $[\mathbf {Grz},\mathbf {S5}]$ the Gödel translation of the monadic Casari formula. This settles the question of finite axiomatization for two of the product logics listed in [13, p. 137] . As another consequence, we obtain that the one-variable fragments of the predicate Grzegorczyk and Gödel–Löb logics with the Barcan formula are Kripke complete (which contrasts the incompleteness of the full predicate logics).

Let M be the generic poset, defined as the Fraïssé limit of the class of finite posets. We show that every countably infinite poset A can be embedded with coinfinite image into M so that each automorphism of the image of A extends uniquely to an automorphism of M.

We show that in $L(\mathbb {R})$, assuming large cardinals in V, $\mathsf {HOD}{\parallel }\eta ^{+\mathsf {HOD}}$ is locally definable from $\mathsf {HOD}{\parallel }\eta $ for all $\mathsf {HOD}$-cardinals $\eta \in [\boldsymbol {\delta }^2_1,\Theta )$. This is a further elaboration of the statement “$\mathsf {HOD}^{L(\mathbb {R})}$ is a core model below $\Theta $” made by John Steel.

We study Doob’s Consistency Theorem and Freedman’s Inconsistency Theorem from the vantage point of computable probability and algorithmic randomness. We show that the Schnorr random elements of the parameter space are computably consistent, when there is a map from the sample space to the parameter space satisfying many of the same properties as limiting relative frequencies. We show that the generic inconsistency in Freedman’s Theorem is effectively comeager, which implies the existence of computable parameters which are not computably consistent. Taken together, this work provides a computability-theoretic solution to Diaconis and Freedman’s problem of “know[ing] for which [parameters] $\theta $ the rule [Bayes’ rule] is consistent” [4, p. 4], and it strengthens recent similar results of Takahashi [31] on Martin-Löf randomness in Cantor space.

We study the problem of distinguishing between two independent samples $\mathbf {G}_n^1,\mathbf {G}_n^2$ of a binomial random graph $G(n,p)$ by first-order (FO) sentences. Shelah and Spencer proved that, for a constant $\alpha \in (0,1)$, $G(n,n^{-\alpha })$ obeys FO zero-one law if and only if $\alpha $ is irrational. Therefore, for irrational $\alpha \in (0,1)$, any fixed FO sentence does not distinguish between $\mathbf {G}_n^1,\mathbf {G}_n^2$ with asymptotical probability 1 (w.h.p.) as $n\to \infty $. We show that the minimum quantifier depth $\mathbf {k}_{\alpha }$ of an FO sentence $\varphi =\varphi (\mathbf {G}_n^1,\mathbf {G}_n^2)$ distinguishing between $\mathbf {G}_n^1,\mathbf {G}_n^2$ depends on how closely $\alpha $ can be approximated by rationals:

• • for all non-Liouville $\alpha \in (0,1)$, $\mathbf {k}_{\alpha }=\Omega (\ln \ln \ln n)$ w.h.p.;

• • there are irrational $\alpha \in (0,1)$ with $\mathbf {k}_{\alpha }$ that grow arbitrarily slowly w.h.p.;

• • $\mathbf {k}_{\alpha }=O_p(\frac {\ln n}{\ln \ln n})$ for all $\alpha \in (0,1)$.

The main ingredients in our proofs are a novel randomized algorithm that generates asymmetric strictly balanced graphs as well as a new method to study symmetry groups of randomly perturbed graphs.

The notion of an existentially closed model is generalised to a property of geometric morphisms between toposes. We show that important properties of existentially closed models extend to existentially closed geometric morphisms, such as the fact that every model admits a homomorphism to an existentially closed one. Other properties do not generalise: classically, there are two equivalent definitions of an existentially closed model, but this equivalence breaks down for the generalised notion. We study the interaction of these two conditions on the topos-theoretic level, and characterise the classifying topos of the existentially closed geometric morphisms when the conditions coincide.

In this article, we present a formalization of spherically complete spaces, a fundamental notion in non-Archimedean functional analysis, using the Lean theorem prover (v4.31.0), building over Mathlib. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples, and non-examples such as the field $\textbf {C}_p$ of p-adic complex numbers. As applications, we formalize the notion of Birkhoff–James orthogonality, the Hahn–Banach extension theorem and the spherical completion for non-Archimedean Banach spaces.

In this article, we introduce novel variations on several well-known model-theoretic tree properties (TPs), and prove several equivalences to known properties. Motivated by the study of generalized indiscernibles, we introduce the notion of the $\mathcal {I}$-tree property ($ \mathcal {I}$-TP), for an arbitrary Ramsey index structure $\mathcal {I}$. We focus attention on the colored linear order index structure c, showing that c-TP is equivalent to instability. After introducing c-$\text {TP}_1$ and c-$ \text {TP}_2$, we prove that c-$ \text {TP}_1$ is equivalent to $\text {TP}_1$, and that c-$ \text {TP}_2$ is equivalent to IP. We see that these three TPs give a dichotomy theorem, just as with TP, $\text {TP}_1$, and $\text {TP}_2$. Along the way, we observe that appropriately generalized tree index structures $\mathcal {I}^{<\omega }$ are Ramsey, allowing for the use of generalized tree indiscernibles.

In this article, we prove that the precipitousness of $\mathbb {Q}_\gamma $, the countable stationary tower of height $\gamma $, where $\gamma $ is a limit ordinal $>\omega $, is a consequence of a certain stationary reflection principle for $\mathcal {P}_{\omega _1} H_{\left \vert {V_\gamma } \right \vert {}^+}$. Using this, we prove the consistency of the precipitousness of $\mathbb {Q}_\gamma $ for some singular $\gamma $ assuming a sufficiently strong large cardinal axiom. Furthermore, assuming the existence of proper class many supercompact cardinals, we build a model where $\mathbb {Q}_\gamma $ is precipitous for every limit ordinal $>\omega $.

We show that for any class of Boolean algebras with an associative operator, if it contains the complex algebra of $(\mathcal {P}(\mathbb {N}), \cup )$, its equational theory is undecidable. Equivalently, any associative normal modal logic valid over the frame $(\mathcal {P}(\mathbb {N}), \cup )$ is undecidable. This settles a long-open question on the decidability of hyperboolean modal logic [16], and addresses several related problems.

We introduce the notion of virtual ultracategory. From a topological point of view, this notion can be seen as a categorification of relational $\beta $-modules. From a categorical point of view, virtual ultracategories generalize ultracategories in the same way that multicategories generalize monoidal categories. From a logical point of view, whereas the points of a coherent topos form an ultracategory, the points of an arbitrary topos form a virtual ultracategory. We then extend Makkai–Lurie’s conceptual completeness: a topos with enough points can be reconstructed from its virtual ultracategory of points.

We prove that it is consistent with ZFC that for every non-decreasing function $f:[0,1]\rightarrow [0,1]$, each subset of $[0,1]$ of cardinality $\mathfrak c$ contains a set of cardinality $\mathfrak c$ on which f is uniformly continuous. We show that this statement follows from the assumptions that $\mathfrak d^* <\mathfrak c$ and $\mathfrak c$ is regular, where $\mathfrak d^*\leq \mathfrak d$ is the smallest cardinality $\kappa $ such that any two disjoint countable dense sets in $2^{\mathbb {N}}$ can be separated by sets each of which is an intersection of at most $\kappa $-many open sets in $2^{\mathbb {N}}$. We establish also that $\mathfrak d^*=\min \{\mathfrak u, \mathfrak d\}=\min \{\mathfrak r, \mathfrak d\}$, thus giving an alternative proof of the latter equality established by J. Aubrey in 2004.

We show that for a Suslin ccc forcing notion $\mathbb Q$ adding a Hechler real, “$\mathrm {ZF}+\mathrm {DC}_{\omega _1}+$all sets of reals are $I_{\mathbb Q,\aleph _0}$-measurable” implies the existence of an inner model with a measurable cardinal. We also introduce a wide class of Suslin ccc forcing notions which add a Hechler real, so that the above result applies to them.

We describe the fibrational structure of sets within the predicative variant $\textbf {pEff}$ of Hyland’s Effective Topos ${\mathbf {Eff} }$, previously introduced in Feferman’s classical predicative theory of non-iterative fixpoints ${\widehat {ID_1}}$. Our structural analysis can be carried out also in constructive and predicative variants of ${\mathbf {Eff} }$ developed within extensions of Aczel’s constructive Zermelo–Fraenkel set theory. This shows that the full subcategory of discrete objects of Hyland’s Effective Topos ${\mathbf {Eff} }$ already contains a fibred predicative topos validating the Formal Church Thesis, even when both are formalized in a constructive and predicative foundational theory.

It is a long-standing open problem whether modal logics of the form $\mathbf {K}\oplus \Box ^np\to \Box ^mp$ for $n>m>1$ have the finite model property (FMP). We solve this by showing that any modal logic axiomatized by formulas of the form $\Box ^np\to \Box ^mp$ where $n>m>1$ has the FMP.

Friedman and Stanley [9] developed the notion of Borel reducibility and illustrated its use in comparing classification problems for some familiar classes of countable structures. For many embeddings, the fact that the embedding is 1–1 on isomorphism types is explained by the existence of simple formulas that, uniformly, interpret the input structure in the output structure. For the embeddings of graphs in trees, and in linear orderings, there is no uniform interpretation [16, 20]. We focus on a version of the Friedman–Stanley embedding from [16] that takes each structure $\mathcal {A}$ for the language of graphs to a labeled tree $T_{\mathcal {A}}$. Gonzalez and Rossegger [13] showed that this embedding preserves Scott complexity. We refine this result, showing that for an X-computable ordinal, if one of $\mathcal {A}$, $T_{\mathcal {A}}$ has a computable infinitary Scott sentence, then so does the other, and the complexities match. Let $\mathbb {T}$ be the class of labeled trees isomorphic to those in the range of the embedding, and let $\mathbb {T}^\alpha $ be the subclass consisting of structures of Scott rank at most $\alpha $. It follows from results of Gao [10] that $\mathbb {T}$ is not Borel. We show that for each $\alpha $, $\mathbb {T}^\alpha $ is Borel. In fact, if $\alpha $ is an X-computable ordinal, then $\mathbb {T}^\alpha $ is complete X-effective $\Pi _{2\alpha +2}$.

We continue the development of the theory of capturing schemes over $\omega _1$ by analyzing the relation between the capturing construction schemes (whose existence is implied by Jensen’s $\Diamond $-principle) and both the Continuum Hypothesis and Ostaszewski’s -principle. Formally, we show that the property of being capturing can be viewed as the conjunction of two properties, one of which is implied by and the other one by CH. We apply these principles to construct multiple gaps, entangled sets, and metric spaces without uncountable monotone subspaces.

The Robinson Splitting Theorem states that a computably enumerable (c.e.) degree $\boldsymbol {b}$ splits over any low c.e. degree $\boldsymbol {c}<\boldsymbol {b}$. We prove that a weaker version of this theorem holds in models of ${\mathsf {P}}^{-}+\mathsf {I}{\Sigma }_1$, with lowness replaced by super-lowness.

Kuroda’s translation embeds first-order classical logic into first-order intuitionistic logic. It satisfies the soundness property—if a judgment is provable in classical logic, then its translation is provable in intuitionistic logic—as well as the characterization property—a formula and its translation are equivalent in classical logic—and the reverse translation property—if the translation of a judgment is provable in intuitionistic logic then the original judgment is provable in classical logic. Brown and Rizkallah extended Kuroda’s translation to higher-order logic. However, they showed that the soundness property fails in the presence of functional extensionality, and they neither proved the characterization property nor the reverse translation property.

In this article, we emphasize different conditions under which Kuroda’s translation works in the presence of functional extensionality, including the double-negation shift. We show that the characterization property and the reverse translation property do not necessarily hold in higher-order logic. Nevertheless, we prove that it is sufficient to assume both functional extensionality and propositional extensionality.

Let $\mathscr {S}$ be the class of all structures whose growth rate on orbits of subsets of size $n$ is not faster than $\frac {2^n}{p(n)}$ for any polynomial $p$. In this article we give a complete classification of all structures in $\mathscr {S}$ in terms of their automorphism groups. As a consequence of our classification we show that $\mathscr {S}$ has only countably many structures up to bidefinability, all these structures are first-order interpretable in $(\mathbb {Q};<)$ and they are interdefinable with a finitely bounded homogeneous structure. Furthermore, we also show that all structures in $\mathscr {S}$ have finitely many first-order reduct up to interdefinability, thereby confirming Thomas’ conjecture for the class $\mathscr {S}$.