arXiv · 2508.01788
This is a survey of the model theory of second order logic.
Explore connections, maps & timelines
Jouko Väänänen. 2025-08-03. Model theory of second order logic. https://arxiv.org/abs/2508.01788
Cite the original work for its findings. Save a collection to share your selection of sources.
KEEP EXPLORING
We study discontinuity of multivalued functions (also known as problems) $P$ on Baire space by assigning an ordinal rank to points in the domain of $P$ that have no local realizers. For each countable ordinal $α$, let $\mathsf{ACC}_{\mathbb N}^α$ be the problem of solving $\mathsf{ACC}_{\mathbb N}$ in at most $α$ many attempts, with a new instance provided for each attempt. Our main theorem shows that, for any problem $P$, the following are equivalent: (i) $P$ is discontinuous on some set all of whose points have Cantor--Bendixson rank at most $α$, and (ii) $\mathsf{ACC}_{\mathbb N}^α\leq_{\mathrm W}^{*}P$. This extends to points: $P \geq_{\mathrm{W}}^* \mathsf{ACC}_{\mathbb{N}}^α$ via a forward function that sends $\#^{\mathbb{N}}$ to $p \in \operatorname{dom}(P)$ if and only if $P$ is discontinuous on a set $A$ with $\operatorname{rank}_A(p) \leq α$ and $P$ has no continuous realizer for any neighborhood of $p$. We also characterize these properties via a Wadge-style discontinuity game for $P$. We apply this framework to the thin set and achromatic Ramsey theorems. Extending $\mathsf{RT}^{n}_{k,j}$ to ordinal parameters, we define $\mathsf{RT}^{n}_{α,β}$ and compute their ranks of discontinuity. The problems $\mathsf{RT}^n_{α,β}$ provide examples of problems with discontinuities of each countable rank which are not reducible to $\mathsf{ACC}_{\mathbb{N}}$. The separation from $\mathsf{ACC}_{\mathbb{N}}$ is obtained via the notion of guessability with identified errors.
Perhaps surprisingly, there are infinite types that can be exhaustively searched mechanically in finite time. We use ideas from topology to build plenty of them, referring to searchable types as compact types, and we use ordinals to measure their logical complexity. We consider two systems of ordinal notations under which a single notation denotes both a discrete ordinal and a compact one, with an embedding of the former into the latter whose image has empty complement. A boolean valued function decides which points in the image of the embedding are isolated and which are topological limit points. The first system consists of the traditional Brouwer codes and the second is an inductive-recursive universe generalizing them. The discrete ordinals so obtained are trichotomous, and the compact ones have the least element property for complemented subsets, but these two desirable properties cannot be fulfilled simultaneously in a constructive setting. The ordinals obtained from Brouwer codes further enjoy a boolean Leibniz principle, which has the notion of total separatedness as its topological counterpart. This extends previous work from Gödel's system T to intensional Martin-Löf type theory with univalent universes, and is formalized in Agda in the TypeTopology repository.
An algebra with binary operations $+,\cdot,\uparrow$ and constant $1$ is called an HSI algebra if it satisfies the basic commutative semiring laws for $+,\cdot,1$ on~$\mathbb{N}$ as well as the familiar index laws for exponentiation $\uparrow$. These basic axioms, known as the ``High School Identities'' are known to be incomplete, and an algebra satisfying $\HSI$ but failing an equation valid on ${\bf N}:=\langle \mathbb{N};+,\cdot,\uparrow,1\rangle$ is called a \emph{Gurevič algebra}. It is currently unknown if there is an algorithm to recognise finite Gurevič algebras, and the best current result is that there exists a 12-element Gurevič algebra, and that none of the five 2-element HSI algebras are Gurevič algebras. We explain how the work of Alex Wilkie can be used to provide an algorithm for deciding validity of the equational laws of $\langle \mathbb{N};+,\cdot,\uparrow,1\rangle$, and use this to show that multiplicatively-idempotent HSI algebras satisfy all valid laws of $\langle \mathbb{N};+,\cdot,\uparrow,1\rangle$. As consequences of this result, we show that all 44 HSI algebras on 3 elements lie in the variety of $\langle \mathbb{N};+,\cdot,\uparrow,1\rangle$ (that is, are not Gurevič algebras), as well as 597 of the 657 models on 4 elements and 11158 of the 13577 models on 5 elements. A further consequence is that every Brouwerian lattice lies in the variety of $\langle \mathbb{N};+,\cdot,\uparrow,1\rangle$ (up to a simple term equivalence), showing that the variety of $\langle \mathbb{N};+,\cdot,\uparrow,1\rangle$ has continuum many subvarieties. The constant-free signature is also explored, and it is shown that in this case all $2$-element models of the constant-free High School Laws satisfy all valid constant-free laws in $\langle \mathbb{N};+,\cdot,\uparrow\rangle$.