We show that the polynomial translation of the classical propositional normal modal logic S4 into the intuitionistic propositional logic Int from Fernández is incorrect. We give a modified translation and prove its correctness, and provide implementations of both translations to allow others to test our results.

A sequence of graphs is FO-convergent if the probability of satisfaction of every first-order formula converges. A graph modeling is a graph, whose domain is a standard probability space, with the property that every definable set is Borel. It was known that FO-convergent sequence of graphs do not always admit a modeling limit, but it was conjectured that FO-convergent sequences of sufficiently sparse graphs have a modeling limits. Precisely, two conjectures were proposed:

1. 1. If a FO-convergent sequence of graphs is residual, that is if for every integer d the maximum relative size of a ball of radius d in the graphs of the sequence tends to zero, then the sequence has a modeling limit.

2. 2. A monotone class of graphs ${\cal C}$ has the property that every FO-convergent sequence of graphs from ${\cal C}$ has a modeling limit if and only if ${\cal C}$ is nowhere dense, that is if and only if for each integer p there is $N\left( p \right)$ such that no graph in ${\cal C}$ contains the pth subdivision of a complete graph on $N\left( p \right)$ vertices as a subgraph.

In this article we prove both conjectures. This solves some of the main problems in the area and among others provides an analytic characterization of the nowhere dense–somewhere dense dichotomy.

The classical Halpern–Läuchli theorem states that for any finite coloring of a finite product of finitely branching perfect trees of height ω, there exist strong subtrees sharing the same level set such that tuples in the product of the strong subtrees consisting of elements lying on the same level get the same color. Relative to large cardinals, we establish the consistency of a tail cone version of the Halpern–Läuchli theorem at a large cardinal (see Theorem 3.1), which, roughly speaking, deals with many colorings simultaneously and diagonally. Among other applications, we generalize a polarized partition relation on rational numbers due to Laver and Galvin to one on linear orders of larger saturation.

Let an oracle be called low for prefix-free complexity on a set in case access to the oracle improves the prefix-free complexities of the members of the set at most by an additive constant. Let an oracle be called weakly low for prefix-free complexity on a set in case the oracle is low for prefix-free complexity on an infinite subset of the given set. Furthermore, let an oracle be called low and weakly for prefix-free complexity along a sequence in case the oracle is low and weakly low, respectively, for prefix-free complexity on the set of initial segments of the sequence. Our two main results are the following characterizations. An oracle is low for prefix-free complexity if and only if it is low for prefix-free complexity along some sequences if and only if it is low for prefix-free complexity along all sequences. An oracle is weakly low for prefix-free complexity if and only if it is weakly low for prefix-free complexity along some sequence if and only if it is weakly low for prefix-free complexity along almost all sequences. As a tool for proving these results, we show that prefix-free complexity differs from its expected value with respect to an oracle chosen uniformly at random at most by an additive constant, and that similar results hold for related notions such as a priori probability. Furthermore, we demonstrate that on every infinite set almost all oracles are weakly low but are not low for prefix-free complexity, while by Shoenfield absoluteness there is an infinite set on which uncountably many oracles are low for prefix-free complexity. Finally, we obtain no-gap results, introduce weakly low reducibility, or WLK-reducibility for short, and show that all its degrees except the greatest one are countable.

We provide dichotomy results characterizing when two disjoint analytic binary relations can be separated by a countable union of ${\bf{\Sigma }}_1^0 \times {\bf{\Sigma }}_\xi ^0$ sets, or by a ${\bf{\Pi }}_1^0 \times {\bf{\Pi }}_\xi ^0$ set.

Our concern is the completeness problem for spi-logics, that is, sets of implications between strictly positive formulas built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, spi-logics have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi and first-order relational structures (aka Kripke frames) often used as the intended structures in applications. Here we lay foundations for a completeness theory that aims to answer the question whether the two semantics define the same consequence relations for a given spi-logic.

In this article I investigate the phenomenon of minimum and minimal models of second-order set theories, focusing on Kelley–Morse set theory KM, Gödel–Bernays set theory GB, and GB augmented with the principle of Elementary Transfinite Recursion. The main results are the following. (1) A countable model of ZFC has a minimum GBC-realization if and only if it admits a parametrically definable global well order. (2) Countable models of GBC admit minimal extensions with the same sets. (3) There is no minimum transitive model of KM. (4) There is a minimum β-model of GB+ETR. The main question left unanswered by this article is whether there is a minimum transitive model of GB+ETR.

We construct a model in which the tree property holds in ${\aleph _{\omega + 1}}$ and it is destructible under $Col\left( {\omega ,{\omega _1}} \right)$. On the other hand we discuss some cases in which the tree property is indestructible under small or closed forcings.

We consider the structure $({\Bbb Z}, + ,0,|_{p_1 } , \ldots ,|_{p_n } )$, where $x|_p y$ means $v_p \left( x \right) \leqslant v_p \left( y \right)$ and vp is the p-adic valuation. We prove that this structure has quantifier elimination in a natural expansion of the language of abelian groups, and that it has dp-rank n. In addition, we prove that a first order structure with universe ${\Bbb Z}$ which is an expansion of $({\Bbb Z}, + ,0)$ and a reduct of $({\Bbb Z}, + ,0,|_p )$ must be interdefinable with one of them. We also give an alternative proof for Conant’s analogous result about $({\Bbb Z}, + ,0, < )$.

