A duality theoretic view on limits of finite structures

TL;DR

This paper explores the connection between structural limits of finite models and model theory by extending the Stone pairing with probabilistic operators, revealing a duality-based framework that links logic, semantics, and complexity.

Contribution

It introduces a finer measure space via Stone-Priestley duality, enriched with probabilistic operators, and provides a complete calculus for this extended logic, bridging semantics and algorithmic logic.

Findings

Identifies the logical core of the theory of structural limits.

Shows that the duality-based Stone pairing captures quantifier addition.

Links model theoretic types to semiring quantifiers in logic.

Abstract

A systematic theory of structural limits for finite models has been developed by Nesetril and Ossona de Mendez. It is based on the insight that the collection of finite structures can be embedded, via a map they call the Stone pairing, in a space of measures, where the desired limits can be computed. We show that a closely related but finer grained space of measures arises --- via Stone-Priestley duality and the notion of types from model theory --- by enriching the expressive power of first-order logic with certain ``probabilistic operators''. We provide a sound and complete calculus for this extended logic and expose the functorial nature of this construction. The consequences are two-fold. On the one hand, we identify the logical gist of the theory of structural limits. On the other hand, our construction shows that the duality-theoretic variant of the Stone pairing captures the adding of a layer of quantifiers, thus making a strong link to recent work on semiring quantifiers in logic on words. In the process, we identify the model theoretic notion of types as the unifying concept behind this link. These results contribute to bridging the strands of logic in computer science which focus on semantics and on more algorithmic and complexity related areas, respectively.

Equations

$$⟨\phi ,A⟩=\frac{|\{\overline{a}\in A^n\mid A\models \phi (\overline{a})\}|}{|A{|}^n}\text{parbox}130.0002pt\text{centering}\text{(the probability that a random assignment in A satisfies φ)}.\text{@add@centering}$$

$$[[\text{-}]]:D\to \wp (X_D),a\mapsto [[a]]=\{F\in X_D\mid a\in F\}$$

$$\xi :A^{\ast }\stackrel{\text{mathmakebox}[3em]R}{\to }\hat{\mathbf{S}}(\beta ((A\times 2{)}^{\ast }))\stackrel{\text{mathmakebox}[3em]\hat{\mathbf{S}}(f)}{\to }\hat{\mathbf{S}}(X),$$

$$\{r^{-}\mid r\in (0,1]\}\cup \{q^{\circ }\mid q\in \mathbb{Q}\cap [0,1]\}.$$

$$\uparrow p^{\circ }=\{x\in \mathbf{\Gamma }\mid p^{\circ }\le x\}\text{and}\downarrow q^{-}=\{x\in \mathbf{\Gamma }\mid x\le q^{-}\}$$

$$\mathbf{L}=\{\perp \}\cup (\mathbb{Q}\cap [0,1]{)}^{\partial },\text{ with }\perp {<}_{\mathbf{L}}q\text{ and }q{\le }_{\mathbf{L}}p\text{ for every }p\le q\text{ in }\mathbb{Q}\cap [0,1].$$

$$\begin{aligned} r^{\circ}-s^{\circ}&\enspace=\enspace(r-s)^{\circ}\\ r^{-}-s^{\circ}&\enspace=\enspace(r-s)^{-}\end{aligned}\qquad\qquad\begin{rcases*}r^{\circ}-s^{-}\\ r^{-}-s^{-}\end{rcases*}\enspace=\enspace\begin{cases}(r-s)^{\circ}&\text{ if }r-s\in\mathbb{Q}\\ (r-s)^{-}&\text{ otherwise}.\end{cases}$$

$$\sim :\mathrm{dom}(-)\to \mathbf{\Gamma },x\sim y=\bigvee \{x-q^{\circ }\mid y<q^{\circ }\le x\}.$$

$$\gamma :\mathbf{\Gamma }\to [0,1],r^{-},r^{\circ }\mapsto r.$$

$$\iota :[0,1]\to \mathbf{\Gamma },r\mapsto \{\begin{array}{ll}{r}^{\circ }& \text{if }r\in \mathbb{Q}\\ r^{-}& \text{otherwise}.\end{array}$$

$$\bigcup \{\uparrow p^{\circ }\mid p\in \mathbb{Q}\cap [0,1]\text{ and }q<p\}\text{and}\bigcup \{\downarrow p^{-}\mid p\in \mathbb{Q}\cap (0,1]\text{ and }p<q\}.$$

$$\forall a,b\in D,m(a)-m(a\wedge b)=m(a\vee b)-m(b).$$

$$\mu (a)\sim \mu (a\wedge b)\le \mu (a\vee b)-\mu (b)\text{ and }\mu (a)-\mu (a\wedge b)\ge \mu (a\vee b)\sim \mu (b).$$

$$C_{1,2}=\{f\in {\mathbf{\Gamma }}^D\mid f(0)=0^{\circ }\}\cap \{f\in {\mathbf{\Gamma }}^D\mid f(1)=1^{\circ }\}\cap \bigcap _{a\le b}\{f\in {\mathbf{\Gamma }}^D\mid f(a)\le f(b)\}.$$

$${\mathcal{M}}_{\mathrm{\Gamma }}(D)=\bigcap _{a,b\in D}$$

$$\cap \bigcap _{a,b\in D}$$

$${\mathcal{M}}_{\mathrm{\Gamma }}(h{)}^{-1}([[a<q]])=\{\mu :E\to \mathbf{\Gamma }\mid \mu (h(a))<q^{\circ }\}=[[h(a)<q]]$$

$${\gamma }^{\#}:{\mathcal{M}}_{\mathrm{\Gamma }}(D)\to {\mathcal{M}}_{\mathrm{I}}(D),\mu \mapsto \gamma \cdot \mu \text{ and }{\iota }^{\#}:{\mathcal{M}}_{\mathrm{I}}(D)\to {\mathcal{M}}_{\mathrm{\Gamma }}(D),m\mapsto \iota \cdot m.$$

$$({\gamma }^{\#}{)}^{-1}\{m\in {\mathcal{M}}_{\mathrm{I}}(D)\mid m(a)\in O\}=\{\mu \in {\mathcal{M}}_{\mathrm{\Gamma }}(D)\mid \mu (a)\in {\gamma }^{-1}(O)\}$$

$$({\iota }^{\#}{)}^{-1}\{\mu \in {\mathcal{M}}_{\mathrm{\Gamma }}(D)\mid \mu (a)\le q^{-}\}$$

$$=\{m\in {\mathcal{M}}_{\mathrm{I}}(D)\mid m(a)<q\},$$

$$+:\mathrm{dom}(+)\to \mathbf{\Gamma },\text{where}\mathrm{dom}(+)=\{(x,y)\mid x\le 1^{\circ }-y\},$$

$$r^{\circ }+s^{\circ }=(r+s{)}^{\circ },r^{-}+s^{\circ }=(r+s{)}^{-},r^{\circ }+s^{-}=(r+s{)}^{-},\text{and }{r}^{-}+s^{-}=(r+s{)}^{-}.$$

$$\int f:M\mapsto {\int }_{M}f=\sum \{f(x)\mid x\in M\cap \mathrm{supp}(f)\}.$$

$$f_n^A(E)=\sum _{(A,\alpha )\in E}{\left(\frac{1}{|A{|}^n}\right)}^{\circ }\text{parbox}205.0003pt\text{centering}\text{(Add ∣A∣n1 for every interpretation α of the free variables s.t. (A,α) is in the equivalence class)}.\text{@add@centering}$$

$${\mu }_n^A:{\mathrm{FO}}_n(\sigma )\to \mathbf{\Gamma },\phi \mapsto {\int }_{[[\phi {]]}_n}{f}_n^A.$$

$$\mathrm{Fin}(\sigma )\to {\mathcal{M}}_{\mathrm{\Gamma }}(\wp ({\mathrm{Typ}}_n(\sigma )))\to {\mathcal{M}}_{\mathrm{\Gamma }}({\mathrm{FO}}_n(\sigma )),A\mapsto \int f_n^A\mapsto {\mu }_n^A.$$

$${\mu }_n^A(\phi )=\sum _{(A,\alpha )\in [[\phi {]]}_n}{\left(\frac{1}{|A{|}^n}\right)}^{\circ }={\left(\frac{|\{\overline{a}\in A^n\mid A\models \phi (\overline{a})|}{|A{|}^n}\right)}^{\circ }=({⟨\phi ,A⟩}_{\mathrm{I}}{)}^{\circ }.$$

$$\left\{\leavevmode\hbox to215.6pt{\vbox to13.1pt{\pgfpicture\makeatletter\hbox{\hskip 107.8023pt\lower-8.09982pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{}{}{}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{\offinterlineskip{}{}{{{}}{{}}}{{{}}}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-110.8023pt}{-7.99998pt}\pgfsys@invoke{ }\hbox{\vbox{\halign{\pgf@matrix@init@row\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding&&\pgf@matrix@step@column{\pgf@matrix@startcell#\pgf@matrix@endcell}&#\pgf@matrix@padding\cr\hfil\hskip 28.66277pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.66277pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}_{n}(\sigma))}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{}}}&\hskip 28.66277pt\hfil&\hfil\hskip 94.63959pt\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-66.63954pt}{0.0pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{${{\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}_{m}(\sigma))\mid m,n\in\mathbb{N},\ m\geq n}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}&\hskip 69.63954pt\hfil\cr}}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}{{{{}}}{{}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {}{ {}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{ {}{}}{}{}{{}{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@setlinewidth{0.39998pt}\pgfsys@invoke{ }{}{}{}{}{}{{}}{}{}{{}}\pgfsys@moveto{-28.67673pt}{-5.49998pt}\pgfsys@lineto{-52.87682pt}{-5.49998pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}}}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-51.63689pt}{-5.49998pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-53.0768pt}{-5.49998pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-46.1768pt}{-1.50833pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{$\scriptstyle{q_{n,m}}$} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}\right\}$$

$${⟨\text{-},A⟩}_{\mathrm{\Gamma }}:\mathrm{FO}(\sigma )\to \mathbf{\Gamma }$$

$$({⟨\neg \psi ,A_n⟩}_{\mathrm{\Gamma }}{)}_n=(1^{\circ },(\frac{1}{3}{)}^{\circ },1^{\circ },(\frac{2}{4}{)}^{\circ },1^{\circ },(\frac{3}{5}{)}^{\circ },\dots ).$$

Full text

The consequences are two-fold. On the one hand, we identify the logical gist of the theory of structural limits. On the other hand, our construction shows that the duality-theoretic variant of the Stone pairing captures the adding of a layer of quantifiers, thus making a strong link to recent work on semiring quantifiers in logic on words. In the process, we identify the model theoretic notion of types as the unifying concept behind this link. These results contribute to bridging the strands of logic in computer science which focus on semantics and on more algorithmic and complexity related areas, respectively.

1 Introduction

While topology plays an important role, via Stone duality, in many parts of semantics, topological methods in more algorithmic and complexity oriented areas of theoretical computer science are not so common. One of the few examples, the one we want to consider here, is the study of limits of finite relational structures. We will focus on the structural limits introduced by Nešetřil and Ossona de Mendez [17, 16]. These provide a common generalisation of various notions of limits of finite structures studied in probability theory, random graphs, structural graph theory, and finite model theory. The basic construction in this work is the so-called Stone pairing. Given a relational signature $\sigma$ and a first-order formula $\varphi$ in the signature $\sigma$ with free variables $v_{1},\dots,v_{n}$, define

[TABLE]

Nešetřil and Ossona de Mendez view the map $A\mapsto\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>$ as an embedding of the finite $\sigma$-structures into the space of probability measures over the Stone space dual to the Lindenbaum-Tarski algebra of all first-order formulas in the signature $\sigma$. This space is complete and thus provides the desired limit objects for all sequences of finite structures which embed as Cauchy sequences.

Another example of topological methods in an algorithmically oriented area of computer science is the use of profinite monoids in automata theory. In this setting, profinite monoids are the subject of the extensive theory, based on theorems by Eilenberg and Reiterman, and used, among others, to settle decidability questions [18]. In [4], it was shown that this theory may be understood as an application of Stone duality, thus making a bridge between semantics and more algorithmically oriented work. Bridging this semantics-versus-algorithmics gap in theoretical computer science has since gained quite some momentum, notably with the recent strand of research by Abramsky, Dawar and co-workers [2, 3]. In this spirit, a natural question is whether the structural limits of Nešetřil and Ossona de Mendez also can be understood semantically, and in particular whether the topological component may be seen as an application of Stone duality.

More precisely, recent work on understanding quantifiers in the setting of languages over finite words [5] has shown that adding a layer of certain quantifiers (such as classical and modular quantifiers) corresponds dually to measure space constructions. The measures involved are not classical but only finitely additive and they take values in finite semirings rather than in the unit interval. Nevertheless, this appearance of measures as duals of quantifiers begs the further question whether the measure spaces in the theory of structural limits may be obtained via Stone duality from a semantic addition of certain quantifiers to classical first-order logic.

The purpose of this paper is to address this question. Our main result is that the Stone pairing of Nešetřil and Ossona de Mendez is related by a retraction to a Stone space of measures, which is dual to the Lindenbaum-Tarski algebra of a logic fragment obtained from first-order logic by adding one layer of a probabilistic quantifier, and which arises in exactly the same way as the spaces of semiring-valued measures in logic on words. That is, the Stone pairing, although originating from other considerations, may be seen as arising by duality from a semantic construction.

A foreseeable hurdle is that spaces of classical measures are valued in the unit interval $[0,1]{}$ which is not zero-dimensional and hence outside the scope of Stone duality. This is well-known to cause problems e.g. in attempts to combine non-determinism and probability in domain theory [12]. However, in the structural limits of Nešetřil and Ossona de Mendez, at the base, one only needs to talk about finite models equipped with normal distributions and thus only the finite intervals $I_{n}=\{0,\frac{1}{n},\frac{2}{n},\dots,1\}$ are involved. A careful duality-theoretic analysis identifies a codirected diagram (i.e. an inverse limit system) based on these intervals compatible with the Stone pairing. The resulting inverse limit, which we denote ${\mathbf{\Gamma}}$, is a Priestley space. It comes equipped with an algebra-like structure, which allows us to reformulate many aspects of the theory of structural limits in terms of ${\mathbf{\Gamma}}$-valued measures as opposed to $[0,1]$-valued measures.

The analysis justifying the structure of ${\mathbf{\Gamma}}$ is based on duality theory for double quasi-operator algebras [7, 8]. In the presentation, we have tried to compromise between giving interesting topo-relational insights into why ${\mathbf{\Gamma}}$ is as it is, and not overburdening the reader with technical details. Some interesting features of ${\mathbf{\Gamma}}$, dictated by the nature of the Stone pairing and the ensuing codirected diagram, are that

• •

${\mathbf{\Gamma}}$ is based on a version of $[0,1]$ in which the rationals are doubled;

• •

${\mathbf{\Gamma}}$ comes with section-retraction maps {[0,1]}$${{\mathbf{\Gamma}}}$${[0,1]}$$\scriptstyle{\iota}$$\scriptstyle{\gamma} ;

• •

the map $\iota$ is lower semicontinuous while the map $\gamma$ is continuous.

These features are a consequence of general theory and precisely allow us to witness continuous phenomena relative to $[0,1]$ in the setting of ${\mathbf{\Gamma}}$.

Our contribution

We show that the ambient measure space for the structural limits of Nešetřil and Ossona de Mendez can be obtained via “adding a layer of quantifiers” in a suitable enrichment of first-order logic. The conceptual framework for seeing this is that of types from classical model theory. More precisely, we will see that a variant of the Stone pairing is a map into a space of measures with values in a Priestley space ${\mathbf{\Gamma}}$. Further, we show that this map is in fact the embedding of the finite structures into the space of ([math]-)types of an extension of first-order logic, which we axiomatise. On the other hand, ${\mathbf{\Gamma}}$-valued measures and $[0,1]$-valued measures are tightly related by a retraction-section pair which allows the transfer of properties. These results identify the logical gist of the theory of structural limits and provide a new interesting connection between logic on words and the theory of structural limits in finite model theory.

Outline of the paper.

In section 2 we briefly recall Stone-Priestley duality, its application in logic via spaces of types, and the particular instance of logic on words (needed only to show the similarity of the constructions). In Section 3 we introduce the Priestley space ${\mathbf{\Gamma}}$ with its additional operations, and show that it admits $[0,1]$ as a retract. The spaces of ${\mathbf{\Gamma}}$-valued measures are introduced in Section 4, and the retraction of ${\mathbf{\Gamma}}$ onto $[0,1]$ is lifted to the appropriate spaces of measures. In Section 5 we introduce the ${\mathbf{\Gamma}}$-valued Stone pairing and make the link with logic on words. Further, we compare convergence in the space of ${\mathbf{\Gamma}}$-valued measures with the one considered by Nešetřil and Ossona de Mendez. Finally, in Section 6 we show that constructing the space of ${\mathbf{\Gamma}}$-valued measures dually corresponds to enriching the logic with probabilistic operators.

2 Preliminaries

Notation.

Throughout this paper, if $X\xrightarrow{f}Y\xrightarrow{g}Z$ are functions, their composition is denoted $g\cdot f$. For a subset $S\subseteq X$, $f_{\mathord{\upharpoonright}S}\colon S\to Y$ is the obvious restriction. Given any set $T$, \raisebox{2.03998pt}{\Large\wp}(T) denotes its power-set. Further, for a poset $P$, $P^{\partial}$ is the poset obtained by turning the order of $P$ upside down.

2.1 Stone-Priestley duality

In this paper, we will need Stone duality for bounded distributive lattices in the order topological form due to Priestley [19]. It is a powerful and well established tool in the study of propositional logic and semantics of programming languages, see e.g. [9, 1] for major landmarks. We briefly recall how this duality works.

A compact ordered space is a pair $(X,\leq)$ where $X$ is a compact space and $\leq$ is a partial order on $X$ which is closed in the product topology of $X\times X$. (Note that such a space is automatically Hausdorff). A compact ordered space is a Priestley space provided it is totally order-disconnected. That is, for all $x,y\in X$ such that $x\not\leq y$, there is a clopen (i.e. simultaneously closed and open) $C\subseteq X$ which is an up-set for $\leq$, and satisfies $x\in C$ but $y\notin C$. We recall the construction of the Priestley space of a distributive lattice $D$.111We assume all distributive lattices are bounded, with the bottom and top denoted by [math] and $1$, respectively. The bounds need to be preserved by homomorphisms.

A non-empty proper subset $F\subset D$ is a prime filter if it is (i) upward closed (in the natural order of $D$), (ii) closed under finite meets, and (iii) if $a\vee b\in F$, either $a\in F$ or $b\in F$. Denote by $X_{D}$ the set of all prime filters of $D$. By Stone’s Prime Filter Theorem, the map

[TABLE]

is an embedding. Priestley’s insight was that $D$ can be recovered from $X_{D}$, if the latter is equipped with the inclusion order and the topology generated by the sets of the form $\llbracket a\rrbracket$ and their complements. This makes $X_{D}$ into a Priestley space — the dual space of $D$ — and the map $\llbracket\mkern 1.5mu\text{-}\mkern 1.5mu\rrbracket$ is an isomorphism between $D$ and the lattice of clopen up-sets of $X_{D}$. Conversely, any Priestley space $X$ is the dual space of the lattice of its clopen up-sets. We call the latter the dual lattice of $X$. This correspondence extends to morphisms. In fact, Priestley duality states that the category of distributive lattices with homomorphisms is dually equivalent to the category of Priestley spaces and continuous monotone maps. When restricting to Boolean algebras, we recover the celebrated Stone duality restricted to Boolean algebras and Boolean spaces, i.e. compact Hausdorff spaces in which the clopen subsets form a basis.

2.2 Stone duality and logic: type spaces

The theory of types is an important tool for first-order logic. We briefly recall the concept as it is closely related to, and provides the link between, two otherwise unrelated occurrences of topological methods in theoretical computer science.

Consider a signature $\sigma$ and a first-order theory $T$ in this signature. For each $n\in\mathbb{N}$, let $\mathrm{Fm}_{n}$ denote the set of first-order formulas whose free variables are among $\overline{v}=\{v_{1},\dots,v_{n}\}$, and let $\mathrm{Mod}_{n}(T)$ denote the class of all pairs $(A,\alpha)$ where $A$ is a model of $T$ and $\alpha$ is an interpretation of $\overline{v}$ in $A$. Then the satisfaction relation, $(A,\alpha)\models\varphi$, is a binary relation from $\mathrm{Mod}_{n}$ to $\mathrm{Fm}_{n}$. It induces the equivalence relations of elementary equivalence $\equiv$ and logical equivalence $\approx$ on these sets, respectively. The quotient $\mathrm{FO}_{n}(T)=\mathrm{Fm}_{n}/{\approx}$ carries a natural Boolean algebra structure and is known as the $n$-th Lindenbaum-Tarski algebra of $T$. Its dual space is $\operatorname{Typ}_{n}(T)$, the space of $n$-types of $T$, whose points can be identified with elements of $\mathrm{Mod}_{n}(T)/{\equiv}$. The Boolean algebra $\mathrm{FO}(T)$ of all first-order formulas modulo logical equivalence over $T$ is the directed colimit of the $\mathrm{FO}_{n}(T)$ for $n\in\mathbb{N}$ while its dual space, $\operatorname{Typ}(T)$, is the codirected limit of the $\operatorname{Typ}_{n}(T)$ for $n\in\mathbb{N}$ and consists of models equipped with interpretations of the full set of variables.

If we want to study finite models, there are two equivalent approaches: e.g. at the level of sentences, we can either consider the theory $T_{\text{\em fin}}$ of finite $T$-models, or the closure of the collection of all finite $T$-models in the space $\operatorname{Typ}_{0}(T)$. This closure yields a space, which should tell us about finite $T$-structures. Indeed, it is equal to $\operatorname{Typ}_{0}(T_{\text{\em fin}})$, the space of pseudofinite $T$-structures. For an application of this, see [10]. Below, we will see an application in finite model theory of the case $T=\emptyset$ (in this case we write $\mathrm{FO}(\sigma)$ and $\operatorname{Typ}(\sigma)$ instead of $\mathrm{FO}(\emptyset)$ and $\operatorname{Typ}(\emptyset)$ to at least flag the signature).

In light of the theory of types as exposed above, the Stone pairing of Nešetřil and Ossona de Mendez (see equation (1)) can be regarded as an embedding of finite structures into the space of probability measures on $\operatorname{Typ}(\sigma)$, which set-theoretically are finitely additive functions $\mathrm{FO}(\sigma)\to[0,1]$.

2.3 Duality and logic on words

As mentioned in the introduction, spaces of measures arise via duality in logic on words [5]. Logic on words, as introduced by Büchi, see e.g. [14] for a recent survey, is a variation and specialisation of finite model theory where only models based on words are considered. I.e., a word $w\in A^{*}$ is seen as a relational structure on $\{1,\ldots,|w|\}$, where $|w|$ is the length of $w$, equipped with a unary relation $P_{a}$, for each $a\in A$, singling out the positions in the word where the letter $a$ appears. Each sentence $\varphi$ in a language interpretable over these structures yields a language $L_{\varphi}\subseteq A^{*}$ consisting of the words satisfying $\varphi$. Thus, logic fragments are considered modulo the theory of finite words and the Lindenbaum-Tarski algebras are subalgebras of \raisebox{2.03998pt}{\Large\wp}(A^{*}) consisting of the appropriate $L_{\varphi}$’s, cf. [10] for a treatment of first-order logic on words.

For lack of logical completeness, the duals of the Lindenbaum-Tarski algebras have more points than those given by models. Nevertheless, the dual spaces of types, which act as compactifications and completions of the collections of models, provide a powerful tool for studying logic fragments by topological means. The central notion is that of recognition, in which, a Boolean subalgebra \operatorname{\mathcal{B}}\subseteq\raisebox{2.03998pt}{\Large\wp}(A^{*}) is studied by means of the dual map $\eta\colon\beta(A^{*})\to X_{\operatorname{\mathcal{B}}}$. Here $\beta(A^{*})$ is the Stone dual of \raisebox{2.03998pt}{\Large\wp}(A^{*}), also known in topology as the Čech-Stone compactification of the discrete space $A^{*}$, and $X_{\operatorname{\mathcal{B}}}$ is the Stone dual of $\operatorname{\mathcal{B}}$. The set $A^{*}$ embeds in $\beta(A^{*})$, and $\eta$ is uniquely determined by its restriction $\eta_{0}\colon A^{*}\to X_{\operatorname{\mathcal{B}}}$. Now, Stone duality implies that $L\subseteq A^{*}$ is in $\operatorname{\mathcal{B}}$ iff there is a clopen subset $V\subseteq X_{\operatorname{\mathcal{B}}}$ so that $\eta_{0}^{-1}(V)=L$. Anytime the latter is true for a map $\eta$ and a language $L$ as above, one says that $\eta$ recognises $L$.222Here, being beyond the scope of this paper, we are ignoring the important role of the monoid structure available on the spaces (in the form of profinite monoids or BiMs, cf. [10, 5]).

When studying logic fragments via recognition, the following inductive step is central: given a notion of quantifier and a recogniser for a Boolean algebra of formulas with a free variable, construct a recogniser for the Boolean algebra generated by the formulas obtained by applying the quantifier. This problem was solved in [5], using duality theory, in a general setting of semiring quantifiers. The latter are defined as follows: let $(S,+,\cdot,0_{S},1_{S})$ be a semiring, and $k\in S$. Given a formula $\psi(v)$, the formula $\exists_{S,k}v.\psi(v)$ is true of a word $w\in A^{*}$ iff $k=1_{S}+\cdots+1_{S}$, $m$ times, where $m$ is the number of assignments of the variable $v$ in $w$ satisfying $\psi(v)$. If $S=\mathbb{Z}/q\mathbb{Z}$, we obtain the so-called modular quantifiers, and for $S$ the two-element lattice we recover the existential quantifier $\exists$.

To deal with formulas with a free variable, one considers maps of the form $f\colon\beta((A\times 2)^{*})\to X$ (the extra bit in $A\times 2$ is used to mark the interpretation of the free variable). In [5] (see also [6]), it was shown that $L_{\psi(v)}$ is recognised by $f$ iff for every $k\in S$ the language $L_{\exists_{S,k}v.\psi(v)}$ is recognised by the composite

[TABLE]

where $\widehat{\mathbf{S}}(X)$ is the space of finitely additive $S$-valued measures on $X$ and $R$ maps $w\in A^{*}$ to the measure \mu_{w}\colon\raisebox{2.03998pt}{\Large\wp}((A\times 2)^{*})\to S sending a set $K\subseteq(A\times 2)^{*}$ to the sum $1_{S}+\cdots+1_{S}$, $n_{w,K}$ times. Here, $n_{w,K}$ is the number of interpretations $\alpha$ of the free variable $v$ in $w$ such that the pair $(w,\alpha)$, seen as an element of $(A\times 2)^{*}$, belongs to $K$. Finally, $\widehat{\mathbf{S}}(f)$ sends a measure to its pushforward along $f$.

3 The space ${\mathbf{\Gamma}}$

Central to our results is a Priestley space ${\mathbf{\Gamma}}$ closely related to $[0,1]$, in which our measures will take values. Its construction comes from the insight that the range of the Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>$, for a finite structure $A$ and formulas restricted to a fixed number of free variables, can be confined to a chain $I_{n}=\{0,\frac{1}{n},\frac{2}{n},\dots,1\}$. Moreover, the floor functions $f_{mn,n}\colon I_{mn}\twoheadrightarrow I_{n}$ are monotone surjections. The ensuing system $\{f_{mn,n}\colon I_{mn}\twoheadrightarrow I_{n}\mid m,n\in\mathbb{N}\}$ can thus be seen as a codirected diagram of finite discrete posets and monotone maps. Let us define ${\mathbf{\Gamma}}$ to be the limit of this diagram. Then, ${\mathbf{\Gamma}}$ is naturally equipped with a structure of Priestley space, see e.g. [11, Corollary VI.3.3], and can be represented as based on the set

[TABLE]

The order of ${\mathbf{\Gamma}}$ is the unique total order which has $0^{\circ}$ as bottom element, satisfies $r^{*}<s^{*}$ if and only if $r<s$ for ${\scriptstyle\ast}\in\{{\scriptstyle-},{\scriptstyle\circ}\}$, and such that $q^{\circ}$ is a cover of $q^{-}$ for every rational $q\in(0,1]$ (i.e. $q^{-}<q^{\circ}$, and there is no element strictly in between). In a sense, the values $q^{-}$ represent approximations of the values of the form $q^{\circ}$. Cf. Figure 1. The topology of ${\mathbf{\Gamma}}$ is generated by the sets of the form

[TABLE]

for $p,q\in\mathbb{Q}\cap[0,1]$ such that $q\neq 0$. The distributive lattice dual to ${\mathbf{\Gamma}}$, denoted by $\mathbf{L}$, is given by

[TABLE]

3.1 The algebraic structure on ${\mathbf{\Gamma}}$

When defining measures we need an algebraic structure available on the space of values. The space ${\mathbf{\Gamma}}$ fulfils this requirement as it comes equipped with a partial operation $-\colon\mathrm{\mathrm{dom}(-)}\to{\mathbf{\Gamma}}$, where $\mathrm{\mathrm{dom}(-)}=\{(x,y)\in{\mathbf{\Gamma}}\times{\mathbf{\Gamma}}\mid y\leq x\}$ and

[TABLE]

In fact, this (partial) operation is dual to the truncated addition on the lattice $\mathbf{L}$. However, explaining this would require us to delve into extended Priestley duality for lattices with operations, which is beyond the scope of this paper. See [9] and also [7, 8] for details. It also follows from the general theory that there exists another partial operation definable from $-$, namely:

[TABLE]

Now we collect some basic properties of $-$ and $\sim$, needed in Section 4, which follow from the general theory of [7, 8]. First, recall that a map into an ordered topological space is lower (resp. upper) semicontinuous provided the preimage of any open down-set (resp. open up-set) is open.

Lemma 1

If $\mathrm{\mathrm{dom}(-)}$ is seen as a subspace of ${\mathbf{\Gamma}}\times{\mathbf{\Gamma}}{}^{\partial}$, the following hold:

$\mathrm{\mathrm{dom}(-)}$* is a closed up-set in ${\mathbf{\Gamma}}\times{\mathbf{\Gamma}}{}^{\partial}$;* 2. 2.

both $-\colon\mathrm{\mathrm{dom}(-)}\to{\mathbf{\Gamma}}$ and $\sim\colon\mathrm{\mathrm{dom}(-)}\to{\mathbf{\Gamma}}$ are monotone in the first coordinate, and antitone in the second; 3. 3.

$-\colon\mathrm{\mathrm{dom}(-)}\to{\mathbf{\Gamma}}$* is lower semicontinuous;* 4. 4.

$\sim\colon\mathrm{\mathrm{dom}(-)}\to{\mathbf{\Gamma}}$* is upper semicontinuous.*

3.2 The retraction ${\mathbf{\Gamma}}\twoheadrightarrow[0,1]$

In this section we show that, with respect to appropriate topologies, the unit interval $[0,1]$ can be obtained as a topological retract of ${\mathbf{\Gamma}}$, in a way which is compatible with the operation $-$. This will be important in Sections 4 and 5, where we need to move between [0,1]-valued and ${\mathbf{\Gamma}}$-valued measures. Let us define the monotone surjection given by collapsing the doubled elements:

[TABLE]

The map $\gamma$ has a right adjoint, given by

[TABLE]

Indeed, it is readily seen that $\gamma(y)\leq x$ iff $y\leq\iota(x)$, for all $y\in{\mathbf{\Gamma}}$ and $x\in[0,1]$. The composition $\gamma\cdot\iota$ coincides with the identity on $[0,1]$, i.e. $\iota$ is a section of $\gamma$. Moreover, this retraction lifts to a topological retract provided we equip ${\mathbf{\Gamma}}$ and $[0,1]$ with the topologies consisting of the open down-sets:

Lemma 2

The map $\gamma\colon{\mathbf{\Gamma}}\to[0,1]$ is continuous and the map $\iota\colon[0,1]\to{\mathbf{\Gamma}}$ is lower semicontinuous.

Proof

To check continuity of $\gamma$ observe that, for a rational $q\in(0,1)$, $\gamma^{-1}(q,1]$ and $\gamma^{-1}[0,q)$ coincide, respectively, with the open sets

[TABLE]

Also, $\iota$ is lower semicontinuous, for $\iota^{-1}(\mathord{\downarrow}\mkern 1.0muq^{-})=[0,q)$ whenever $q\in\mathbb{Q}\cap(0,1]$.∎

It is easy to see that both $\gamma$ and $\iota$ preserve the minus structure available on ${\mathbf{\Gamma}}$ and [0,1] (the unit interval is equipped with the usual minus operation $x-y$ defined whenever $y\leq x$), that is,

• •

$\gamma(x-y)=\gamma(x\sim y)=\gamma(x)-\gamma(y)$ whenever $y\leq x$ in ${\mathbf{\Gamma}}$, and

• •

$\iota(x-y)=\iota(x)-\iota(y)$ whenever $y\leq x$ in [0,1].

Remark

$\iota\colon[0,1]\to{\mathbf{\Gamma}}$ is not upper semicontinuous because, for every $q\in\mathbb{Q}\cap[0,1]$, $\iota^{-1}(\mathord{\uparrow}\mkern 1.0muq^{\circ})=\{x\in[0,1]\mid q^{\circ}\leq\iota(x)\}=\{x\in[0,1]\mid\gamma(q^{\circ})\leq x\}=[q,1]$.

4 Spaces of measures valued in ${\mathbf{\Gamma}}$ and in $[0,1]$

The aim of this section is to replace $[0,1]$-valued measures by ${\mathbf{\Gamma}}$-valued measures. The reason for doing this is two-fold. First, the space of ${\mathbf{\Gamma}}$-valued measures is Priestley (Proposition 1), and thus amenable to a duality theoretic treatment and a dual logic interpretation (cf. Section 6). Second, it retains more topological information than the space of $[0,1]$-valued measures. Indeed, the former retracts onto the latter (Theorem 4.1).

Let $D$ be a distributive lattice. Recall that, classically, a monotone function $m\colon D\to[0,1]$ is a (finitely additive, probability) measure provided $m(0)=0$, $m(1)=1$, and $m(a)+m(b)=m(a\vee b)+m(a\wedge b)$ for every $a,b\in D$. The latter property is equivalently expressed as

[TABLE]

We write $\operatorname{\mathcal{M}_{I}}(D)$ for the set of all measures $D\to[0,1]$, and regard it as an ordered topological space, with the structure induced by the product order and product topology of $[0,1]^{D}$. The notion of (finitely additive, probability) ${\mathbf{\Gamma}}$-valued measure is analogous to the classical one, except that the finite additivity property (6) splits into two conditions, involving $-$ and $\sim$.

Definition 1

Let $D$ be a distributive lattice. A ${\mathbf{\Gamma}}$-valued measure (or simply a measure) on $D$ is a function $\mu\colon D\to{\mathbf{\Gamma}}$ such that

$\mu(0)=0^{\circ}$ and $\mu(1)=1^{\circ}$, 2. 2.

$\mu$ is monotone, and 3. 3.

for all $a,b\in D$,

[TABLE]

We denote by $\operatorname{\mathcal{M}_{\Gamma}}(D)$ the subspace of ${\mathbf{\Gamma}}^{D}$ consisting of the measures $\mu\colon D\to{\mathbf{\Gamma}}$.

Since ${\mathbf{\Gamma}}$ is a Priestley space, so is ${\mathbf{\Gamma}}^{D}$ equipped with the product order and topology. Hence, we regard $\operatorname{\mathcal{M}_{\Gamma}}(D)$ as an ordered topological space, whose topology and order are induced by those of ${\mathbf{\Gamma}}^{D}$. In fact $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is a Priestley space:

Proposition 1

For any distributive lattice $D$, $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is a Priestley space.

Proof

It suffices to show that $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is a closed subspace of ${\mathbf{\Gamma}}^{D}$. Let

[TABLE]

Note that the evaluation maps $\mathrm{ev}_{a}\colon{\mathbf{\Gamma}}^{D}\to{\mathbf{\Gamma}}$, $f\mapsto f(a)$, are continuous for every $a\in D$. Thus, the first set in the intersection defining $C_{1,2}$ is closed because it is the equaliser of the evaluation map $\mathrm{ev}_{0}$ and the constant map of value $0^{\circ}$. Similarly, for the set $\{f\in{\mathbf{\Gamma}}^{D}\mid f(1)=1^{\circ}\}$. The last one is the intersection of the sets of the form $\langle\mathrm{ev}_{a},\mathrm{ev}_{b}\rangle^{-1}(\leq)$, which are closed because $\leq$ is closed in ${\mathbf{\Gamma}}\times{\mathbf{\Gamma}}$. Whence, $C_{1,2}$ is a closed subset of ${\mathbf{\Gamma}}^{D}$. Moreover,

[TABLE]

From semicontinuity of $-$ and $\sim$ (Lemma 1) and the following well-known fact in order-topology we conclude that $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is closed in ${\mathbf{\Gamma}}^{D}$.

Fact

Let $X,Y$ be compact ordered spaces, $f\colon X\to Y$ a lower semicontinuous function and $g\colon X\to Y$ an upper semicontinuous function. If $X^{\prime}$ is a closed subset of $X$, then so is $E=\{x\in X^{\prime}\mid g(x)\leq f(x)\}$.∎

Next, we prove a property which is very useful when approximating a fragment of a logic by smaller fragments (see, e.g., Section 5.1). Let us denote by $\mathbf{DLat}$ the category of distributive lattices and homomorphisms, and by $\mathbf{Pries}$ the category of Priestley spaces and continuous monotone maps.

Proposition 2

The assignment $D\mapsto\operatorname{\mathcal{M}_{\Gamma}}(D)$ yields a contravariant functor $\operatorname{\mathcal{M}_{\Gamma}}\colon\mathbf{DLat}\to\mathbf{Pries}$ which sends directed colimits to codirected limits.

Proof

If $h\colon D\to E$ is a lattice homomorphism and $\mu\colon E\to{\mathbf{\Gamma}}$ is a measure, it is not difficult to see that $\operatorname{\mathcal{M}_{\Gamma}}(h)(\mu)=\mu\cdot h\colon D\to{\mathbf{\Gamma}}$ is a measure. The mapping $\operatorname{\mathcal{M}_{\Gamma}}(h)\colon\operatorname{\mathcal{M}_{\Gamma}}(E)\to\operatorname{\mathcal{M}_{\Gamma}}(D)$ is clearly monotone. For continuity, recall that the topology of $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is generated by the sets $\llbracket a<q\rrbracket=\{\nu\colon D\to{\mathbf{\Gamma}}\mid\nu(a)<q^{\circ}\}$ and $\llbracket a\geq q\rrbracket=\{\nu\colon D\to{\mathbf{\Gamma}}\mid\nu(a)\geq q^{\circ}\}$, with $a\in D$ and $q\in\mathbb{Q}\cap[0,1]$. We have

[TABLE]

which is open in $\operatorname{\mathcal{M}_{\Gamma}}(E)$. Similarly, $\operatorname{\mathcal{M}_{\Gamma}}(h)^{-1}(\llbracket a\geq q\rrbracket)=\llbracket h(a)\geq q\rrbracket$, showing that $\operatorname{\mathcal{M}_{\Gamma}}(h)$ is continuous. Thus, $\operatorname{\mathcal{M}_{\Gamma}}$ is a contravariant functor.

The rest of the proof is a routine verification.∎

Remark 1

We work with the contravariant functor $\operatorname{\mathcal{M}_{\Gamma}}\colon\mathbf{DLat}\to\mathbf{Pries}$ because $\operatorname{\mathcal{M}_{\Gamma}}$ is concretely defined on the lattice side. However, by Priestley duality, $\mathbf{DLat}$ is dually equivalent to $\mathbf{Pries}$, so we can think of $\operatorname{\mathcal{M}_{\Gamma}}$ as a covariant functor $\mathbf{Pries}\to\mathbf{Pries}$ (this is the perspective traditionally adopted in analysis, and also in the works of Nešetřil and Ossona de Mendez). From this viewpoint, Section 6 provides a description of the endofunctor on $\mathbf{DLat}$ dual to $\operatorname{\mathcal{M}_{\Gamma}}\colon\mathbf{Pries}\to\mathbf{Pries}$.

Recall the maps $\gamma\colon{\mathbf{\Gamma}}\to[0,1]$ and $\iota\colon[0,1]\to{\mathbf{\Gamma}}$ from equations (4)–(5). In Section 3.2 we showed that this is a retraction-section pair. In Theorem 4.1 this retraction is lifted to the spaces of measures. We start with an easy observation:

Lemma 3

Let $D$ be a distributive lattice. The following statements hold:

for every $\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)$, $\gamma\cdot\mu\in\operatorname{\mathcal{M}_{I}}(D)$, 2. 2.

for every $m\in\operatorname{\mathcal{M}_{I}}(D)$, $\iota\cdot m\in\operatorname{\mathcal{M}_{\Gamma}}(D)$.

Proof

$1$. The only non-trivial condition to verify is finite additivity. In view of the discussion after Lemma 2, the map $\gamma$ preserves both minus operations on ${\mathbf{\Gamma}}$. Hence, for every $a,b\in D$, the inequalities $\mu(a)\sim\mu(a\wedge b)\leq\mu(a\vee b)-\mu(b)$ and $\mu(a)-\mu(a\wedge b)\geq\mu(a\vee b)\sim\mu(b)$ imply that $\gamma\cdot\mu(a)-\gamma\cdot\mu(a\wedge b)=\gamma\cdot\mu(a\vee b)-\gamma\cdot\mu(b)$.

$2$. The first two conditions in Definition 1 are immediate. The third condition follows from the fact that $\iota(r-s)=\iota(r)-\iota(s)$ whenever $s\leq r$ in [0,1], and $x\sim y\leq x-y$ for every $(x,y)\in\mathrm{\mathrm{dom}(-)}$.∎

In view of the previous lemma, there are well-defined functions

[TABLE]

Lemma 4

$\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(D)\to\operatorname{\mathcal{M}_{I}}(D)$* is a continuous and monotone map.*

Proof

The topology of $\operatorname{\mathcal{M}_{I}}(D)$ is generated by the sets of the form $\{m\in\operatorname{\mathcal{M}_{I}}(D)\mid m(a)\in O\}$, for $a\in D$ and $O$ an open subset of $[0,1]$. In turn,

[TABLE]

is open in $\operatorname{\mathcal{M}_{\Gamma}}(D)$ because $\gamma\colon{\mathbf{\Gamma}}\to[0,1]$ is continuous by Lemma 2. This shows that $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(D)\to\operatorname{\mathcal{M}_{I}}(D)$ is continuous. Monotonicity is immediate.∎

Note that $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(D)\to\operatorname{\mathcal{M}_{I}}(D)$ is surjective, since it admits $\iota^{\#}$ as a (set-theoretic) section. It follows that $\operatorname{\mathcal{M}_{I}}(D)$ is a compact ordered space:

Corollary 1

For each distributive lattice $D$, $\operatorname{\mathcal{M}_{I}}(D)$ is a compact ordered space.

Proof

The surjection $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(D)\to\operatorname{\mathcal{M}_{I}}(D)$ is continuous (Lemma 4). Since $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is compact by Proposition 1, so is $\operatorname{\mathcal{M}_{I}}(D)$. The order of $\operatorname{\mathcal{M}_{I}}(D)$ is clearly closed in the product topology, thus $\operatorname{\mathcal{M}_{I}}(D)$ is a compact ordered space.∎

Finally, we see that the set-theoretic retraction of $\operatorname{\mathcal{M}_{\Gamma}}(D)$ onto $\operatorname{\mathcal{M}_{I}}(D)$ lifts to the topological setting, provided we restrict to the down-set topologies. If $(X,\leq)$ is a partially ordered topological space, write $X^{\downarrow}$ for the space with the same underlying set as $X$ and whose topology consists of the open down-sets of $X$.

Theorem 4.1

The maps $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(D)^{\downarrow}\to\operatorname{\mathcal{M}_{I}}(D)^{\downarrow}$ and $\iota^{\#}\colon\operatorname{\mathcal{M}_{I}}(D)^{\downarrow}\to\operatorname{\mathcal{M}_{\Gamma}}(D)^{\downarrow}$ are a retraction-section pair of topological spaces.

Proof

It suffices to show that $\gamma^{\#}$ and $\iota^{\#}$ are continuous. It is not difficult to see, using Lemma 4, that $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(D)^{\downarrow}\to\operatorname{\mathcal{M}_{I}}(D)^{\downarrow}$ is continuous. For the continuity of $\iota^{\#}$, note that the topology of $\operatorname{\mathcal{M}_{\Gamma}}(D)^{\downarrow}$ is generated by the sets of the form $\{\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)\mid\mu(a)\leq q^{-}\}$, for $a\in D$ and $q\in\mathbb{Q}\cap(0,1]$. We have

[TABLE]

which is an open set in $\operatorname{\mathcal{M}_{I}}(D)^{\downarrow}$. This concludes the proof.∎

5 The ${\mathbf{\Gamma}}$-valued Stone pairing and limits of finite structures

In the work of Nešetřil and Ossona de Mendez, the Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>$ is $[0,1]$-valued, i.e. an element of $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$. In this section, we show that basically the same construction for the recognisers arising from the application of a layer of semiring quantifiers in logic on words (cf. Section 2.3) provides an embedding of finite $\sigma$-structures into the space of ${\mathbf{\Gamma}}$-valued measures. It turns out that this embedding is a ${\mathbf{\Gamma}}$-valued version of the Stone pairing. Hereafter we make a notational difference, writing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{I}}$ for the (classical) [0,1]-valued Stone pairing.

The main ingredient of the construction are the ${\mathbf{\Gamma}}$-valued finitely supported functions. To start with, we point out that the partial operation $-$ on ${\mathbf{\Gamma}}$ uniquely determines a partial “plus” operation on ${\mathbf{\Gamma}}$. Define

[TABLE]

by the following rules (whenever the expressions make sense):

[TABLE]

Then, for every $y\in{\mathbf{\Gamma}}$, $(\mkern 1.5mu\text{-}\mkern 1.5mu)+y$ is left adjoint to $(\mkern 1.5mu\text{-}\mkern 1.5mu)-y$.

Definition 2

For any set $X$, ${\mathcal{F}}(X)$ is the set of all functions $f\colon X\to{\mathbf{\Gamma}}$ s.t.

the set $\mathrm{supp}(f)=\{x\in X\mid f(x)\not=0^{\circ}\}$ is finite, and 2. 2.

$f(x_{1})+\cdots+f(x_{n})$ is defined and equal to $1^{\circ}$, where $\mathrm{supp}(f)=\{x_{1},\ldots,x_{n}\}$.

To improve readability, if the sum $y_{1}+\cdots+y_{m}$ exists in ${\mathbf{\Gamma}}$, we denote it $\sum_{i=1}^{m}{y_{i}}$. Finitely supported functions in the above sense always determine measures over the power-set algebra (the proof is an easy verification and is omitted):

Lemma 5

Let $X$ be any set. There is a well-defined mapping \int\colon{\mathcal{F}}(X)\to\operatorname{\mathcal{M}_{\Gamma}}(\raisebox{2.03998pt}{\Large\wp}(X)), assigning to every $f\in{\mathcal{F}}(X)$ the measure

[TABLE]

5.1 The ${\mathbf{\Gamma}}$-valued Stone pairing and logic on words

Fix a countably infinite set of variables $\{v_{1},v_{2},\dots\}$. Recall that $\mathrm{FO}_{n}(\sigma)$ is the Lindenbaum-Tarski algebra of first-order formulas with free variables among $\{v_{1},\dots,v_{n}\}$. The dual space of $\mathrm{FO}_{n}(\sigma)$ is the space of $n$-types $\operatorname{Typ}_{n}(\sigma)$. Its points are the equivalence classes of pairs $(A,\alpha)$, where $A$ is a $\sigma$-structure and $\alpha\colon\{v_{1},\dots,v_{n}\}\to A$ is an interpretation of the variables. Write $\mathrm{Fin}(\sigma)$ for the set of all finite $\sigma$-structures. We have a map $\mathrm{Fin}(\sigma)\to{\mathcal{F}}(\operatorname{Typ}_{n}(\sigma))$ defined by $A\mapsto f_{n}^{A}$, where $f_{n}^{A}$ is the function which sends an equivalence class $E\in\operatorname{Typ}_{n}(\sigma)$ to

[TABLE]

By Lemma 5, we get a measure \int f_{n}^{A}\colon\raisebox{2.03998pt}{\Large\wp}(\operatorname{Typ}_{n}(\sigma))\to{\mathbf{\Gamma}}. Now, for each $\varphi\in\mathrm{FO}_{n}(\sigma)$, let $\llbracket\varphi\rrbracket_{n}\subseteq\operatorname{Typ}_{n}(\sigma)$ be the set of (equivalence classes of) $\sigma$-structures with interpretations satisfying $\varphi$. By Stone duality we obtain an embedding \llbracket\mkern 1.5mu\text{-}\mkern 1.5mu\rrbracket_{n}\colon\mathrm{FO}_{n}(\sigma)\hookrightarrow\raisebox{2.03998pt}{\Large\wp}(\operatorname{Typ}_{n}(\sigma)). Restricting $\int f_{n}^{A}$ to $\mathrm{FO}_{n}(\sigma)$, we get a measure

[TABLE]

Summing up, we have the composite map

[TABLE]

Essentially the same construction is featured in logic on words, cf. equation (2):

• •

The set of finite $\sigma$-structures $\mathrm{Fin}(\sigma)$ corresponds to the set of finite words $A^{*}$.

• •

The collection $\operatorname{Typ}_{n}(\sigma)$ of (equivalence classes of) $\sigma$-structures with interpretations corresponds to $(A\times 2)^{*}$ or, interchangeably, $\beta(A\times 2)^{*}$ (in the case of one free variable).

• •

The fragment $\mathrm{FO}_{n}(\sigma)$ of first-order logic corresponds to the Boolean algebra of languages, defined by formulas with a free variable, dual to the Boolean space $X$ appearing in (2).

• •

The first map in the composite (7) sends a finite structure $A$ to the measure $\int f_{n}^{A}$ which, evaluated on $K\subseteq\operatorname{Typ}_{n}(\sigma)$, counts the (proportion of) interpretations $\alpha\colon\{v_{1},\dots,v_{n}\}\to A$ such that $(A,\alpha)\in K$, similarly to $R$ from (2).

• •

Finally, the second map in (7) sends a measure in \operatorname{\mathcal{M}_{\Gamma}}(\raisebox{2.03998pt}{\Large\wp}(\operatorname{Typ}_{n}(\sigma))) to its pushforward along \llbracket\mkern 1.5mu\text{-}\mkern 1.5mu\rrbracket_{n}\colon\mathrm{FO}_{n}(\sigma)\hookrightarrow\raisebox{2.03998pt}{\Large\wp}(\operatorname{Typ}_{n}(\sigma)). This is the second map in the composition (2).

On the other hand, the assignment $A\mapsto\mu_{n}^{A}$ defined in (7) is also closely related to the classical Stone pairing. Indeed, for every formula $\varphi$ in $\mathrm{FO}_{n}(\sigma)$,

[TABLE]

In this sense, $\mu_{n}^{A}$ can be regarded as a ${\mathbf{\Gamma}}$-valued Stone pairing, relative to the fragment $\mathrm{FO}_{n}(\sigma)$. Next, we show how to extend this to the full first-order logic $\mathrm{FO}(\sigma)$. First, we observe that the construction is invariant under extensions of the set of free variables (the proof is the same as in the classical case).

Lemma 6

Given $m,n\in\mathbb{N}$ and $A\in\mathrm{Fin}(\sigma)$, if $m\geq n$ then $(\mu_{m}^{A})_{\mathord{\upharpoonright}\mathrm{FO}_{n}(\sigma)}=\mu_{n}^{A}$.

The Lindenbaum-Tarski algebra of all first-order formulas $\mathrm{FO}(\sigma)$ is the directed colimit of the Boolean subalgebras $\mathrm{FO}_{n}(\sigma)$, for $n\in\mathbb{N}$. Since the functor $\operatorname{\mathcal{M}_{\Gamma}}$ turns directed colimits into codirected limits (Proposition 2), the Priestley space $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ is the limit of the diagram

[TABLE]

where, for any $\mu\colon\mathrm{FO}_{m}(\sigma)\to{\mathbf{\Gamma}}$ in $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}_{m}(\sigma))$, the measure $q_{n,m}(\mu)$ is the restriction of $\mu$ to $\mathrm{FO}_{n}(\sigma)$. In view of Lemma 6, for every $A\in\mathrm{Fin}(\sigma)$, the tuple $(\mu_{n}^{A})_{n\in\mathbb{N}}$ is compatible with the restriction maps. Thus, recalling that limits in the category of Priestley spaces are computed as in sets, by universality of the limit construction, this tuple yields a measure

[TABLE]

in the space $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$. This we call the ${\mathbf{\Gamma}}$-valued Stone pairing associated with $A$. As in the classical case, it is not difficult to see that the mapping $A\mapsto\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>_{\mathrm{\Gamma}}$ gives an embedding $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{\Gamma}}\colon\mathrm{Fin}(\sigma)\hookrightarrow\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$. The following theorem illustrates the relation between the classical Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{I}}\colon\mathrm{Fin}(\sigma)\hookrightarrow\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$, and the ${\mathbf{\Gamma}}$-valued one.

Theorem 5.1

The following diagram commutes:

{\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))}$${\mathrm{Fin}(\sigma)}$${\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))}$$\scriptstyle{\gamma^{\#}}$$\scriptstyle{\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{\Gamma}}}$$\scriptstyle{\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{I}}}$$\scriptstyle{\iota^{\#}}

Proof

Fix an arbitrary finite structure $A\in\mathrm{Fin}(\sigma)$. Let $\varphi$ be a formula in $\mathrm{FO}(\sigma)$ with free variables among $\{v_{1},\dots,v_{n}\}$, for some $n\in\mathbb{N}$. By construction, $\left<\varphi,A\right>_{\mathrm{\Gamma}}=\mu_{n}^{A}(\varphi)$. Therefore, by equation (8), $\left<\varphi,A\right>_{\mathrm{\Gamma}}=(\left<\varphi,A\right>_{\mathrm{I}})^{\circ}$. The statement then follows at once.∎

Remark

The construction in this section works also for proper fragments, i.e. for sublattices $D\subseteq\mathrm{FO}(\sigma)$. This corresponds to composing the embedding $\mathrm{Fin}(\sigma)\hookrightarrow\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ with the restriction map $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))\to\operatorname{\mathcal{M}_{\Gamma}}(D)$ sending $\mu\colon\mathrm{FO}(\sigma)\to{\mathbf{\Gamma}}$ to $\mu_{\mathord{\upharpoonright}D}\colon D\to{\mathbf{\Gamma}}$. The only difference is that the ensuing map $\mathrm{Fin}(\sigma)\to\operatorname{\mathcal{M}_{\Gamma}}(D)$ need not be injective, in general.

5.2 Limits in the spaces of measures

By Theorem 5.1 the ${\mathbf{\Gamma}}$-valued Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{\Gamma}}$ and the classical Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{I}}$ determine each other. However, the notions of convergence associated with the spaces $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ and $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$ are different: since the topology of $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ is richer, there are “fewer” convergent sequences. Recall from Lemma 4 that $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))\to\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$ is continuous. Also, $\gamma^{\#}(\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>_{\mathrm{\Gamma}})=\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>_{\mathrm{I}}$ by Theorem 5.1. Thus, for any sequence of finite structures $(A_{n})_{n\in\mathbb{N}}$, if

$\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A_{n}\right>_{\mathrm{\Gamma}}$ converges to a measure $\mu$ in $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$

then

$\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A_{n}\right>_{\mathrm{I}}$ converges to the measure $\gamma^{\#}(\mu)$ in $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$.

The converse is not true. For example, consider the signature $\sigma=\{<\}$ consisting of a single binary relation symbol, and let $(A_{n})_{n\in\mathbb{N}}$ be the sequence of finite posets displayed in the picture below.

A_{1}$$A_{2}$$A_{3}$$A_{4}$$A_{5}$$A_{6}$$\cdots

Let $\psi(x)\approx\forall y\,\neg(x<y)\wedge\exists z\,\neg(z<x)\wedge\neg(z=x)$ be the formula stating that $x$ is maximal but not the maximum in the order given by $<$. Then, for the sublattice $D=\{\mathbf{f},\psi,\mathbf{t}\}$ of $\mathrm{FO}(\sigma)$, the sequences $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A_{n}\right>_{\mathrm{\Gamma}}$ and $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A_{n}\right>_{\mathrm{I}}$ converge in $\operatorname{\mathcal{M}_{\Gamma}}(D)$ and $\operatorname{\mathcal{M}_{I}}(D)$, respectively. However, if we consider the Boolean algebra $B=\{\mathbf{f},\psi,\neg\psi,\mathbf{t}\}$, then the $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A_{n}\right>_{\mathrm{I}}$’s still converge whereas the $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A_{n}\right>_{\mathrm{\Gamma}}$’s do not. Indeed, the following sequence does not converge in ${\mathbf{\Gamma}}$:

[TABLE]

Next, identify $\mathrm{Fin}(\sigma)$ with a subset of $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ (resp. $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$) through $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{\Gamma}}$ (resp. $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{I}}$). A central question in the theory of structural limits, cf. [15], is to determine the closure of $\mathrm{Fin}(\sigma)$ in $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$, which consists precisely of the limits of sequences of finite structures. The following theorem gives an answer to this question in terms of the corresponding question for $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$.

Theorem 5.2

Let $\overline{\mathrm{Fin}(\sigma)}$ denote the closure of $\mathrm{Fin}(\sigma)$ in $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$. Then the set $\gamma^{\#}(\overline{\mathrm{Fin}(\sigma)})$ coincides with the closure of $\mathrm{Fin}(\sigma)$ in $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$.

Proof

Write $U$ for the image of $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{\Gamma}}\colon\mathrm{Fin}(\sigma)\hookrightarrow\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$, and $V$ for the image of $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{I}}\colon\mathrm{Fin}(\sigma)\hookrightarrow\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$. We must prove that $\gamma^{\#}(\overline{U})=\overline{V}$. By Theorem 5.1, $\gamma^{\#}(U)=V$. The map $\gamma^{\#}\colon\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))\to\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$ is continuous (Lemma 4), and the spaces $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ and $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$ are compact Hausdorff (Proposition 1 and Corollary 1). Since continuous maps between compact Hausdorff spaces are closed, $\gamma^{\#}(\overline{U})=\overline{\gamma^{\#}(U)}=\overline{V}$. ∎

6 The logic of measures

Let $D$ be a distributive lattice. We know from Proposition 1 that the space $\operatorname{\mathcal{M}_{\Gamma}}(D)$ of ${\mathbf{\Gamma}}$-valued measures on $D$ is a Priestley space, whence it has a dual distributive lattice $\operatorname{\mathbf{P}}(D)$. In this section we show that $\operatorname{\mathbf{P}}(D)$ can be represented as the Lindenbaum-Tarski algebra for a propositional logic $P\mkern-1.0mu\mathcal{L}_{D}$ obtained from $D$ by adding probabilistic quantifiers. Since we adopt a logical perspective, we write $\mathbf{f}$ and $\mathbf{t}$ for the bottom and top elements of $D$, respectively.

The set of propositional variables of $P\mkern-1.0mu\mathcal{L}_{D}$ consists of the symbols $\mathbb{P}_{\geq p}\,a$, for every $a\in D$ and $p\in\mathbb{Q}\cap[0,1]$. For every measure $\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)$, we set

[TABLE]

This satisfaction relation extends in the obvious way to the closure under finite conjunctions and finite disjunctions of the set of propositional variables. Define

[TABLE]

Also, write $\models\varphi$ if $\mu\models\varphi$ for every $\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)$, and $\varphi\models$ if there is no $\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)$ with $\mu\models\varphi$.

Consider the following conditions, for any $p,q,r\in\mathbb{Q}\cap[0,1]$ and $a,b\in D$.

1. (L1)

$\mathbb{P}_{\geq q}\,a\models\mathbb{P}_{\geq p}\,a$ whenever $p\leq q$ 2. (L2)

$\mathbb{P}_{\geq p}\,\mathbf{f}\models{}$ whenever $p>0$, ${}\models\mathbb{P}_{\geq 0}\,\mathbf{f}$ and ${}\models\mathbb{P}_{\geq q}\,\mathbf{t}$ 3. (L3)

$\mathbb{P}_{\geq q}\,a\models\mathbb{P}_{\geq q}\,b$ whenever $a\leq b$ 4. (L4)

$\mathbb{P}_{\geq p}\,a\,\wedge\,\mathbb{P}_{\geq q}\,b\models\mathbb{P}_{\geq p+q-r}\,(a\vee b)\,\vee\,\mathbb{P}_{\geq r}\,(a\wedge b)$ whenever $0\leq p+q-r\leq 1$ 5. (L5)

$\mathbb{P}_{\geq p+q-r}\,(a\vee b)\,\wedge\,\mathbb{P}_{\geq r}\,(a\wedge b)\models\mathbb{P}_{\geq p}\,a\,\vee\,\mathbb{P}_{\geq q}\,b$ whenever $0\leq p+q-r\leq 1$

It is not hard to see that the interpretation in (9) validates these conditions:

Lemma 7

The conditions (L1)–(L5) are satisfied in $\operatorname{\mathcal{M}_{\Gamma}}(D)$.

Write $\operatorname{\mathbf{P}}(D)$ for the quotient of the free distributive lattice on the set

[TABLE]

with respect to the congruence generated by the conditions (L1)–(L5).

Proposition 3

Let $F\subseteq\operatorname{\mathbf{P}}(D)$ be a prime filter. The assignment

[TABLE]

Proof

Items (L2) and (L3) take care of the first two conditions defining ${\mathbf{\Gamma}}$-valued measures (cf. Definition 1). We prove the first half of the third condition, as the other half is proved in a similar fashion. We must show that, for every $a,b\in D$,

[TABLE]

It is not hard to show that $\mu_{F}(a)-r^{\circ}=\bigvee\{p_{1}^{\circ}-r^{\circ}\mid r^{\circ}\leq p_{1}^{\circ}\leq\mu_{F}(a)\}$, and $x-(\mkern 1.5mu\text{-}\mkern 1.5mu)$ transforms non-empty joins into meets (this follows by Scott continuity of $x-(\mkern 1.5mu\text{-}\mkern 1.5mu)$ seen as a map $[0^{\circ},x]\to{\mathbf{\Gamma}}^{\partial}$). Hence, equation (10) is equivalent to

[TABLE]

To settle this inequality it is enough to show that, provided $\mu_{F}(a\wedge b)<r^{\circ}\leq p^{\circ}\leq\mu_{F}(a)$ and $q^{\circ}\leq\mu_{F}(b)$, we have $(p-r)^{\circ}\leq\mu_{F}(a\vee b)-q^{\circ}$. The latter inequality is equivalent to $(p+q-r)^{\circ}\leq\mu_{F}(a\vee b)$. In turn, using (L4) and the fact that $F$ is a prime filter, $\mathbb{P}_{\geq p}\,a,\mathbb{P}_{\geq q}\,b\in F$ and $\mathbb{P}_{\geq r}\,(a\wedge b)\notin F$ entail $\mathbb{P}_{\geq p+q-r}\,(a\vee b)\in F$. Whence,

[TABLE]

We can now describe the dual lattice of $\operatorname{\mathcal{M}_{\Gamma}}(D)$ as the Lindenbaum-Tarski algebra for the logic $P\mkern-1.0mu\mathcal{L}_{D}$, built from the propositional variables $\mathbb{P}_{\geq p}\,a$ by imposing the laws (L1)–(L5).

Theorem 6.1

Let $D$ be a distributive lattice. Then the lattice $\operatorname{\mathbf{P}}(D)$ is isomorphic to the distributive lattice dual to the Priestley space $\operatorname{\mathcal{M}_{\Gamma}}(D)$.

Proof

Let $X_{\operatorname{\mathbf{P}}(D)}$ be the space dual to $\operatorname{\mathbf{P}}(D)$. By Proposition 3 there is a map $\vartheta\colon X_{\operatorname{\mathbf{P}}(D)}\to\operatorname{\mathcal{M}_{\Gamma}}(D)$, $F\mapsto\mu_{F}$. We claim that $\vartheta$ is an isomorphism of Priestley space. Clearly, $\vartheta$ is monotone. If $\mu_{F_{1}}(a)\not\leq\mu_{F_{2}}(a)$ for some $a\in D$, we have

[TABLE]

Equation (11) implies the existence of $p,q$ satisfying $\mathbb{P}_{\geq q}\,a\in F_{1}$, $\mathbb{P}_{\geq p}\,a\notin F_{2}$ and $q\geq p$. It follows by (L1) that $\mathbb{P}_{\geq p}\,a\in F_{1}$. We conclude that $\mathbb{P}_{\geq p}\,a\in F_{1}\setminus F_{2}$, whence $F_{1}\not\subseteq F_{2}$. This shows that $\vartheta$ is an order embedding, whence injective.

We prove that $\vartheta$ is also surjective, thus a bijection. Fix a measure $\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)$. It is not hard to see, using Lemma 7, that the filter $F_{\mu}\subseteq\operatorname{\mathbf{P}}(D)$ generated by