Given a weakly o-minimal structure ${\cal M}$ and its o-minimal completion $\bar{{\cal M}}$, we first associate to $\bar{{\cal M}}$ a canonical language and then prove that Th$\left( {\cal M} \right)$ determines $Th\left( {\bar{{\cal M}}} \right)$. We then investigate the theory of the pair $\left( {\bar{{\cal M}},{\cal M}} \right)$ in the spirit of the theory of dense pairs of o-minimal structures, and prove, among other results, that it is near model complete, and every definable open subset of ${\bar{M}^n}$ is already definable in $\bar{{\cal M}}$.

We give an example of a weakly o-minimal structure interpreting $\bar{{\cal M}}$ and show that it is not elementarily equivalent to any reduct of an o-minimal trace.

We prove from the existence of a Mahlo cardinal the consistency of the statement that 2ω = ω3 holds and every stationary subset of ${\omega _2}\mathop \cap \nolimits {\rm{cof}}\left( \omega \right)$ reflects to an ordinal less than ω2 with cofinality ω1.

We prove that infinite definably simple locally finite groups of finite centraliser dimension are simple groups of Lie type over locally finite fields. Then, we identify conditions on automorphisms of a stable group that make it resemble the Frobenius maps, and allow us to classify definably simple stable groups in the specific case when they admit such automorphisms.

$ISP$ cannot hold at the first or second successor of a singular strong limit of countable cofinality; on the other hand, we force a failure of “strong ${\rm{SCH}}$” across a cardinal where $ITP$ holds. We also show that $ITP$ does not imply that there are stationary many internally unbounded models.

In this article, we study an analogue of tt-reducibility for points in computable metric spaces. We characterize the notion of the metric tt-degree in the context of first-level Borel isomorphism. Then, we study this concept from the perspectives of effective topological dimension theory and of effective fractal dimension theory.

We study the theory Tm,n of existentially closed incidence structures omitting the complete incidence structure Km,n, which can also be viewed as existentially closed Km,n-free bipartite graphs. In the case m = n = 2, this is the theory of existentially closed projective planes. We give an $\forall \exists$-axiomatization of Tm,n, show that Tm,n does not have a countable saturated model when m, n ≥ 2, and show that the existence of a prime model for T2,2 is equivalent to a longstanding open question about finite projective planes. Finally, we analyze model theoretic notions of complexity for Tm,n. We show that Tm,n is NSOP1, but not simple when m, n ≥ 2, and we show that Tm,n has weak elimination of imaginaries but not full elimination of imaginaries. These results rely on combinatorial characterizations of various notions of independence, including algebraic independence, Kim independence, and forking independence.

Given a compact Polish space E and the hyperspace of its compact subsets ${\cal K}\left( E \right)$, we consider Gδσ-ideals of compact subsets of E. Solecki has shown that any σ-ideal in a broad natural class of Gδ ideals can be represented via a compact subset of ${\cal K}\left( E \right)$; in this article we examine the behaviour of Gδ subsets of E with respect to the representing set. Given an ideal I in this class, we construct a representing set that recognises a compact subset of E as being “small” precisely when it is in I, and recognises a Gδ subset of E as being “small” precisely when it is covered by countably many compact sets from I.

This paper consists in the formulation of a novel categorical set theory, MLCat, which is proved to be equiconsistent to New Foundations (NF), and which can be modulated to correspond to intuitionistic (denoted with an “I” on the left) or classical NF, with atoms (denoted with a “U” on the right) or not:

We introduce a notion of the space of types in positive model theory based on Stone duality for distributive lattices. We show that this space closely mirrors the Stone space of types in the full first-order model theory with negation (Tarskian model theory). We use this to generalise some classical results on countable models from the Tarskian setting to positive model theory.

A formula φ is called n-provable in a formal arithmetical theory S if φ is provable in S together with all true arithmetical ${{\rm{\Pi }}_n}$-sentences taken as additional axioms. While in general the set of all n-provable formulas, for a fixed $n > 0$, is not recursively enumerable, the set of formulas φ whose n-provability is provable in a given r.e. metatheory T is r.e. This set is deductively closed and will be, in general, an extension of S. We prove that these theories can be naturally axiomatized in terms of progressions of iterated local reflection principles. In particular, the set of provably 1-provable sentences of Peano arithmetic $PA$ can be axiomatized by ${\varepsilon _0}$ times iterated local reflection schema over $PA$. Our characterizations yield additional information on the proof-theoretic strength of these theories (w.r.t. various measures of it) and on their axiomatizability. We also study the question of speed-up of proofs and show that in some cases a proof of n-provability of a sentence can be much shorter than its proof from iterated reflection principles.

Using a technique developed by Coquand and Hofmann [3] we verify that adding the analytical form MP1: $\forall \alpha (\neg \neg \exists {\rm{x}}\alpha ({\rm{x}}) = 0 \to \exists {\rm{x}}\alpha ({\rm{x}}) = 0)$ of Markov’s Principle does not increase the class of ${\rm{\Pi }}_2^0$ formulas provable in Kleene and Vesley’s formal system for intuitionistic analysis, or in subsystems obtained by omitting or restricting various axiom schemas in specified ways.