[TABLE]

is prime. Further, $\vartheta(F_{\mu})(a)=\bigvee{\{q^{\circ}\mid\mathbb{P}_{\geq q}\,a\in F_{\mu}\}}=\bigvee{\{q^{\circ}\mid\mu(a)\geq q^{\circ}\}}=\mu(a)$ for every $a\in D$. Hence, $\vartheta(F_{\mu})=\mu$ and $\vartheta$ is surjective.

To settle the theorem it remains to show that $\vartheta$ is continuous. Note that for a basic clopen of the form $C=\{\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)\mid\mu(a)\geq p^{\circ}\}$ where $a\in D$ and $p\in\mathbb{Q}\cap[0,1]$, the preimage $\vartheta^{-1}(C)=\{F\subseteq\operatorname{\mathbf{P}}(D)\mid\mu_{F}(a)\geq p^{\circ}\}$ is equal to

[TABLE]

which is a clopen of $X_{\operatorname{\mathbf{P}}(D)}$. Similarly, if $C=\{\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)\mid\mu(a)\leq q^{-}\}$ for some $a\in D$ and $q\in\mathbb{Q}\cap(0,1]$, by the claim above $\vartheta^{-1}(C)=\{F\in X_{\operatorname{\mathbf{P}}(D)}\mid\mathbb{P}_{\geq q}\,a\notin F\}$, which is again a clopen of $X_{\operatorname{\mathbf{P}}(D)}$.∎

By Theorem 6.1, for any distributive lattice $D$, the lattice of clopen up-sets of $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is isomorphic to the Lindenbaum-Tarski algebra $\operatorname{\mathbf{P}}(D)$ of our positive propositional logic $P\mkern-1.0mu\mathcal{L}_{D}$. Moving from the lattice of clopen up-sets to the Boolean algebra of all clopens logically corresponds to adding negation to the logic. The logic obtained this way can be presented as follows. Introduce a new propositional variable $\mathbb{P}_{<q}\,a$, for each $a\in D$ and $q\in\mathbb{Q}\cap[0,1]$. For a measure $\mu\in\operatorname{\mathcal{M}_{\Gamma}}(D)$, set

[TABLE]

We also add a new rule, stating that $\mathbb{P}_{<q}\,a$ is the negation of $\mathbb{P}_{\geq q}\,a$:

1. (L6)

$\mathbb{P}_{<q}\,a\wedge\mathbb{P}_{\geq q}\,a\models{}$ and ${}\models\mathbb{P}_{<q}\,a\vee\mathbb{P}_{\geq q}\,a$

Clearly, (L6) is satisfied in $\operatorname{\mathcal{M}_{\Gamma}}(D)$. Moreover, the Boolean algebra of all clopens of $\operatorname{\mathcal{M}_{\Gamma}}(D)$ is isomorphic to the quotient of the free distributive lattice on

[TABLE]

with respect to the congruence generated by the conditions (L1)–(L6).

Specialising to $\mathrm{FO}(\sigma)$.

Let us briefly discuss what happens when we instantiate $D$ with the full first-order logic $\mathrm{FO}(\sigma)$. For a formula $\varphi\in\mathrm{FO}(\sigma)$ with free variables $v_{1},\dots,v_{n}$ and a $q\in\mathbb{Q}\cap[0,1]$, we have two new sentences $\mathbb{P}_{\geq q}\,\varphi$ and $\mathbb{P}_{<q}\,\varphi$. For a finite $\sigma$-structure $A$ identified with its ${\mathbf{\Gamma}}$-valued Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,A\right>_{\mathrm{\Gamma}}$,

[TABLE]

That is, $\mathbb{P}_{\geq q}\,\varphi$ is true in $A$ if a random assignment of the variables $v_{1},\dots,v_{n}$ in $A$ satisfies $\varphi$ with probability at least $q$. Similarly for $\mathbb{P}_{<q}\,\varphi$. If we regard $\mathbb{P}_{\geq q}\,$ and $\mathbb{P}_{<q}\,$ as probabilistic quantifiers that bind all free variables of a given formula, the Stone pairing $\left<\mkern 1.5mu\text{-}\mkern 1.5mu,\mkern 1.5mu\text{-}\mkern 1.5mu\right>_{\mathrm{\Gamma}}\colon\mathrm{Fin}\to\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ can be seen as the embedding of finite structures into the space of types for the logic $P\mkern-1.0mu\mathcal{L}_{\mathrm{FO}(\sigma)}$.

Conclusion

Types are points of the dual space of a logic (viewed as a Boolean algebra). In classical first-order logic, [math]-types are just the models modulo elementary equivalence. But when there are not ‘enough’ models, as in finite model theory, the spaces of types provide completions of the sets of models.

In [5], it was shown that for logic on words and various quantifiers we have that, given a Boolean algebra of formulas with a free variable, the space of types of the Boolean algebra generated by the formulas obtained by quantification is given by a measure space construction. Here we have shown that a suitable enrichment of first-order logic gives rise to a space of measures $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ closely related to the space $\operatorname{\mathcal{M}_{I}}(\mathrm{FO}(\sigma))$ used in the theory of structural limits. Indeed Theorem 5.1 tells us that the ensuing Stone pairings interdetermine each other. Further, the Stone pairing for $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ is just the embedding of the finite models in the completion/compactification provided by the space of types of the enriched logic.

These results identify the logical gist of the theory of structural limits, and provide a new and interesting connection between logic on words and the theory of structural limits in finite model theory. But we also expect that it may prove a useful tool in its own right. Thus, for structural limits, it is an open problem to characterise the closure of the image of the $[0,1]$-valued Stone pairing [15]. Reasoning instead in the ${\mathbf{\Gamma}}$-valued setting, native to logic and where we can use duality, one would expect that this is the subspace $\operatorname{\mathcal{M}_{\Gamma}}({\rm Th}(\mathrm{Fin}))$ of $\operatorname{\mathcal{M}_{\Gamma}}(\mathrm{FO}(\sigma))$ given by the quotient $\mathrm{FO}(\sigma)\twoheadrightarrow{\rm Th}(\mathrm{Fin})$ onto the theory of pseudofinite structures. The purpose of such a characterisation would be to understand the points of the closure as “generalised models”. Another subject that we would like to investigate is that of zero-one laws. The zero-one law for first-order logic states that the sequence of measures for which the $n$th measure, on a sentence $\psi$, yields the proportion of $n$-element structures satisfying $\psi$, converges to a $\{0,1\}$-valued measure. Over ${\mathbf{\Gamma}}$ this will no longer be true as $1$ is split into its ‘limiting’ and ‘achieved’ personae. Yet, we expect the above sequence to converge also in this setting and by Theorem 5.1, it will converge to a $\{0^{\circ},1^{-},1^{\circ}\}$-valued measure. Understanding this more fine-grained measure may yield useful information about the zero-one law.

Further, it would be interesting to investigate whether the limits for schema mappings introduced by Kolaitis et al. [13] may be seen also as a type-theoretic construction. Finally, we would want to explore the connections with other semantically inspired approaches to finite model theory, such as those recently put forward by Abramsky, Dawar et al. [2, 3].