352024

# Liveness Properties in Geometric Logic for Domain-Theoretic Streams

Colin Riba  ENS Lyon, Université de Lyon, LIP111UMR 5668 CNRS ENS Lyon UCBL
INRIA Solal Stern  ENS Lyon, Université de Lyon, LIP111UMR 5668 CNRS ENS Lyon
UCBL INRIA

###### Abstract

We devise a version of Linear Temporal Logic ($\mathsf{LTL}$) on a
denotational domain of streams. We investigate this logic in terms of domain
theory, (point-free) topology and geometric logic. This yields the first steps
toward an extension of the “Domain Theory in Logical Form” paradigm to
temporal liveness properties.

We show that the negation-free formulae of $\mathsf{LTL}$ induce sober
subspaces of streams, but that this is in general not the case in presence of
negation. We propose a direct, inductive, translation of negation-free
$\mathsf{LTL}$ to geometric logic. This translation reflects the
approximations used to compute the usual fixpoint representations of
$\mathsf{LTL}$ modalities.

As a motivating example, we handle a natural input-output specification for
the usual $\mathsf{filter}$ function on streams.

##  1 Introduction

We are interested in input-output properties of higher-order programs that
handle infinite data, such as streams or non-wellfounded trees. Consider for
instance the usual $\mathsf{filter}$ function

$\begin{array}[]{r c
l}\mathsf{filter}&:&(A\to\mathsf{Bool})\leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \mathsf{Str}A\leavevmode\nobreak\
\longrightarrow\leavevmode\nobreak\ \mathsf{Str}A\\\ \mathsf{filter}\ p\
(a\mathrel{::}x)&=&\mathsf{if}\leavevmode\nobreak\ (p\ a)\leavevmode\nobreak\
\mathsf{then}\leavevmode\nobreak\ a\mathrel{::}(\mathsf{filter}\ p\
x)\leavevmode\nobreak\ \mathsf{else}\leavevmode\nobreak\ (\mathsf{filter}\ p\
x)\end{array}$

where $\mathsf{Str}A$ stands for the type of streams on $A$. Assume
$p:A\to\mathsf{Bool}$ is a total function that tests for a property $P$. If
$x$ is a stream on $A$, then $(\mathsf{filter}\ p\ x)$ retains those elements
of $x$ which satisfy $P$. The stream produced by $(\mathsf{filter}\ p\ x)$ is
thus only partially defined, unless $x$ has infinitely many elements
satisfying $P$.

Logics like $\mathsf{LTL}$, $\mathsf{CTL}$ or the modal $\mu$-calculus are
widely used to formulate, on infinite objects, safety and liveness properties
(see e.g. [HR07, BS07]). Safety properties state that some “bad” event will
not occur, while liveness properties specify that “something good” will happen
(see e.g. [BK08]). One typically uses temporal modalities like $\square$
(_always_) or $\diamondsuit$ (_eventually_) to write properties of streams and
specifications of programs over such data.

A possible specification for $\mathsf{filter}$ asserts that $(\mathsf{filter}\
p\ x)$ is a totally defined stream whenever $x$ is a totally defined stream
with infinitely many elements satisfying $P$. We express this with the
temporal modalities $\square$ and $\diamondsuit$. Let $A$ be finite, and
assume given, for each $a$ of type $A$, a formula $\Phi_{a}$ which holds on
$b:A$ exactly when $b$ equals $a$.222In the setting of [JR21], we would assume
$A=\sum_{i=1}^{n}\mathbf{1}$, with $\Phi_{i}$ representing the image of the
$i$th injection. Then $\square\bigvee_{a}\Phi_{a}$ selects those streams on
$A$ which are totally defined. The formula $\square\diamondsuit P$ expresses
that a stream has infinitely many elements satisfying $P$. We can thus state
that for all streams $x:\mathsf{Str}A$,

$\begin{array}[]{c}\text{$x$ satisfies $\square\bigvee_{a}\Phi_{a}$ and
$\square\diamondsuit P$}\quad\Longrightarrow\quad\text{$(\mathsf{filter}\ p\
x)$ satisfies $\square\bigvee_{a}\Phi_{a}$}\end{array}$ (1)

The question we address in this paper is the following. Having in mind that a
stream (as opposed to e.g. an integer) is inherently an infinite object, what
do we mean exactly by “the stream $x$ satisfies $\square\diamondsuit P$”? In
our view, the above specification for $\mathsf{filter}$ should hold for any
stream whatsoever, and not only for those definable with a given programming
language.

This leads us to investigate temporal properties on infinite datatypes at the
level of denotational semantics. Logics on top of domains are known since
quite a long time. Our reference is the paradigm of “Domain Theory in Logical
Form” (DTLF) [Abr91] (see also [Zha91]), which allows one to systematically
generate a logic from a domain representing a type. These logics are actually
obtained by Stone duality, which is at the core of a rich interplay between
domain theory, logic and (point-free) topology. This area is presented under
various perspectives in a number of sources. We refer to [Abr91, AC98] and
(e.g.) [Joh82, Vic89, Vic07, GL13, GvG23]. Some key ideas are put at work in
[CZ00].

However, logics on domains given by Stone duality are usually restricted to
safety properties. To our knowledge, there is no systematic investigation of
liveness properties, such as the ones used in the specification for
$\mathsf{filter}$ above.

This paper reports on preliminary works, mostly based on an internship of the
second author during summer 2023. We devise a version of the logic
$\mathsf{LTL}$ on a domain of streams $\llbracket\mathsf{Str}A\rrbracket$
determined by the recursive type equation $\mathsf{Str}A\cong
A\times\mathsf{Str}A$. Each formula $\Phi$ of $\mathsf{LTL}$ yields a subset
$\llbracket\Phi\rrbracket\subseteq\llbracket\mathsf{Str}A\rrbracket$. We
investigate such $\mathsf{LTL}$-definable subsets in terms of domain theory,
of (point-free) topology and of a logic called geometric logic.

Our first step is to view domains as topological spaces, so as to benefit from
the rich notion of subspace. For instance, (with $A$ finite) the set of
$\omega$-words $A^{\omega}=\llbracket\square\bigvee_{a}\Phi_{a}\rrbracket$
turns out to be a discrete sub-poset of $\llbracket\mathsf{Str}A\rrbracket$.
But as a subspace of $\llbracket\mathsf{Str}A\rrbracket$, it becomes equipped
with its usual product topology (in the sense of e.g. [PP04]). We observe that
$\mathsf{LTL}$ formulae without negation induce subspaces of
$\llbracket\mathsf{Str}A\rrbracket$ which are sober, but that this may fail in
presence of negation. The notion of sobriety originates from point-free
topology, and has become quite important for the general (point-set) topology
of domains (see e.g. [GL13]).

We then turn to geometric logic. The idea is roughly the following. DTLF rests
on the fact that finite approximations in a domain can be represented in a
propositional logic generated from the topology of the domain. But this is too
weak to handle infinitary properties such as those definable with the
modalities $\square$ and $\diamondsuit$. On the other hand, the sobriety of
$\llbracket\Phi\rrbracket$ means that we can reason using an abstract notion
of approximation induced by the subspace topology. Geometric logic is an
infinitary propositional logic which allows for concrete representations of
topologies. We provide a direct, inductive, translation of negation-free
$\mathsf{LTL}$ to a geometric logic based on the domain
$\llbracket\mathsf{Str}A\rrbracket$. This translation reflects the
approximations used to compute the usual fixpoint representations of
$\square,\diamondsuit$. This shows that for the negation-free fragment, the
semantics of $\mathsf{LTL}$ can be concretely represented by approximations
which live in a natural extension of DTLF for the domain
$\llbracket\mathsf{Str}A\rrbracket$.

We also check that our translation of negation-free $\mathsf{LTL}$ indeed
conveys the good approximations to prove that the denotation of
$\mathsf{filter}$ meets the specification (1) above.

Let us finally mention the scientific context of this work. It is undecidable
whether a given higher-order program satisfies a given input-output temporal
property written with formulae of the modal $\mu$-calculus [KTU10]. A previous
work with the first author provided a refinement type system for proving such
properties [JR21]. This type system handles the alternation-free modal
$\mu$-calculus on (finitary) polynomial types, which includes $\mathsf{LTL}$.
But it is based on guarded recursion and does not allow for non-productive
functions such as $\mathsf{filter}$. We ultimately target a similar refinement
type systems for a language based on $\mathrm{FPC}$ (which extends Plotkin’s
seminal $\mathrm{PCF}$ [Plo77] with recursive types, see e.g. [Pie02]). We
think that the present work is a significant step in this direction. On the
one hand, DTLF allows for reasoning on denotations using (finitary) type
systems [Abr91]. On the other hand, it has been advocated in [KT14] that a
form of oracle is needed to handle liveness properties in type systems. And
indeed, [JR21] incorporates such oracles in a notion of “iteration term”,
which in fact makes the system infinitary.333Actually, as well as e.g.
[NUKT18, SU23], despite a fundamentally different approach (see §7). We think
that our representation of negation-free $\mathsf{LTL}$ in geometric logic can
lead to an infinitary type system which extends [Abr91], and whose infinitary
part can be simulated using iteration terms.

##### Organization of the paper.

The preliminary §2 introduces background on domain theory, and the logic
$\mathsf{LTL}$ on $\llbracket\mathsf{Str}A\rrbracket$. The (point-free)
topological approach is presented in §3, and §4 is devoted to geometric logic.
fullSection A deals with a deduction system for geometric logic, in connection
with the notion of spatiality. The specification of $\mathsf{filter}$ is
discussed in §6. We conclude in §7. shortProofs are available in the full
version [rs23full] attached to the submission, which also contains additional
material on deduction for geometric logic.longProofs are available in the
Appendices, which also contain additional material on deduction for geometric
logic.fullProofs are available in the Appendices.

draftTODO FOR SUBMISSION:

  * •

Enable draft option (line numbers).

##  2 A Linear Temporal Logic on a Domain of Streams

Let $A$ be a set. A (finite) _word_ on $A$ is an element of $A^{*}$.
$A^{\omega}$ is the set of _$\omega$ -words_ on $A$, i.e. the set of all
functions $\sigma\colon\mathbb{N}\to A$. We write $u\subseteq v$ when $u\in
A^{*}$ is a prefix of $v\in A^{*}\cup A^{\omega}$. The concatenation of $u\in
A^{*}$ with $v\in A^{*}\cup A^{\omega}$ is denoted $u\cdot v$ or $uv$. Given
$\sigma\in A^{\omega}$ and $k\in\mathbb{N}$, we let
$\sigma\mathord{\upharpoonright}k\in A^{\omega}$ be the $\omega$-word with
$(\sigma\mathord{\upharpoonright}k)(n)=\sigma(k+n)$ for all $n\in\mathbb{N}$.
For instance, $\sigma\mathord{\upharpoonright}0$ is $\sigma$, while
$\sigma\mathord{\upharpoonright}1=\sigma(1)\cdot\sigma(2)\cdots\sigma(n+1)\cdots$
is $\sigma$ deprived from its first letter.

###  2.1 Domains

The basic idea of domain theory is to represent a type by partial order
$(X,\leq_{X})$ thought about as an “information order”. The intuition is that
$x\leq_{X}y$ means that $y$ has “more information” than $x$, or that $x$ is
“less defined” than $y$. Domains are often required to have a least element
(representing plain divergence), and are always asked to be stable under
certain supremums (so that infinite objects can be thought about as limits of
their finite approximations). Our presentation mostly follows [AC98, §1]. See
also [Abr91, GL13].

##### Dcpos and Cpos.

Let $(X,\leq)$ be a partial order (or _poset_). An _upper bound_ of a subset
$S\subseteq X$ is an element $x\in X$ such that $(\forall s\in S)(s\leq x)$. A
_least upper bound_ (or _supremum_ , _sup_) of $S$ is an upper bound $\ell$ of
$S$ such that $\ell\leq x$ for every upper bound $x$ of $S$. The sup of $S$ is
unique whenever it exists, and is usually denoted $\bigvee S$. The notion of
_greatest lower bound_ (or _infimum_ , _inf_) is defined dually. A subset
$D\subseteq X$ is _directed_ if $D$ is non-empty and for every $x,y\in D$,
there is some $z\in D$ such that $x\leq z$ and $y\leq z$.

We say that $(X,\leq)$ is a _dcpo_ if every directed $D\subseteq X$ has a sup
$\bigvee D\in X$. A _cpo_ is a dcpo with a least element (usually denoted
$\bot$). Note that each set $A$ is a dcpo for the discrete order (in which $x$
is comparable with $y$ if, and only if, $x=y$). However, such a dcpo $A$ is
not a cpo unless $A$ is a singleton.

[Flat Domains] Given a set $A$, the _flat domain_ $\llbracket A\rrbracket$ is
the disjoint union $\\{\bot\\}+A$ equipped with the partial order
$\leq_{\llbracket A\rrbracket}$, where $x\leq_{\llbracket A\rrbracket}y$ iff
$x=y$ or ($x=\bot$ and $y\in A$).

It is easy to see that $(\llbracket A\rrbracket,\leq_{\llbracket
A\rrbracket})$ is a cpo whose directed subsets have at most one element from
$A$. For instance, the domain $\llbracket\mathsf{Bool}\rrbracket$ can be
represented by the following Hasse diagram.

${\mathsf{tt}}$${\mathsf{ff}}$${\bot}$

##### Scott-Continuous Functions.

Let $X=(X,\leq_{X})$ and $Y=(Y,\leq_{Y})$ be dcpos. A function $f\colon X\to
Y$ is _Scott-continuous_ if $f$ is monotone ($x\leq_{X}x^{\prime}$ implies
$f(x)\leq_{Y}f(x^{\prime})$) and if moreover $f$ preserves directed sups, in
the sense that for each directed $D\subseteq X$, we have

$\begin{array}[]{l l l}f(\bigvee D)&=&\bigvee\left\\{f(d)\mid d\in
D\right\\}\end{array}$

We write $\mathbf{CPO}$ (resp. $\mathbf{DCPO}$) for the category with cpos
(resp. dcpos) as objects and with Scott-continuous functions as morphisms. We
say that $f\in\mathbf{CPO}[X,Y]$ is strict if $f(\bot_{X})=\bot_{Y}$. A non-
strict monotone map between flat domains is necessarily constant.

Given dcpos $X=(X,\leq_{X})$ and $Y=(Y,\leq_{Y})$, the set of Scott-continuous
functions $\mathbf{DCPO}[X,Y]$ is itself a dcpo w.r.t. the _pointwise order_

$\begin{array}[]{l l l}f\leq_{\mathbf{DCPO}[X,Y]}g&\text{iff}&\forall x\in
X,\leavevmode\nobreak\ f(x)\leq_{Y}g(x)\end{array}$

If $Y$ is actually a cpo, then $\mathbf{DCPO}[X,Y]$ is a cpo whose least
element is the constant function $x\in X\mapsto\bot_{Y}\in Y$, where
$\bot_{Y}$ is the least element of $Y$.

[Streams] Let $A$ be a set. We let $\llbracket\mathsf{Str}A\rrbracket$, the
cpo of _streams over $A$_, be $\mathbf{DCPO}[\mathbb{N},\llbracket
A\rrbracket]$ with $\mathbb{N}$ discrete. We unfold this important example.
Since $\mathbb{N}$ is discrete, $\llbracket\mathsf{Str}A\rrbracket$ actually
consists of the set $\llbracket A\rrbracket^{\omega}$ equipped with the
partial order

$\begin{array}[]{l !{\quad\text{iff}\quad}
l}x\leq_{\llbracket\mathsf{Str}A\rrbracket}y&\forall
n\in\mathbb{N},\leavevmode\nobreak\ x(n)\leq_{\llbracket
A\rrbracket}y(n)\end{array}$

A set $D\subseteq\llbracket\mathsf{Str}A\rrbracket$ is directed if, and only
if, $D$ is non-empty and each $D(n)=\left\\{x(n)\mid x\in D\right\\}$ has at
most one element from $A$. Then $\bigvee
D\in\llbracket\mathsf{Str}A\rrbracket$ takes $n\in\mathbb{N}$ to the largest
element of $D(n)$. The least element of $\llbracket\mathsf{Str}A\rrbracket$ is
the stream $\bot^{\omega}$ of constant value $\bot\in\llbracket A\rrbracket$.

Note that $\llbracket\mathsf{Str}A\rrbracket$ has “partially defined”
elements. Besides the least element $\bot^{\omega}$, we have e.g. the stream
$u\cdot\bot^{\omega}$ (which agrees with $u\in A^{*}$ and then is $\bot$ at
all sufficiently large positions) or $(a\cdot\bot)^{\omega}$ (which is $a$ at
all even positions, and is $\bot$ everywhere else). The $\omega$-words on $A$
are precisely those streams $x\in\llbracket\mathsf{Str}A\rrbracket$ which
never take the value $\bot$. Such streams are called _total_. Note that if $x$
is total, then

$\begin{array}[]{*{3}{l}}x&=&\bigvee\left\\{u\cdot\bot^{\omega}\mid\text{$u\in
A^{*}$ and $u\subseteq x$}\right\\}\end{array}$

######  Remark 2.1.

The cpo $\llbracket\mathsf{Str}A\rrbracket$ is the usual solution in the
category $\mathbf{CPO}$ of the _domain equation_

$\begin{array}[]{l l l}X&\cong&\llbracket A\rrbracket\times X\end{array}$

(where $\llbracket A\rrbracket\times X$ is equipped with the pointwise order),
see e.g. [AC98, Theorem 7.1.10 and Proposition 7.1.13]. In particular, the
constructor $(-\mathrel{::}-)$ of the type $\mathsf{Str}A$ is interpreted as
the isomorphism taking $(a,x)\in\llbracket
A\rrbracket\times\llbracket\mathsf{Str}A\rrbracket$ to $a\cdot
x\in\llbracket\mathsf{Str}A\rrbracket$, with inverse
$x\mapsto(x(0),x\mathord{\upharpoonright}1)$. Note that
$\llbracket\mathsf{Str}A\rrbracket$ differs from the usual _Kahn domain_
$A^{*}\cup A^{\omega}$ (see e.g. [Vic89, Definition 3.7.5 and Example 5.4.4]
or [DST19, §7.4], see also [VVK05]).

######  Remark 2.2.

Each $f\colon X\to_{\mathbf{CPO}}X$ has a _least fixpoint_
$\mathsf{Y}(f)\coloneqq\bigvee_{n\in\mathbb{N}}f^{n}(\bot)\in X$. In
particular, $\mathsf{filter}$ is interpreted as the Scott-continuous function
$\llbracket\mathsf{filter}\rrbracket$ taking $p\colon\llbracket
A\rrbracket\to_{\mathbf{CPO}}\llbracket\mathsf{Bool}\rrbracket$ to the least
fixpoint of the following function $f_{p}$, where $X$ is the cpo
$\llbracket\mathsf{Str}A\rrbracket\to_{\mathbf{CPO}}\llbracket\mathsf{Str}A\rrbracket$.

$\begin{array}[]{*{7}{l}}f_{p}&\coloneqq&\lambda g.\lambda
x.\leavevmode\nobreak\ \mathsf{if}\leavevmode\nobreak\
p(x(0))\leavevmode\nobreak\ \mathsf{then}\leavevmode\nobreak\ x(0)\cdot
g(x\mathord{\upharpoonright}1)\leavevmode\nobreak\
\mathsf{else}\leavevmode\nobreak\
g(x\mathord{\upharpoonright}1)&:&X&\longrightarrow_{\mathbf{CPO}}&X\end{array}$

##### Algebraicity.

Among the many good properties of $\llbracket\mathsf{Str}A\rrbracket$,
algebraicity is the crucial one in this work. This property is not used right
away, but will be the main assumption of various statements later on.

Let $(X,\leq)$ be a dcpo. We say that $x\in X$ is _finite_ 444Finite elements
are called _compact_ in [AC98]. if for every directed $D\subseteq X$ such that
$x\leq\bigvee D$, there is some $d\in D$ such that $x\leq d$. We say that $X$
is _algebraic_ if for every $x\in X$, the set $\\{d\in X\mid\text{$d$ finite
and $d\leq x$}\\}$ is directed and has sup $x$. Each discrete or flat dcpo is
algebraic.

[Streams] The cpo $\llbracket\mathsf{Str}A\rrbracket$ is algebraic, and its
finite elements admit a particularly simple description. The _support_ of
$x\in\llbracket\mathsf{Str}A\rrbracket$ is the set $\mathrm{supp}(x)$ of
“defined letters” of $x$:

$\begin{array}[]{l l l}\mathrm{supp}(x)&\coloneqq&\left\\{n\in\mathbb{N}\mid
x(n)\neq\bot\right\\}\end{array}$

We say that a stream $x$ has finite support when $\mathrm{supp}(x)$ is a
finite set. For instance, given a finite word $u\in A^{*}$ and
$n\in\mathbb{N}$, the stream $\bot^{n}\cdot u\cdot\bot^{\omega}$ has finite
support. On the other hand, total streams, as well as e.g.
$(a\cdot\bot)^{\omega}$, do not have finite support.

For each $x\in\llbracket\mathsf{Str}A\rrbracket$, the set
$\left\\{d\mid\text{$d$ of finite support and
$\leq_{\llbracket\mathsf{Str}A\rrbracket}x$}\right\\}$ is directed and has sup
$x$. Moreover, the finite elements of $\llbracket\mathsf{Str}A\rrbracket$ are
exactly those of finite support.

###  2.2 Linear Temporal Logic ($\mathsf{LTL}$)

##### Syntax and Semantics.

Let $A$ be a set. The formulae of $\mathsf{LTL}=\mathsf{LTL}(A)$ are given by

$\begin{array}[]{l l l}\Phi,\Psi&\Coloneqq&a\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\mathsf{True}\leavevmode\nobreak\ \leavevmode\nobreak\ |\leavevmode\nobreak\
\leavevmode\nobreak\ \mathsf{False}\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \Phi\land\Psi\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\Phi\lor\Psi\leavevmode\nobreak\ \leavevmode\nobreak\ |\leavevmode\nobreak\
\leavevmode\nobreak\ \lnot\Phi\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\ \bigcirc\Phi\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\Phi\mathrel{\mathsf{U}}\Psi\leavevmode\nobreak\ \leavevmode\nobreak\
|\leavevmode\nobreak\ \leavevmode\nobreak\
\Phi\mathrel{\mathsf{W}}\Psi\end{array}$

where $a\in A$. Hence, besides pure propositional logic, $\mathsf{LTL}(A)$ has
_atomic formulae_ $a\in A$, and _modalities_ $\bigcirc\Phi$ (read “next
$\Phi$”), $\Phi\mathrel{\mathsf{U}}\Psi$ (read “$\Phi$ until $\Psi$”) and
$\Phi\mathrel{\mathsf{W}}\Psi$ (read “$\Phi$ weak until $\Psi$” or “$\Phi$
unless $\Psi$”).

The $\mathsf{LTL}$ formulae over $A$ are usually interpreted on $\omega$-words
over $A$, see e.g. [BK08, §5]. The interpretation of modalities actually
implicitly relies on the bijection $A^{\omega}\cong A\times A^{\omega}$. We
similarly rely on the isomorphism
$\llbracket\mathsf{Str}A\rrbracket\cong_{\mathbf{CPO}}\llbracket
A\rrbracket\times\llbracket\mathsf{Str}A\rrbracket$ for interpreting
$\mathsf{LTL}(A)$ formulae in $\llbracket\mathsf{Str}A\rrbracket$. We define
$\llbracket\Phi\rrbracket\subseteq\llbracket\mathsf{Str}A\rrbracket$ by
induction on $\Phi$. The propositional connectives of $\mathsf{LTL}$ are
interpreted using the usual Boolean algebra structure of the powerset
$\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$. For $a\in A$, we let
$\llbracket a\rrbracket\coloneqq\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid
x(0)=a\\}$. The modalities are interpreted as follows.

$\begin{array}[]{r c
l}\llbracket\bigcirc\Phi\rrbracket&\coloneqq&\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid
x\mathord{\upharpoonright}1\in\llbracket\Phi\rrbracket\right\\}\\\
\llbracket\Phi\mathrel{\mathsf{U}}\Psi\rrbracket&\coloneqq&\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid\exists
i\in\mathbb{N},\leavevmode\nobreak\
x\mathord{\upharpoonright}0,\dots,x\mathord{\upharpoonright}(i-1)\in\llbracket\Phi\rrbracket\leavevmode\nobreak\
\text{and}\leavevmode\nobreak\
x\mathord{\upharpoonright}i\in\llbracket\Psi\rrbracket\right\\}\\\
\llbracket\Phi\mathrel{\mathsf{W}}\Psi\rrbracket&\coloneqq&\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid\forall
i\in\mathbb{N},\leavevmode\nobreak\
x\mathord{\upharpoonright}i\in\llbracket\Phi\rrbracket\right\\}\cup\llbracket\Phi\mathrel{\mathsf{U}}\Psi\rrbracket\par\end{array}$

We say that $x\in\llbracket\mathsf{Str}A\rrbracket$ _satisfies_ a formula
$\Phi$ (notation $x\Vdash\Phi$) when $x\in\llbracket\Phi\rrbracket$. It is
often convenient to decompose $\llbracket\bigcirc\Phi\rrbracket$ as
$\llbracket\bigcirc\rrbracket(\llbracket\Phi\rrbracket)$, where
$\llbracket\bigcirc\rrbracket\colon\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)\to\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$
takes $S$ to $\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid
x\mathord{\upharpoonright}1\in S\right\\}$. The modalities
$\mathrel{\mathsf{U}}$ and $\mathrel{\mathsf{W}}$ may not be easy to grasp.
Given $\mathsf{LTL}$ formulae $\Phi$ and $\Psi$, we let

$\begin{array}[]{r !{\quad} r c l !{\quad} r !{=} l}\text{``eventually
$\Psi$''}&\diamondsuit\Psi&\coloneqq&\mathsf{True}\mathrel{\mathsf{U}}\Psi&\big{(}\llbracket\diamondsuit\Psi\rrbracket&\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid\exists
i\in\mathbb{N},\leavevmode\nobreak\
x\mathord{\upharpoonright}i\in\llbracket\Psi\rrbracket\right\\}\big{)}\\\
\text{``always
$\Phi$''}&\square\Phi&\coloneqq&\Phi\mathrel{\mathsf{W}}\mathsf{False}&\big{(}\llbracket\square\Phi\rrbracket&\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid\forall
i\in\mathbb{N},\leavevmode\nobreak\
x\mathord{\upharpoonright}i\in\llbracket\Phi\rrbracket\right\\}\big{)}\end{array}$

Consider a stream $x\in\llbracket\mathsf{Str}A\rrbracket$.

  1. (1)

We have $x\Vdash\bigcirc a$ if, and only if, $x(1)=a$. For instance, $\bot
a\bot^{\omega}\Vdash\bigcirc a$ but $a\bot^{\omega}\not\Vdash\bigcirc a$.

  2. (2)

We have $x\Vdash\diamondsuit a$ if, and only if, $x(i)=a$ for some
$i\in\mathbb{N}$. For instance $\bot^{n}a\bot^{\omega}\Vdash\diamondsuit a$
for every $n\in\mathbb{N}$. But $b^{\omega}\not\Vdash\diamondsuit a$ if $b\neq
a$.

  3. (3)

We have $x\Vdash\square a$ if, and only if, $x=a^{\omega}$. If $A$ is finite,
then $x$ is total iff $x\Vdash\square\bigvee_{a\in A}a$.

  4. (4)

We have $x\Vdash\square\diamondsuit a$ if, and only if, $x(i)=a$ for
infinitely many $i\in\mathbb{N}$. E.g. $(\bot
a)^{\omega}\Vdash\square\diamondsuit a$.

  5. (5)

We have $x\Vdash\diamondsuit\square a$ if, and only if, $x(i)=a$ for
“ultimately all $i\in\mathbb{N}$”. This means that for some $n\in\mathbb{N}$,
we have $x(i)=a$ for all $i\geq n$. For instance,
$\bot^{n}a^{\omega}\Vdash\diamondsuit\square a$ for all $n\in\mathbb{N}$. But
$(\bot a)^{\omega}\not\Vdash\diamondsuit\square a$.

Say that $\Phi$ and $\Psi$ are (logically) _equivalent_ , notation
$\Phi\equiv\Psi$, if $\llbracket\Phi\rrbracket=\llbracket\Psi\rrbracket$.
$\mathsf{LTL}$ has many redundancies w.r.t. logical equivalence. Besides the
usual De Morgan laws, we have e.g.

$\begin{array}[]{l !{\equiv} l !{\qquad} l !{\equiv} l !{\qquad} l !{\equiv}
l}\lnot\square\Phi&\diamondsuit\lnot\Phi\par&\lnot\diamondsuit\Phi&\square\lnot\Phi\par&\Phi\mathrel{\mathsf{W}}\Psi&(\Phi\mathrel{\mathsf{U}}\Psi)\lor\square\Phi\end{array}$

######  Remark 2.3.

The modalities $\mathrel{\mathsf{U}}$ and $\mathrel{\mathsf{W}}$ are also “De
Morgan” duals, in the following sense. Given $\Phi$ and $\Psi$, it is well-
known that $\llbracket\Phi\mathrel{\mathsf{U}}\Psi\rrbracket$ and
$\llbracket\Phi\mathrel{\mathsf{W}}\Psi\rrbracket$ are respectively the least
and the greatest fixpoint of the (monotone) map on
$\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$ taking $S$ to
$\llbracket\Psi\rrbracket\cup\left(\llbracket\Phi\rrbracket\cap\llbracket\bigcirc\rrbracket(S)\right)$.
See e.g. [BK08, Lemmas 5.18 and 5.19]. But
$\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$ is a complete atomic Boolean
algebra, and given a monotone endo-function $f$ on such a Boolean algebra, the
least and greatest fixpoints of $f$ are related by
$\mathord{\mathrm{lfp}}(f)=\lnot\mathord{\mathrm{gfp}}(b\mapsto\lnot f(\lnot
b))$ and $\mathord{\mathrm{gfp}}(f)=\lnot\mathord{\mathrm{lfp}}(b\mapsto\lnot
f(\lnot b))$.

##### Negation-Free $\mathsf{LTL}$.

Our main positive results only hold for the negation-free fragment of
$\mathsf{LTL}$. An $\mathsf{LTL}$ formula is _negation-free_ (_n.-f._) if it
contains no negation ($\lnot(-)$). Hence, the negation-free formulae of
$\mathsf{LTL}$ are generated by the above grammar for $\mathsf{LTL}$, but
without the production $\lnot\Phi$.

All formulae of Example 2.2 are negation-free. Moreover, the negation-free
fragment is closed under $\square(-)$ and $\diamondsuit(-)$.

Assume $A$ is finite. For any $S\subseteq A$, there is a negation-free formula
$\Psi_{S}$ such that $x\Vdash\Psi_{S}$ iff $x(0)\in S$. It follows that for
any Scott-continuous $p\colon\llbracket
A\rrbracket\to\llbracket\mathsf{Bool}\rrbracket$, there is a negation-free
formula $\Psi_{p}$ such that $x\Vdash\square\diamondsuit\Psi_{p}$ if, and only
if, $x$ has infinitely many elements satisfying $p$.

Most redundancies of $\mathsf{LTL}$ mentioned above disappear in the negation-
free fragment. This is why we have chosen this set of connectives from the
start. In negation-free $\mathsf{LTL}(A)$, all connectives have a De Morgan
dual. But negated atomic formulae ($\lnot a$ for $a\in A$) are not available.
Hence, in contrast with positive normal forms (see e.g. [BK08, Definition
5.20]), negation is _not_ definable in negation-free $\mathsf{LTL}$. This
positive character is reflected in the following fundamental fact, proved by
induction on formulae.

If $\Phi$ is n.-f. then $\llbracket\Phi\rrbracket$ is upward-closed (if
$x\in\llbracket\Phi\rrbracket$ and
$x\leq_{\llbracket\mathsf{Str}A\rrbracket}y$ then
$y\in\llbracket\Phi\rrbracket$).

Let $\Phi$ be negation-free. Then $\llbracket\Phi\rrbracket$ is closed in
$\llbracket\mathsf{Str}A\rrbracket$ under directed sups. Moreover, the
inclusion
$\llbracket\Phi\rrbracket\hookrightarrow\llbracket\mathsf{Str}A\rrbracket$ is
a Scott-continuous order-embedding.

Hence, $\llbracket\Phi\rrbracket$ is a sub-dcpo of
$\llbracket\mathsf{Str}A\rrbracket$ when $\Phi$ is n.-f. But this may not give
much information on $\llbracket\Phi\rrbracket$. For instance,
$A^{\omega}=\llbracket\square\bigvee_{a\in A}a\rrbracket$ (Example 2.2.(3),
$A$ finite) is a discrete dcpo. Building on Lemma 2.2, we are going to exhibit
much more structure on such inclusions
$\llbracket\Phi\rrbracket\hookrightarrow\llbracket\mathsf{Str}A\rrbracket$.
But before, we note that Lemma 2.2 and Corollary 2.2 may fail in presence of
negation.

Consider the formula $\lnot\square a$. Note that
$a^{\omega}\not\Vdash\lnot\square a$. But for every finite
$d\leq_{\llbracket\mathsf{Str}A\rrbracket}a^{\omega}$, we have
$d\Vdash\lnot\square a$. Hence $\llbracket\lnot\square a\rrbracket$ is not
upward-closed. Moreover, $\\{\text{$d$ finite}\mid
d\leq_{\llbracket\mathsf{Str}A\rrbracket}a^{\omega}\\}$ is a directed subset
of $\llbracket\lnot\square a\rrbracket$ which has no sup in
$\llbracket\lnot\square a\rrbracket$. Hence $\llbracket\lnot\square
a\rrbracket$ is not a dcpo w.r.t. the restriction of
$\leq_{\llbracket\mathsf{Str}A\rrbracket}$.

##  3 The Topological Approach

We shall now look at inclusions
$\llbracket\Phi\rrbracket\hookrightarrow\llbracket\mathsf{Str}A\rrbracket$
from a topological perspective. We recall in §3.1 that the categories
$\mathbf{(D)CPO}$ can be embedded in the category $\mathbf{Top}$ of
topological spaces and continuous functions. The highlight is that
$\mathbf{Top}$ has a much richer notion of substructures (called subspaces)
than $\mathbf{(D)CPO}$.

Actually, when looking at (d)cpos as topological spaces, the notion of
sobriety from point-free (or “element-free”) topology comes to the front.
Ample mathematical justifications for the importance of sober spaces in domain
theory are gathered in [GL13]. We shall content ourselves with more informal
motivations in §3.2. In §3.3, we abstractly prove that
$\llbracket\Phi\rrbracket$ induces a sober subspace of
$\llbracket\mathsf{Str}A\rrbracket$ when $\Phi$ is negation-free.
full,longThis will be refined to concrete representations in §4 and §A, using
geometric logic.shortThis will be refined to concrete representations in §4
(and also [rs23full, §A]), using geometric logic.

###  3.1 Topological Spaces

A _topological space_ is a pair $(X,\Omega(X))$ of a set $X$ and a collection
$\Omega=\Omega(X)$ of subsets of $X$, called _open sets_. $\Omega$ is called a
_topology_ on $X$, and is asked to be stable under arbitrary unions and under
finite intersections. In particular, $\emptyset$ and $X$ are open in $X$
(respectively as the empty union and the empty intersection).

A set $C\subseteq X$ is _closed_ if its complement $X\setminus C$ is open.
Closed sets are stable under finite unions and arbitrary intersections. Hence,
any $S\subseteq X$ is contained in a least closed set $\overline{S}\subseteq
X$. Each space $(X,\Omega)$ is equipped with a _specialization_ (pre)order
$\leq_{\Omega}$ on $X$, defined as

$\begin{array}[]{l l l}x\leq_{\Omega}y&\text{iff}&(\forall
U\in\Omega)\left(x\in U\leavevmode\nobreak\
\Longrightarrow\leavevmode\nobreak\ y\in U\right)\end{array}$

Given $x\in X$, we have
$\overline{\\{x\\}}=\mathord{\downarrow}x\coloneqq\\{y\in X\mid
y\leq_{\Omega}x\\}$ (see e.g. [GL13, Lemma 4.2.7]). A topology $\Omega$ is
_$T_{0}$_ when $\leq_{\Omega}$ is a partial order (see e.g. [GL13, Proposition
4.2.3]).

Given spaces $(X,\Omega(X))$ and $(Y,\Omega(Y))$, a function $f\colon X\to Y$
is _continuous_ when its inverse image
$f^{-1}\colon\mathcal{P}(Y)\to\mathcal{P}(X)$ restricts to a function
$\Omega(Y)\to\Omega(X)$, i.e. when $f^{-1}(V)\in\Omega(X)$ for all
$V\in\Omega(Y)$. We write $\mathbf{Top}$ for the category of topological
spaces and continuous functions. An _homeomorphism_ is an isomorphism in
$\mathbf{Top}$.

##### The Scott Topology.

The following is well-known. See e.g. [AC98, §1.2] or [GL13, §4].

Let $(X,\leq_{X})$ be a dcpo. A subset $U\subseteq X$ is _Scott-open_ if $U$
is upward-closed, and if moreover $U$ is inaccessible by directed sups, in the
sense that if $\bigvee D\in U$ with $D\subseteq X$ directed, then $D\cap
U\neq\emptyset$. This equips $X$ with a $T_{0}$ topology, called the _Scott
topology_ , whose specialization order coincides with $\leq_{X}$.

When $(X,\leq)$ is algebraic, the sets $\mathord{\uparrow}d\coloneqq\\{x\in
X\mid d\leq x\\}$ with $d$ finite form a sub-basis for the Scott topology. For
instance, the Scott-open subsets of $\llbracket\mathsf{Str}A\rrbracket$ are
arbitrary unions of sets of the form

$\begin{array}[]{l l
l}\mathord{\uparrow}d&=&\left\\{x\in\llbracket\mathsf{Str}A\rrbracket\mid\forall
i\in\mathrm{supp}(d),\leavevmode\nobreak\ x(i)=d(i)\right\\}\end{array}$

with $\mathrm{supp}(d)$ finite. In particular, given $x\in U$ with
$U\subseteq\llbracket\mathsf{Str}A\rrbracket$ Scott-open, there is a _finite_
set $\\{i_{1},\dots,i_{k}\\}\subseteq\mathbb{N}$ such that $\left\\{y\mid
y(i_{1})=x(i_{1}),\dots,y(i_{k})=x(i_{k})\right\\}\subseteq U$.

Beware that $\llbracket\Phi\rrbracket$ may not be an open nor a closed subset
of $\llbracket\mathsf{Str}A\rrbracket$, even when $\Phi$ is negation-free.
Consider for instance $A^{\omega}=\llbracket\square\bigvee_{a\in
A}a\rrbracket$ (with $A$ non-empty and finite), which contains $a^{\omega}$
but no finite $d\leq_{\llbracket\mathsf{Str}A\rrbracket}a^{\omega}$.

A function $f\colon X\to Y$ between dcpos is Scott-continuous precisely when
$f$ is continuous w.r.t. the Scott-topologies on $X$ and $Y$. It follows that
$\mathbf{DCPO}$ and $\mathbf{CPO}$ are full subcategories of $\mathbf{Top}$.
From now on, we shall mostly look at $\mathbf{(D)CPO}$ in this way. Unless
stated otherwise, dcpos will always be equipped with their Scott topology.

##### Subspaces.

Our motivation for moving from $\mathbf{(D)CPO}$ to $\mathbf{Top}$ is that
$\mathbf{Top}$ has a rich notion of subspace. We refer to [BBT20, §1.2]. Given
a space $(X,\Omega)$ and a subset $P\subseteq X$, the _subspace topology_ on
$P$ is

$\begin{array}[]{l l
l}\Omega\mathord{\upharpoonright}P&\coloneqq&\left\\{U\cap P\mid
U\in\Omega\right\\}\end{array}$

The subspace topology on $P$ makes the inclusion function $\iota\colon
P\hookrightarrow X$ continuous. It is the “best possible” topology on $P$ in
the following sense: given a space $(Y,\Omega(Y))$, a function $f\colon Y\to
P$ is continuous if, and only if, the composition $\iota\mathbin{\circ}f\colon
Y\to X$ is continuous.

${P}$${Y}$${X}$$\scriptstyle{\iota}$$\scriptstyle{f}$$\scriptstyle{\iota\mathbin{\circ}f}$

Generalizing Example 2.2.(3) and Lemma 2.2, $A^{\omega}$ is a discrete sub-
dcpo of $\llbracket\mathsf{Str}A\rrbracket$.

On the other hand, the subspace topology
$\Omega(\llbracket\mathsf{Str}A\rrbracket)\mathord{\upharpoonright}A^{\omega}$
is the usual _product topology_ on $A^{\omega}$ (see e.g. [PP04, §III] or
[Kec95]). The sets of the form $A^{\omega}\cap\mathord{\uparrow}d$ (with $d$
finite) form a sub-basis for the subspace topology. In fact, its opens are
unions of sets of the form $\\{\sigma\in
A^{\omega}\mid\sigma(i_{1})=a_{1},\dots,\sigma(i_{k})=a_{k}\\}$, where
$i_{1},\dots,i_{k}\in\mathbb{N}$ and $a_{1},\dots,a_{k}\in A$ with $k\geq 0$.

###  3.2 The Element-Free Setting

The topological setting comes with an intrinsic notion of approximation.

Consider for instance $\omega$-words $\sigma\in A^{\omega}$ (Example 3.1).
Similarly as with streams in Example 3.1, given an $\omega$-word $\sigma$ and
an open $U$, if $\sigma$ belongs to $U$, then this fact is witnessed by the
knowledge of a finite number of elements of $\sigma$.555By contrast, the
knowledge of the whole $\omega$-word $\sigma$ may be needed to testify that
$\sigma\notin U$. We view the opens $U$ such that $\sigma\in U$ as
approximations of $\sigma$.

Given a space $(X,\Omega)$, we are interested in describing the elements of
$X$ by their approximations, represented as suitable sets of opens
$\mathcal{F}\subseteq\Omega$. This is the realm of _element-free_ (or _point-
free_) _topology_. Its central objects, called _frames_ (or _locales_),
abstract away from the elements of spaces, and only retain the lattice
structure of open sets. Besides [GL13], we refer to [Joh82, Joh83, Vic89,
PP11, PP21].

##### Frames.

A _complete lattice_ is a poset having all sups and all infs. But recall (from
e.g. [DP02, Theorem 2.31]) that a poset has all sups if, and only if, it has
all infs. Hence, we can see complete lattices indifferently as posets with all
sups or as posets with all infs.

A _frame_ is a poset $L$ with all sups (and thus all infs), and which
satisfies the following _frame distributive law_ : for all $S\subseteq L$ and
all $a\in L$,

$\begin{array}[]{l l l}a\wedge\bigvee S&=&\bigvee\left\\{a\wedge s\mid s\in
S\right\\}\end{array}$

Not every complete lattice is a frame (consider e.g. a finite (and thus
complete) non-distributive lattice, see e.g. [DP02, Example 4.6(6)]). But
every $(\mathcal{P}(X),\subseteq)$ is a frame, and so is the two-elements
poset $\mathbf{2}\coloneqq\\{0\leq 1\\}$.

Given frames $L$ and $K$, a _frame morphism_ $f\colon L\to K$ is a function
which preserves all sups and all _finite_ infs. Note that frame morphisms are
automatically monotone. We write $\mathbf{Frm}$ for the category of frames and
frame morphisms.

Let $(X,\Omega(X))$ be a space. Then $\Omega(X)$ has all sups and they are
given by unions. Hence $\Omega(X)$ is a complete lattice. Beware that the inf
in $\Omega(X)$ of an arbitrary $S\subseteq\Omega(X)$ is in general not its
intersection $\bigcap S$, but the _interior_ of $\bigcap S$ (the largest open
set contained in $\bigcap S$). However, _finite_ infs in $\Omega(X)$ are given
by intersections, and $\Omega(X)$ is a frame.

Moreover, if $f\colon X\to Y$ is continuous, then its inverse image $f^{-1}$
restricts to a function $\Omega(Y)\to\Omega(X)$. This function is actually a
frame morphism $\Omega(f)\in\mathbf{Frm}[\Omega(Y),\Omega(X)]$. In other
words, the operation $(X,\Omega(X))\mapsto\Omega(X)$ extends to a functor
$\Omega$ from the category $\mathbf{Top}$ to $\mathbf{Frm}^{\mathrm{op}}$, the
opposite of $\mathbf{Frm}$. The category $\mathbf{Frm}^{\mathrm{op}}$ is the
category of _locales_.

##### The Space of Points.

We see a frame $L$ as a collection of formal approximations. Suitable subsets
of $L$ describe “converging” sets of formal approximations, and constitute the
elements of a space, the space of points of $L$. The idea is as follows. Given
a space $X$ and $x\in X$, let

$\begin{array}[]{l l l}\mathcal{F}_{x}&\coloneqq&\left\\{U\in\Omega(X)\mid
x\in U\right\\}\end{array}$

Note the following properties of $\mathcal{F}_{x}$ w.r.t. the frame structure
of $\Omega(X)$. First, $\mathcal{F}_{x}$ is stable under finite intersections
($x\in X$, and $x\in U\cap V$ iff $x\in U$ and $x\in V$). Second, given
$S\subseteq\Omega(X)$ with $\bigcup S\in\mathcal{F}_{x}$, we have
$U\in\mathcal{F}_{x}$ for some $U\in S$ (if $x\in\bigcup S$ then $x\in U$ for
some $U\in S$). Hence, the characteristic function of
$\mathcal{F}_{x}\subseteq\Omega(X)$ is a frame morphism
$\Omega(X)\to\mathbf{2}$.

A _point_ of a frame $L$ is an element of
$\mathrm{pt}(L)\coloneqq\mathbf{Frm}[L,\mathbf{2}]$. We shall always identify
a point $\mathcal{F}\in\mathbf{Frm}[L,\mathbf{2}]$ with the set $\\{a\in
L\mid\mathcal{F}(a)=1\\}$. Given $a\in L$, let

$\begin{array}[]{l l
l}\mathsf{ext}(a)&\coloneqq&\left\\{\mathcal{F}\in\mathrm{pt}(L)\mid
a\in\mathcal{F}\right\\}\end{array}$

The function $\mathsf{ext}\colon L\to\mathcal{P}(\mathrm{pt}(L))$ is a frame
morphism (see e.g. [Joh82, Lemma II.1.6]). In particular, its image is a sub-
frame of $\mathcal{P}(\mathrm{pt}(L))$, and is thus a topology
$\Omega(\mathrm{pt}(L))$ on $\mathrm{pt}(L)$. The _space of points_ of $L$ is
$(\mathrm{pt}(L),\Omega(\mathrm{pt}(L))$.

The operation $L\mapsto\mathrm{pt}(L)$ extends to a functor
$\mathrm{pt}\colon\mathbf{Frm}^{\mathrm{op}}\to\mathbf{Top}$ which is right
adjoint to $\Omega$ (see e.g. [Joh82, Theorem II.1.4]). The action of
$\mathrm{pt}\colon\mathbf{Frm}^{\mathrm{op}}\to\mathbf{Top}$ on a frame
morphism $f\colon L\to K$ is the continuous function
$\mathrm{pt}(K)\to\mathrm{pt}(L)$ which takes
$\mathcal{F}\in\mathbf{Frm}[K,\mathbf{2}]$ to
$\mathcal{F}\mathbin{\circ}f\in\mathbf{Frm}[L,\mathbf{2}]$. The unit at
$X\in\mathbf{Top}$ of the adjunction $\Omega\dashv\mathrm{pt}$ is the
continuous function $\eta_{X}\colon X\to\mathrm{pt}(\Omega(X))$ taking $x$ to
$\mathcal{F}_{x}$.

##### Sober Spaces.

The function $\eta_{X}\colon X\to\mathrm{pt}(\Omega(X))$ continuously maps the
space $X$ to its space of “converging formal approximations”
$\mathrm{pt}(\Omega(X))$. But $\mathrm{pt}(\Omega(X))$ may not correctly
represent $X$. A space $X$ is _sober_ if $\eta_{X}$ is a bijection (in which
case $\eta_{X}$ is automatically an homeomorphism, see [Joh82, §II.1.6]).

Given a frame $L$, the space of points $\mathrm{pt}(L)$ is always sober
([Joh82, Lemma II.1.7]). Hence (by functoriality of $\Omega$ and
$\mathrm{pt}$), if $X$ is homeomorphic to $\mathrm{pt}(L)$, then $X$ is sober
as well. It follows from [Joh82, Lemma II.1.6.(ii)] that $A^{\omega}$ is sober
for its product topology.666Actually, [Joh82, Lemma II.1.6.(ii)] states that
each $T_{2}$ space is sober. But not every dcpo is sober ([Joh82, II.1.9]).
For the following, see e.g. [Joh82, Theorem VII.2.6].

######  Proposition 1.

Algebraic dcpos are sober.

######  Remark 3.1.

In fact, a sober space is always $T_{0}$, and is moreover a dcpo w.r.t. its
specialization order ([Joh82, Lemmas II.1.6(i) and II.1.9]). This provides a
functor $\mathbf{Frm}^{\mathrm{op}}\to\mathbf{DCPO}$ which is actually right
adjoint to the composite
$\mathbf{DCPO}\hookrightarrow\mathbf{Top}\to\mathbf{Frm}^{\mathrm{op}}$,
yielding the _Scott adjunction_ of [DL22].

In particular, a sober dcpo is completely determined by the specialization
order of its space of points. On the other hand, beware that the composite
$\mathbf{Frm}^{\mathrm{op}}\to\mathbf{DCPO}\to\mathbf{Frm}^{\mathrm{op}}$ may
loose a lot of structure (e.g. it takes the product topology on $A^{\omega}$
to the discrete (Scott) topology).

###  3.3 Sobriety of Subspaces

Proposition 1 and Remark 3.1 imply that for an algebraic dcpo $X$, the
topological notion of approximation coincides with the domain-theoretic one.
But we are interested in subspaces of the algebraic cpo
$\llbracket\mathsf{Str}A\rrbracket$. Discussing the sobriety of such subspaces
involves going further in the point-free setting. While the main results of
this §3.3 are important for this paper, the technical developments
full,longare used again only in §A.shortare used again only in [rs23full, §A].

Let $(X,\Omega)$ be a space, and consider some $P\subseteq X$. The subspace
inclusion
$\iota\colon(P,\Omega\mathord{\upharpoonright}P)\hookrightarrow(X,\Omega)$
induces the surjective frame morphism
${\iota}^{\star}\coloneqq\Omega(\iota)\colon\Omega\twoheadrightarrow\Omega\mathord{\upharpoonright}P$
which takes $U\in\Omega$ to $(U\cap P)\in\Omega\mathord{\upharpoonright}P$.
The following is a handy reformulation of sobriety for
$(P,\Omega\mathord{\upharpoonright}P)$.

Assume that $(X,\Omega)$ is sober. Then the following are equivalent.

  1. (i)

$(P,\Omega\mathord{\upharpoonright}P)$ is sober.

  2. (ii)

For each $x\in X$, we have $x\in P$ if, and only if,
$\mathcal{F}_{x}=\mathcal{G}\mathbin{\circ}{\iota}^{\star}$ for some
$\mathcal{G}\in\mathrm{pt}(\Omega\mathord{\upharpoonright}P)$.

${\Omega}$${\Omega\mathord{\upharpoonright}P}$${\mathbf{2}}$$\scriptstyle{{\iota}^{\star}}$$\scriptstyle{\mathcal{F}_{x}}$$\scriptstyle{\mathcal{G}}$

Let $L$ be a frame. A _quotient frame_ of $L$ is an isomorphism-class of
surjective frame morphisms $L\twoheadrightarrow K$. We are going to discuss an
abstract but mathematically powerful representation of the quotient frame
$\Omega\twoheadrightarrow\Omega\mathord{\upharpoonright}P$. We use tools from
[Joh82, §II.2] and [PP11, §VI.1] on the dual notion of _sub-locale_.

Everything starts from Galois connections and related adjointness properties,
for which we refer to [DP02, 7.23–7.34]. Fix a frame morphism $f\colon L\to
K$. Since $f\colon L\to K$ preserves all sups, it has an _upper adjoint_
${f}_{\star}\colon K\to L$. This means that for all $a\in L$ and all $b\in K$,

$f(a)\leq_{K}b\qquad\text{if, and only if,}\qquad a\leq_{L}{f}_{\star}(b)$

The pair $(f,{f}_{\star})$ thus forms a Galois connection, and ${f}_{\star}$
is (uniquely) determined by

$\begin{array}[]{l l l}{f}_{\star}(b)&=&\bigvee_{L}\left\\{a\mid
f(a)\leq_{K}b\right\\}\end{array}$

The function ${f}_{\star}$ is in general not a frame morphism, but it always
preserves all infs.

The composition $j\coloneqq{f}_{\star}\mathbin{\circ}f\colon L\to L$ is a
_nucleus_ in the sense of [Joh82, §II2.2]: we have (i) $j(a\wedge
a^{\prime})=j(a)\wedge j(a^{\prime})$, (ii) $a\leq j(a)$ and (iii),
$j(j(a))\leq j(a)$. Nuclei are monotone and idempotent. If $j\colon L\to L$ is
a nucleus, then the set $L_{j}\coloneqq\left\\{a\in L\mid j(a)=a\right\\}$ of
_$j$ -fixpoints_ is a frame and $j\colon L\to L_{j}$ is a frame morphism
([Joh82, Lemma II.2.2]). Note that the finite infs in $L_{j}$ are those of
$L$. But the sup of $S\subseteq L_{j}$ in $L_{j}$ is $j(\bigvee_{L}S)$.

Consider now a subspace inclusion
$\iota\colon(P,\Omega\mathord{\upharpoonright}P)\hookrightarrow(X,\Omega)$.
Following [PP11, §VI.1.1], we write $\widetilde{P}$ for the frame of
$j$-fixpoints, where $j\coloneqq{\iota}_{\star}\mathbin{\circ}{\iota}^{\star}$
and ${\iota}_{\star}$ is the upper adjoint of ${\iota}^{\star}$.

${\Omega}$${\Omega\mathord{\upharpoonright}P}$${\Omega}$$\scriptstyle{{\iota}^{\star}}$$\scriptstyle{{\iota}_{\star}}$

We rely on the following description of the nucleus $j$ (see also [PP11,
§III.5 and §VI.1.1]).

######  Remark 3.2.

Given an open $U\in\Omega$ of $X$, we have

$\begin{array}[]{l l l}j(U)&=&\bigcup\left\\{V\in\Omega\mid V\cap P=U\cap
P\right\\}\end{array}$

The proof of [Joh82, Theorem II.2.3] gives Lemma 3.3 below. Recall that order-
isomorphisms preserve all existing sups and infs ([DP02, Lemma 2.27(ii)]).

The function ${\iota}_{\star}\colon\Omega\mathord{\upharpoonright}P\to\Omega$
co-restricts to a frame isomorphism
${\iota}_{\star}\colon\Omega\mathord{\upharpoonright}P\to\widetilde{P}$.

We use
$j={\iota}_{\star}{\iota}^{\star}\colon\Omega\twoheadrightarrow\widetilde{P}$
to represent the quotient frame induced by the subspace inclusion
$\iota\colon(P,\Omega\mathord{\upharpoonright}P)\hookrightarrow(X,\Omega)$.
The frame $\widetilde{P}$ turns out to be a good tool for studying the
sobriety of $(P,\Omega\mathord{\upharpoonright}P)$. Following [PP11, VI.1.3],
given $x\in X$ we let $\widetilde{x}\coloneqq
X\setminus\overline{\\{x\\}}=X\setminus\mathord{\downarrow}x$. We shall now
see that it is useful to characterize when $\widetilde{x}\in\widetilde{P}$
(i.e. when $j(\widetilde{x})=\widetilde{x}$).

######  Remark 3.3.

Given $x\in X$ and $U\in\Omega$, we have $U\subseteq\widetilde{x}$ if, and
only if, $x\notin U$.

Let $x\in X$ and $\widetilde{\mathcal{F}}_{x}\coloneqq\\{U\in\widetilde{P}\mid
x\in U\\}$. Then $\widetilde{\mathcal{F}}_{x}\in\mathrm{pt}(\widetilde{P})$ if
and only if $\widetilde{x}\in\widetilde{P}$.

######  Proposition 2.

Let $P\subseteq X$ with $(X,\Omega)$ sober. Then the following are equivalent.

  1. (i)

$(P,\Omega\mathord{\upharpoonright}P)$ is sober.

  2. (ii)

For each $x\in X$, we have $x\in P$ if, and only if,
$\widetilde{x}\in\widetilde{P}$.

In condition (ii) above, we actually always have
$\widetilde{x}\in\widetilde{P}$ when $x\in P$ (see [PP11, VI.1.3.1]).

Proposition 2 will yield a general sufficient condition for the sobriety of
$(P,\Omega P)$ (Theorem 3.3 below), from which we will obtain the case of
negation-free $\mathsf{LTL}$ (Corollary 3.3).

One further step into the point-free setting gives us sharper results. A space
$(X,\Omega)$ is $T_{D}$ when for each $x\in X$, there is some open
$U\in\Omega$ such that $x\in U$ and $(U\setminus\\{x\\})\in\Omega$. See [PP11,
§I.2]. It is shown in [PP11, Proposition VI.1.3.1] that if $X$ is a (possibly
not sober) $T_{D}$ space, then condition (ii) of Proposition 2 holds for _any_
$P\subseteq X$. It follows that if $X$ is sober _and_ $T_{D}$, then each
$P\subseteq X$ induces a sober subspace.

Consider now the case of a sober space $(X,\Omega)$ which is not $T_{D}$.
Hence, there is some $x\in X$ such that for all open $U$ with $x\in U$, the
set $U\setminus\\{x\\}$ is not open.

Let $x\in X$ as above and set $P\coloneqq X\setminus\\{x\\}$. Then
$(P,\Omega\mathord{\upharpoonright}P)$ is not sober.

It follows from [PP11, §I.2.1] that $A^{\omega}$ is $T_{D}$ for the product
topology.777Actually, each $T_{1}$ space is $T_{D}$ ([PP11, §I.2.1]). But
$\llbracket\mathsf{Str}A\rrbracket$ is not $T_{D}$, unless $A=\emptyset$.
Consider $a^{\omega}\in\llbracket\mathsf{Str}A\rrbracket$. Then any Scott-open
$U$ containing $a^{\omega}$ contains also some finite
$d\leq_{\llbracket\mathsf{Str}A\rrbracket}a^{\omega}$. Hence
$U\setminus\\{a^{\omega}\\}$ is not upward-closed and thus not Scott-open.

$\llbracket\lnot\square
a\rrbracket=\llbracket\mathsf{Str}A\rrbracket\setminus\\{a^{\omega}\\}$ is not
a sober subspace of $\llbracket\mathsf{Str}A\rrbracket$.

Let $(X,\Omega)$ be sober, and let $P\subseteq X$ be upward-closed for
$\leq_{\Omega}$. Assume $x\notin P$. Then $P\setminus\mathord{\downarrow}x=P$,
and thus $P\cap\widetilde{x}=P$. Hence
$j(\widetilde{x})=\bigcup\left\\{V\in\Omega\mid V\cap P=P\right\\}$, so
$j(\widetilde{x})=X$ and $\widetilde{x}\notin\widetilde{P}$. It follows that
$x\in P$ precisely when $\widetilde{x}\in\widetilde{P}$, and Proposition 2
gives the following.

If $(X,\Omega)$ is sober and $P\subseteq X$ is upward-closed for
$\leq_{\Omega}$, then $(P,\Omega\mathord{\upharpoonright}P)$ is sober.

If $(X,\Omega)$ is a sober dcpo and if $P\subseteq X$ is upward-closed, then
$(P,\Omega\mathord{\upharpoonright}P)$ is sober. In particular, if $\Phi$ is
negation-free, then $\llbracket\Phi\rrbracket$ is a sober subspace of
$\llbracket\mathsf{Str}A\rrbracket$.

The importance we give to the negation-free fragment of $\mathsf{LTL}$
ultimately rests on Corollaries 3.3 and 3.3. But the frame $\widetilde{P}$
seems too abstract to be used concretely.

##  4 Geometric Logic

Geometric logic is an infinitary propositional logic which describes frames.
Very roughly, the idea is that if a theory $\mathtt{Th}$ in geometric logic
represents a frame $L$, then the models of $\mathtt{Th}$ can be organized in a
space which is homeomorphic to $\mathrm{pt}(L)$, the space of points of $L$.

We will represent the (sober) space $\llbracket\mathsf{Str}A\rrbracket$ by a
theory $\mathtt{T}\llbracket\mathsf{Str}A\rrbracket$ in geometric logic.
Further, for each negation-free formula $\Phi$ of $\mathsf{LTL}$, we shall
(inductively) devise a theory $\mathtt{T}\llbracket\Phi\rrbracket$ such that
$\mathtt{T}\llbracket\mathsf{Str}A\rrbracket\cup\mathtt{T}\llbracket\Phi\rrbracket$
represents the (sober) subspace induced by
$\llbracket\Phi\rrbracket\hookrightarrow\llbracket\mathsf{Str}A\rrbracket$.
This will provide a concrete presentation of the corresponding quotient frame.

Our approach to geometric logic here is not the usual one, as presented in
e.g. [Vic07] (see also [Joh02, §D]). full,longThe relations between the two
approaches are discussed in §A.shortThe relations between the two approaches
are discussed in [rs23full, §A].

###  4.1 Geometric Theories

##### Formulae and Valuations.

Let $\mathit{At}$ be a set of _atomic propositions_. The _conjunctive_ and the
_geometric_ formulae over $\mathit{At}$ are respectively defined as

$\begin{array}[]{l l l !{\qquad\text{and}\qquad} l l
l}\gamma,\gamma^{\prime}\in\mathtt{Conj}(\mathit{At})&\Coloneqq&p\leavevmode\nobreak\
\leavevmode\nobreak\ |\leavevmode\nobreak\ \leavevmode\nobreak\
\mathtt{true}\leavevmode\nobreak\ \leavevmode\nobreak\ |\leavevmode\nobreak\
\leavevmode\nobreak\
\gamma\land\gamma^{\prime}\par&\varphi,\psi,\theta\in\mathtt{Geom}(\mathit{At})&\Coloneqq&\bigvee
S\end{array}$

where $p\in\mathit{At}$ and $S\subseteq\mathtt{Conj}(\mathit{At})$. A
_valuation_ of $\mathit{At}$ is a function
$\nu\colon\mathit{At}\to\mathbf{2}$. Given
$\chi\in\mathtt{Conj}(\mathit{At})\cup\mathtt{Geom}(\mathit{At})$, the
_satisfaction relation_ $\nu\models\chi$ is defined by

$\begin{array}[]{l c l !{\qquad} l c
l}\nu\models\mathtt{true}&&&\nu\models\gamma\land\gamma^{\prime}&\text{iff}&\text{$\nu\models\gamma$
and $\nu\models\gamma^{\prime}$}\\\ \nu\models
p&\text{iff}&\nu(p)=1\par\par&\nu\models\bigvee S&\text{iff}&\text{there
exists $\gamma\in S$ such that $\nu\models\gamma$}\par\end{array}$

We let $\mathtt{false}$ be the geometric formula $\bigvee\emptyset$. We may
write $\gamma$ for the geometric formula $\bigvee\\{\gamma\\}$. Given
conjunctive formulae $(\gamma_{i}\mid i\in I)$, we write $\bigvee_{i\in
I}\gamma_{i}$ for the geometric formula $\bigvee\\{\gamma_{i}\mid i\in I\\}$.
Note that $\bigvee_{i\in I}\gamma_{i}=\bigvee_{j\in J}\gamma^{\prime}_{j}$ if
there is a bijection $f\colon I\to J$ with
$\gamma_{i}=\gamma^{\prime}_{f(i)}$.

######  Remark 4.1.

There is no primitive notion of conjunction or disjunction on geometric
formulae, but they can be defined. Given $(\varphi_{i}\mid i\in I)$ with
$\varphi_{i}=\bigvee\left\\{\gamma_{i,j}\mid j\in J_{i}\right\\}$, we define
$\bigvee_{i\in I}\varphi_{i}$ to be the geometric formula
$\bigvee\left\\{\gamma_{i,j}\mid\text{$i\in I$ and $j\in J_{i}$}\right\\}$. We
then have $\nu\models\bigvee_{i\in I}\varphi_{i}$ iff $\nu\models\varphi_{i}$
for some $i\in I$.

Similarly, given $\varphi=\bigvee_{i\in I}\gamma_{i}$ and $\psi=\bigvee_{j\in
J}\gamma^{\prime}_{j}$, we define
$\varphi\land\psi\coloneqq\bigvee\\{\gamma_{i}\land\gamma^{\prime}_{j}\mid(i,j)\in
I\times J\\}$. Then $\nu\models\varphi\land\psi$ iff $\nu\models\varphi$ and
$\nu\models\psi$.

##### Sequents and Theories.

A _sequent_ over $\mathit{At}$ is a pair $\psi\vdash\varphi$ of geometric
formulae $\varphi,\psi\in\mathtt{Geom}(\mathit{At})$. A valuation $\nu$ of
$\mathit{At}$ is a _model_ of $\psi\vdash\varphi$ if $\nu\models\psi$ implies
$\nu\models\varphi$. Note that $\nu$ is a model of the sequent
$\varphi\vdash\mathtt{false}$ if, and only if, $\nu\not\models\varphi$.

A _geometric theory_ over $\mathit{At}$ is a set $\mathtt{T}$ of sequents over
$\mathit{At}$. A valuation $\nu$ of $\mathit{At}$ is a _model_ of $\mathtt{T}$
if $\nu$ is a model of all the sequents of $\mathtt{T}$. We write
$\mathbf{Mod}(\mathtt{T})$ for the set of models of $\mathtt{T}$.

An _antecedent-free sequent_ has the form $\mathtt{true}\vdash\varphi$, and is
denoted $\vdash\varphi$ (or even $\varphi$) for short. An _antecedent-free
theory_ consists of antecedent-free sequents only.

##### Algebraic Dcpos.

Algebraic dcpos have a natural representation by geometric theories. This
relies on the following well-known facts, for which we refer to [AC98, §1.1].

An _ideal_ on a poset $(P,\leq)$ is a subset $J\subseteq P$ which is downward-
closed and directed. The set $\mathrm{Idl}(P)$ of ideals on $P$ is an
algebraic dcpo for inclusion. The operation $P\mapsto\mathrm{Idl}(P)$ is left
adjoint to the forgetful functor from $\mathbf{DCPO}$ to the category of
posets and monotone maps.

Let $X$ be a dcpo, and let $\mathrm{Fin}(X)$ be its sub-poset of finite
elements. Given an ideal $J\in\mathrm{Idl}(\mathrm{Fin}(X))$, since $J$ is
directed we have $\bigvee J\in X$. For the following, see e.g. [AC98, Proof of
Proposition 1.1.21(2)].

Let $X$ be an algebraic dcpo. The function
$J\in\mathrm{Idl}(\mathrm{Fin}(X))\mapsto\bigvee J\in X$ is an order-
isomorphism. Its inverse $X\to\mathrm{Idl}(\mathrm{Fin}(X))$ takes $x$ to
$\\{d\in\mathrm{Fin}(X)\mid d\leq x\\}$.

We represent an algebraic dcpo $X=(X,\leq_{X})$ by a geometric theory
$\mathtt{T}(X)$ over $\mathit{At}=\mathrm{Fin}(X)$. The theory $\mathtt{T}(X)$
consists of $\vdash\bigvee\mathrm{Fin}(X)$ together with all the sequents

$\begin{array}[]{c}d\vdash d^{\prime}\quad\text{(if
$d^{\prime}\leq_{X}d$)}\par\qquad\quad\par\par d\land
d^{\prime}\vdash\bigvee\left\\{d^{\prime\prime}\in\mathrm{Fin}(X)\mid\text{$d\leq_{X}d^{\prime\prime}$
and $d^{\prime}\leq_{X}d^{\prime\prime}$}\right\\}\end{array}$

where $d,d^{\prime}\in\mathrm{Fin}(X)$. Note that $J\subseteq\mathrm{Fin}(X)$
is an ideal if, and only if, its characteristic function
$\mathrm{Fin}(X)\to\mathbf{2}$ is a model of $\mathtt{T}(X)$. Combined with
Lemma 4.1, this yields Proposition 3 below. If $x\in X$, let
$\nu(x)\colon\mathit{At}\to\mathbf{2}$ be the characteristic function of
$\\{d\in\mathrm{Fin}(X)\mid d\leq_{X}x\\}$.

######  Proposition 3.

The map $x\mapsto\nu(x)$ is a bijection $X\to\mathbf{Mod}(\mathtt{T}(X))$.

When $X$ is actually an algebraic cpo, let $\mathtt{T}_{\bot}(X)$ be the
theory obtained from $\mathtt{T}(X)$ by replacing the antecedent-free sequent
$\vdash\bigvee\mathrm{Fin}(X)$ with $\vdash\bot_{X}$ (where
$\bot_{X}\in\mathrm{Fin}(X)$ is the least element of $X$). The theories
$\mathtt{T}(X)$ and $\mathtt{T}_{\bot}(X)$ have exactly the same models. Hence
Proposition 3 also holds with $\mathtt{T}_{\bot}(X)$ in place of
$\mathtt{T}(X)$.

[Streams] We further simplify the theory representing the cpo
$\llbracket\mathsf{Str}A\rrbracket$.

Consider $x,y\in\llbracket\mathsf{Str}A\rrbracket$ such that
$\mathord{\uparrow}x\cap\mathord{\uparrow}y\neq\emptyset$ (i.e. such that
$x,y\leq_{\llbracket\mathsf{Str}A\rrbracket}z$ for some
$z\in\llbracket\mathsf{Str}A\rrbracket$). Then, since $\llbracket A\rrbracket$
is a flat cpo, we have $x(n)=y(n)$ for all
$n\in\mathrm{supp}(x)\cap\mathrm{supp}(y)$. It follows that the set
$\\{x,y\\}$ has a sup $x\vee_{\llbracket\mathsf{Str}A\rrbracket}y$ in
$\llbracket\mathsf{Str}A\rrbracket$. Note that
$x\vee_{\llbracket\mathsf{Str}A\rrbracket}y$ is finite whenever so are $x$ and
$y$.

Hence, we can represent $\llbracket\mathsf{Str}A\rrbracket$ with the following
theory $\mathtt{T}\llbracket\mathsf{Str}A\rrbracket$, where
$d,d^{\prime}\in\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$.

$\begin{array}[]{r !{\thesis} l @{\quad} l !{\qquad\qquad} r !{\thesis} l
@{\quad} l}d\lx@intercol\vdash&d^{\prime}&\text{(if
$d^{\prime}\leq_{\llbracket\mathsf{Str}A\rrbracket}d$)}\par&d\land
d^{\prime}\lx@intercol\vdash&\mathtt{false}&\text{(if
$\mathord{\uparrow}d\cap\mathord{\uparrow}d^{\prime}=\emptyset$)}\\\
\lx@intercol\vdash&\bot^{\omega}&&d\land
d^{\prime}\lx@intercol\vdash&d\vee_{\llbracket\mathsf{Str}A\rrbracket}d^{\prime}&\text{(if
$\mathord{\uparrow}d\cap\mathord{\uparrow}d^{\prime}\neq\emptyset$)}\end{array}$

######  Remark 4.2.

Note that the theory $\mathtt{T}(\llbracket\mathsf{Str}A\rrbracket)$ of
Example 3 only involves finite geometric formulae. Actually, this amounts to
the fact that $\llbracket\mathsf{Str}A\rrbracket$ is _spectral_ in its Scott
topology (see [GvG23, Corollary 7.48 and Definition 6.2]).888Note that
$\llbracket\mathsf{Str}A\rrbracket$ is always compact, since any Scott-open
containing $\bot^{\omega}$ contains the whole of
$\llbracket\mathsf{Str}A\rrbracket$. This contrasts with the product topology
on $A^{\omega}$, which is compact iff $A$ is finite (see e.g. [PP04,
§III.3.5]). Roughly, being a spectral space means that the topology can be
generated from a distributive lattice (as opposed to a frame). See e.g.
[GvG23, Proposition 3.26 and Theorem 6.1] for details.

Spectral cpos include those known as “SFP” domains (see e.g. [Abr91, §2.2]).
SFP domains are also called “bifinite” domains (see e.g. [AC98, Definition
5.2.2 and Theorem 5.2.7]). They are stable under most common domain operations
and have solutions for recursive type equations (see e.g. [Abr91, §2.2]).

short full,long In the paradigm of “Domain Theory in Logical Form”, spectral
domains are particularly important because the logic of the underlying
distributive lattice can be incorporated into finitary type systems [Abr91]
(see also [AC98, §10.5] for a simple instance).999Note that
$\llbracket\mathsf{Str}A\rrbracket$ is always compact, since any Scott-open
containing $\bot^{\omega}$ contains the whole of
$\llbracket\mathsf{Str}A\rrbracket$. This contrasts with the product topology
on $A^{\omega}$, which is compact iff $A$ is finite (see e.g. [PP04,
§III.3.5]).

###  4.2 The Sober Space of Models

Given a geometric theory $\mathtt{T}$ over $\mathit{At}$, we will now equip
$\mathbf{Mod}(\mathtt{T})$ with a sober topology induced by a quotient of
$\mathtt{Geom}(\mathit{At})$. In particular, this will extend the bijection of
Proposition 3 to an homeomorphism between an algebraic dcpo $X$ and the space
of models $\mathbf{Mod}(\mathtt{T}(X))$.

In view of Example 3, we may have
$\mathbf{Mod}(\mathtt{T})=\mathbf{Mod}(\mathtt{U})$ for different theories
$\mathtt{T}$ and $\mathtt{U}$ over $\mathit{At}$. The topology on
$M=\mathbf{Mod}(\mathtt{T})$ depends on $M$ (and $\mathit{At}$), but not on
the theory $\mathtt{T}$ such that $M=\mathbf{Mod}(\mathtt{T})$. Fix a set of
atomic propositions $\mathit{At}$ and let $M$ be a set of the form
$\mathbf{Mod}(\mathtt{T})$ for some theory $\mathtt{T}$ over $\mathit{At}$.
Define

$\mathsf{mod}_{M}\colon\mathtt{Geom}(\mathit{At})\to\mathcal{P}(M),\quad\varphi\mapsto\left\\{\nu\in
M\mid\nu\models\varphi\right\\}$

Let $\Omega(M)\subseteq\mathcal{P}(M)$ be the image of $\mathsf{mod}_{M}$. We
have $\mathsf{mod}_{M}(\mathtt{true})=M$, and (via Remark 4.1),

$\begin{array}[]{c !{\quad\text{and}\quad}
c}\mathsf{mod}_{M}(\varphi\land\psi)=\mathsf{mod}_{M}(\varphi)\cap\mathsf{mod}_{M}(\psi)\par&\mathsf{mod}_{M}\left(\bigvee_{i\in
I}\varphi_{i}\right)=\bigcup_{i\in I}\mathsf{mod}_{M}(\varphi_{i})\end{array}$

It follows that $(\Omega(M),\subseteq)$ is stable under the sups and the
finite infs of $(\mathcal{P}(M),\subseteq)$. Hence $(\Omega(M),\subseteq)$ is
a sub-frame of $(\mathcal{P}(M),\subseteq)$, and $(M,\Omega(M))$ is a
topological space.

Given a theory $\mathtt{T}$, we write $\mathbf{Mod}(\mathtt{T})$ for
$(\mathbf{Mod}(\mathtt{T}),\Omega(\mathbf{Mod}(\mathtt{T})))$, the _space of
models of $\mathtt{T}$_. Since the space $\mathbf{Mod}(\mathtt{T})$ only
depends on the models of $\mathtt{T}$, the following directly applies to the
theory $\mathtt{T}\llbracket\mathsf{Str}A\rrbracket$ of Example 3.

######  Proposition 4.

Let $X$ be an algebraic dcpo. The bijection $x\mapsto\nu(x)$ of Proposition 3
extends to an homeomorphism from $X$ to $\mathbf{Mod}(\mathtt{T}(X))$.

Spaces of models are always sober. To this end, given $M$ as above, we
quotient $\mathtt{Geom}(\mathit{At})$ under the preorder $\preceq_{M}$ with
$\varphi\preceq_{M}\psi$ iff
$\mathsf{mod}_{M}(\varphi)\subseteq\mathsf{mod}_{M}(\psi)$. The relation
$\sim_{M}$ of _$M$ -equivalence_ on $\mathtt{Geom}(\mathit{At})$ is defined as
$\varphi\sim_{M}\psi$ iff $\varphi\preceq_{M}\psi$ and
$\psi\preceq_{M}\varphi$ (i.e.
$\mathsf{mod}_{M}(\varphi)=\mathsf{mod}_{M}(\psi)$). We let $[\varphi]_{M}$ be
the $\sim_{M}$-class of $\varphi$, and $\mathtt{Geom}(\mathit{At})/M$ be the
set of $\sim_{M}$-classes of geometric formulae. We write $\leq_{M}$ for the
partial order on $\mathtt{Geom}(\mathit{At})/M$ induced by the preorder
$\preceq_{M}$ (see e.g. [GL13, §2.3.1]).

The function $\mathsf{mod}_{M}$ yields an order-isomorphism
$(\mathtt{Geom}(\mathit{At})/M,\leq_{M})\to(\Omega(M),\subseteq)$. Since
order-isomorphisms preserve all existing sups and infs ([DP02, Lemma
2.27(ii)]), we obtain

$(\mathtt{Geom}(\mathit{At})/M,\leq_{M})$ is a frame with greatest element
$[\mathtt{true}]_{M}$, and

$\begin{array}[]{r c l}[\bigvee_{i\in I}\gamma_{i}]_{M}\wedge[\bigvee_{j\in
J}\gamma^{\prime}_{j}]_{M}&=&[\bigvee\left\\{\gamma_{i}\land\gamma^{\prime}_{j}\mid\text{$i\in
I$ and $j\in J$}\right\\}]_{M}\\\ \bigvee_{i\in I}[\bigvee_{j\in
J_{i}}\gamma_{i,j}]_{M}&=&[\bigvee\left\\{\gamma_{i,j}\mid\text{$i\in I$ and
$j\in J_{i}$}\right\\}]_{M}\end{array}$

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. The function taking
$\nu\in\mathbf{Mod}(\mathtt{T})$ to
$\\{[\varphi]_{\mathbf{Mod}(\mathtt{T})}\mid\nu\models\varphi\\}$ is an
homeomorphism from $\mathbf{Mod}(\mathtt{T})$ to
$\mathrm{pt}(\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T}))$.

Let $\mathtt{T}$ be a geometric theory. The space $\mathbf{Mod}(\mathtt{T})$
is sober.

##### Subspaces.

Consider a (sober) space $(X,\Omega)$. Assume that $X$ is represented by a
geometric theory $\mathtt{T}$ over $\mathit{At}$, in the sense that $X$ is
homeomorphic to the space $\mathbf{Mod}(\mathtt{T})$. Given a subset
$P\subseteq X$, there might be a theory $\mathtt{U}$ over $\mathit{At}$ such
that the bijection $X\cong\mathbf{Mod}(\mathtt{T})$ restricts to a bijection
$P\cong\mathbf{Mod}(\mathtt{T}\cup\mathtt{U})$. In this case, Proposition 5
below implies that the subspace $(P,\Omega\mathord{\upharpoonright}P)$ is
homeomorphic to the space $\mathbf{Mod}(\mathtt{T}\cup\mathtt{U})$, so that
$(P,\Omega\mathord{\upharpoonright}P)$ is sober and
$\Omega\mathord{\upharpoonright}P$ is isomorphic to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T}\cup\mathtt{U})$. In such
situations, we write $\mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$ for the space
$\mathbf{Mod}(\mathtt{T}\cup\mathtt{U})$.

######  Proposition 5.

Given geometric theories $\mathtt{T}$ and $\mathtt{U}$ on $\mathit{At}$, the
space $\mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$ is _equal_ to the subspace
induced by the inclusion
$\mathbf{Mod}(\mathtt{T}\cup\mathtt{U})\subseteq\mathbf{Mod}(\mathtt{T})$.

Let $X$ be an algebraic dcpo, and let $P\coloneqq\mathord{\uparrow}y$ for some
fixed $y\in X$. Given $x\in X$, we have $x\in P$ precisely when $\nu(x)$ is a
model of $\mathtt{U}(y)\coloneqq\\{\vdash d\mid d\leq_{X}y\\}$. Hence, the
subspace induced by $P\subseteq X$ is homeomorphic to
$\mathbf{Mod}_{\mathtt{T}(X)}(\mathtt{U}(y))$.

Assume now $X=\llbracket\mathsf{Str}A\rrbracket$, and let $a\in A$. Since the
subspace induced by the $\mathsf{LTL}$ formula $\lnot\square a$ is not sober
(Corollary 3.3), it follows from Proposition 5 and Corollary 4.2 that there is
_no_ geometric theory $\mathtt{T}$ over
$\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$ such that for all
$x\in\llbracket\mathsf{Str}A\rrbracket$, we have $x\in\llbracket\lnot\square
a\rrbracket$ iff $\nu(x)\in\mathbf{Mod}(\mathtt{T})$.

###  4.3 Operations on Theories

We shall now see that for each negation-free formula $\Phi$ of $\mathsf{LTL}$,
there is a geometric theory $\mathtt{T}\llbracket\Phi\rrbracket$ such that for
all streams $x$, we have $x\in\llbracket\Phi\rrbracket$ iff
$\nu(x)\in\mathbf{Mod}(\mathtt{T}\llbracket\Phi\rrbracket)$ (where $\nu(x)$ is
as in Propositions 3 and 4). This may not be possible if $\Phi$ contains
negations (Example 4.2).

To this end, we devise operations on theories which represent unions and
intersections of sets of models. Given theories $(\mathtt{T}_{i}\mid i\in I)$
over $\mathit{At}$, we let $\bigcurlywedge_{i\in
I}\mathtt{T}_{i}\coloneqq\bigcup_{i\in I}\mathtt{T}_{i}$. Then we have

$\begin{array}[]{l l l}\mathbf{Mod}\left(\bigcurlywedge_{i\in
I}\mathtt{T}_{i}\right)&=&\bigcap_{i\in
I}\mathbf{Mod}(\mathtt{T}_{i})\end{array}$

Intersections of sets of models can thus be represented by unions of theories.
It is more difficult to devise an operation on theories for _unions_ of sets
of models. A solution is provided by the following crucial construction. Let
$(\mathtt{T}_{i}\mid i\in I)$ be theories, all over $\mathit{At}$, with
$\mathtt{T}_{i}=\\{\psi_{i,j}\vdash\varphi_{i,j}\mid j\in J_{i}\\}$.

  1. (1)

If $I$ is finite, we let $\bigcurlyvee_{i\in
I}\mathtt{T}_{i}\coloneqq\left\\{\bigwedge_{i\in
I}\psi_{i,f(i)}\vdash\bigvee_{i\in I}\varphi_{i,f(i)}\mid f\in\prod_{i\in
I}J_{i}\right\\}$.

  2. (2)

If $I$ is infinite, and all $\mathtt{T}_{i}$’s are antecedent-free,
$\bigcurlyvee_{i\in I}\mathtt{T}_{i}\coloneqq\left\\{\vdash\bigvee_{i\in
I}\varphi_{i,f(i)}\mid f\in\prod_{i\in I}J_{i}\right\\}$.

######  Proposition 6.

In both cases above, we have (using the Axiom of Choice when $I$ is infinite)

$\begin{array}[]{l l l}\mathbf{Mod}\left(\bigcurlyvee_{i\in
I}\mathtt{T}_{i}\right)&=&\bigcup_{i\in
I}\mathbf{Mod}(\mathtt{T}_{i})\end{array}$

Let $X$ be an algebraic dcpo, and let $P\subseteq X$ be upward-closed. Then
$P=\bigcup_{y\in P}\mathord{\uparrow}y$. Hence, given $x\in X$, we have $x\in
P$ exactly when $\nu(x)$ is a model of $\bigcurlyvee_{y\in P}\mathtt{U}(y)$,
where $\mathtt{U}(y)$ is as in Example 4.2. Note that combining this with
Proposition 5 and Corollary 4.2 yields another proof of Corollary 3.3.

####  4.3.1 Translation of Negation-Free $\mathsf{LTL}$ Formulae

short full,long Recall from Lemma 2.2 that if $\Phi$ is a negation-free
formula of $\mathsf{LTL}(A)$, then $\llbracket\Phi\rrbracket$ is upward-closed
in $\llbracket\mathsf{Str}A\rrbracket$. Example 4.3 thus provides a geometric
theory over $\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$ for
$\llbracket\Phi\rrbracket$.101010Actually, each $T_{1}$ space is $T_{D}$
([PP11, §I.2.1]). But we shall get more information by explicitly defining a
geometric theory $\mathtt{T}\llbracket\Phi\rrbracket$ by induction on $\Phi$.
Actually, it is even better to work with a stratified presentation of
negation-free $\mathsf{LTL}$.

Our stratification of negation-free $\mathsf{LTL}$ formulae is based on the
following expected fact. Recall from §2.2 the map
$\llbracket\bigcirc\rrbracket$ taking
$S\in\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$ to $\\{x\mid
x\mathord{\upharpoonright}1\in
S\\}\in\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$.

Fix set $A$.

  1. (1)

The function
$\O\llbracket\bigcirc\rrbracket\colon\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)\to\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$
preserves all unions and all intersections.

  2. (2)

Given $\mathsf{LTL}$ formulae $\Phi,\Psi$, let $H_{\Phi,\Psi}$ take
$S\in\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$ to
$\llbracket\Psi\rrbracket\cup(\llbracket\Phi\rrbracket\cap\llbracket\bigcirc\rrbracket(S))$.
Then we have
$\llbracket\Phi\mathrel{\mathsf{U}}\Psi\rrbracket=\bigcup_{n\in\mathbb{N}}H^{n}_{\Phi,\Psi}(\llbracket\mathsf{False}\rrbracket)$
and
$\llbracket\Phi\mathrel{\mathsf{W}}\Psi\rrbracket=\bigcap_{n\in\mathbb{N}}H^{n}_{\Phi,\Psi}(\llbracket\mathsf{True}\rrbracket)$.

$\begin{array}[]{r r l c l c l c l c
l}\Phi_{0},\Psi_{0}&\Coloneqq&\mathsf{False}&|&\mathsf{True}&|&a\\\
&|&\Phi_{0}\lor\Psi_{0}&|&\Phi_{0}\land\Psi_{0}&|&\bigcirc\Phi_{0}\\\ \\\
G(A)\ni\Phi_{1},\Psi_{1}&\Coloneqq&\Phi_{0}\\\
&|&\Phi_{1}\lor\Psi_{1}&|&\Phi_{1}\land\Psi_{1}&|&\bigcirc\Phi_{1}&|&\Phi_{1}\mathrel{\mathsf{U}}\Psi_{1}\\\
\\\ G_{\delta}(A)\ni\Phi_{2},\Psi_{2}&\Coloneqq&\Phi_{1}\\\
&|&\Phi_{2}\lor\Psi_{2}&|&\Phi_{2}\land\Psi_{2}&|&\bigcirc\Phi_{2}&|&\Phi_{2}\mathrel{\mathsf{W}}\Psi_{2}\\\
\\\ \text{n.-f.\ $\mathsf{LTL}(A)$}\ni\Phi_{3},\Psi_{3}&\Coloneqq&\Phi_{2}\\\
&|&\Phi_{3}\lor\Psi_{3}&|&\Phi_{3}\land\Psi_{3}&|&\bigcirc\Phi_{3}&|&\Phi_{3}\mathrel{\mathsf{U}}\Psi_{3}&|&\Phi_{3}\mathrel{\mathsf{W}}\Psi_{3}\end{array}$
Figure 1: Stratified grammar for negation-free $\mathsf{LTL}(A)$, where $a\in
A$.

Figure 1 presents a stratified grammar for negation-free $\mathsf{LTL}(A)$. We
let $G=G(A)$ be the set of all formulae $\Phi_{1},\Psi_{1}$ from the second
layer in Figure 1. $G_{\delta}=G_{\delta}(A)$ consists of formulae
$\Phi_{2},\Psi_{2}$ from the third layer. The negation-free
$\mathsf{LTL}(A)$-formulae are the those from the last layer.

Recall from §2.2 that
$\diamondsuit\Psi=(\mathsf{True}\mathrel{\mathsf{U}}\Psi)$ and
$\square\Phi=(\Phi\mathrel{\mathsf{W}}\mathsf{False})$. Hence, $G$ is closed
under $\diamondsuit(-)$ and $G_{\delta}$ is closed under $\square(-)$. But
$G_{\delta}$ is (crucially) _not_ closed under $\diamondsuit(-)$. In
particular, we have $\bigcirc a,\diamondsuit a\in G$ and $\square
a,\square\diamondsuit a\in G_{\delta}$. On the other hand, the negation-free
formula $\diamondsuit\square a$ is not a $G_{\delta}$ formula.

When looking at $\diamondsuit\Psi$ and $\square\Phi$ via Lemma 4.3.1(2), it is
convenient to simplify the functions $H_{\mathsf{True},\Psi}$ and
$H_{\Phi,\mathsf{False}}$ to respectively
$\llbracket\Psi\rrbracket\cup\llbracket\bigcirc\rrbracket(-)$ and
$\llbracket\Phi\rrbracket\cap\llbracket\bigcirc\rrbracket(-)$. This amounts to
restate Lemma 4.3.1(2) as
$\llbracket\diamondsuit\Psi\rrbracket=\bigcup_{m\in\mathbb{N}}\llbracket\Psi\rrbracket\cup\llbracket\bigcirc\Psi\rrbracket\cup\dots\cup\llbracket\bigcirc^{m}\Psi\rrbracket$,
and similarly for $\llbracket\square\Phi\rrbracket$.

######  Remark 4.3.

The interpretations of formulae from $G$ or $G_{\delta}$ have the expected
topological complexity. Namely, if $\Phi_{1}\in G$, then
$\llbracket\Phi_{1}\rrbracket$ is Scott-open in
$\llbracket\mathsf{Str}A\rrbracket$. If $\Phi_{2}\in G_{\delta}$, then
$\llbracket\Phi_{2}\rrbracket$ is a countable intersection of Scott-opens
(i.e. a $G_{\delta}$ subset of $\llbracket\mathsf{Str}A\rrbracket$).

This stratification of negation-free $\mathsf{LTL}$ allows for a stratified
translation to geometric theories. In fact, each $\mathsf{LTL}$ formula
$\Phi_{1}\in G$ can be translated to a single geometric formula
$\mathtt{F}\llbracket\Phi_{1}\rrbracket$, with
$\mathtt{F}\llbracket\Phi_{0}\rrbracket$ finite when $\Phi_{0}$ is from the
first layer. Formulae $\Phi$ from the last two layers will be translated to
antecedent-free theories $\mathtt{T}\llbracket\Phi\rrbracket$, with
$\mathtt{T}\llbracket\Phi_{2}\rrbracket$ countable when $\Phi_{2}\in
G_{\delta}$.

Fix a set $A$ and let
$\mathit{At}\coloneqq\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$. We
devise operations on geometric formulae and theories which mimic the action of
$\llbracket\bigcirc\rrbracket(-)$ on
$\mathcal{P}(\llbracket\mathsf{Str}A\rrbracket)$. We begin with geometric
formulae. The idea is that given $x\in\llbracket\mathsf{Str}A\rrbracket$ and
$d\in\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$, we have
$d\leq_{\llbracket\mathsf{Str}A\rrbracket}x\mathord{\upharpoonright}1$ exactly
when $(\bot\cdot d)\leq_{\llbracket\mathsf{Str}A\rrbracket}x$. The geometric
formula $\bigcirc\varphi$ then is defined by propagating the stream operation
$d\mapsto\bot\cdot d$ in $\varphi$. We set $\bigcirc d\coloneqq\bot\cdot d$
and

$\begin{array}[]{l !{\deq} l !{\qquad} l !{\deq} l !{\qquad} l !{\deq}
l}\bigcirc\mathtt{true}\hfil\lx@intercol\coloneqq&\mathtt{true}\par&\bigcirc(\gamma\land\gamma^{\prime})\hfil\lx@intercol\coloneqq&(\bigcirc\gamma)\land(\bigcirc\gamma^{\prime})\par&\bigcirc\bigvee_{i\in
I}\gamma_{i}\hfil\lx@intercol\coloneqq&\bigvee_{i\in
I}\bigcirc\gamma_{i}\end{array}$

Given a theory $\mathtt{Th}$ over $\mathit{At}$, we let
$\bigcirc\mathtt{Th}\coloneqq\left\\{\bigcirc\psi\vdash\bigcirc\varphi\mid(\psi\vdash\varphi)\in\mathtt{Th}\right\\}$.
Note that $\bigcirc\mathtt{Th}$ is antecedent-free whenever so is
$\mathtt{Th}$. Recall the map $x\mapsto\nu(x)$ of Propositions 3 and 4.

Let $x\in\llbracket\mathsf{Str}A\rrbracket$.

  1. (1)

We have $\nu(x)\models\bigcirc\varphi$ if, and only if,
$\nu(x\mathord{\upharpoonright}1)\models\varphi$.

  2. (2)

We have $\nu(x)\in\mathbf{Mod}(\bigcirc\mathtt{Th})$ if, and only if,
$\nu(x\mathord{\upharpoonright}1)\in\mathbf{Mod}(\mathtt{Th})$.

We now define a geometric formula $\mathtt{F}\llbracket\Phi_{1}\rrbracket$
over $\mathit{At}$ by induction on $\Phi_{1}\in G$:

$\begin{array}[]{l !{\deq} l !{\qquad} l !{\deq} l
!{\qquad}}\mathtt{F}\llbracket
a\rrbracket\hfil\lx@intercol\coloneqq&a\cdot\bot^{\omega}&\lx@intercol\hfil\lx@intercol\\\
\mathtt{F}\llbracket\mathsf{True}\rrbracket\hfil\lx@intercol\coloneqq&\mathtt{true}\par&\mathtt{F}\llbracket\Phi_{1}\land\Psi_{1}\rrbracket\hfil\lx@intercol\coloneqq&\mathtt{F}\llbracket\Phi_{1}\rrbracket\land\mathtt{F}\llbracket\Psi_{1}\rrbracket\\\
\mathtt{F}\llbracket\mathsf{False}\rrbracket\hfil\lx@intercol\coloneqq&\mathtt{false}\par&\mathtt{F}\llbracket\Phi_{1}\lor\Psi_{1}\rrbracket\hfil\lx@intercol\coloneqq&\mathtt{F}\llbracket\Phi_{1}\rrbracket\lor\mathtt{F}\llbracket\Psi_{1}\rrbracket\\\
\mathtt{F}\llbracket\bigcirc\Phi_{1}\rrbracket\hfil\lx@intercol\coloneqq&\bigcirc\mathtt{F}\llbracket\Phi_{1}\rrbracket\par&\mathtt{F}\llbracket\Phi_{1}\mathrel{\mathsf{U}}\Psi_{1}\rrbracket\hfil\lx@intercol\coloneqq&\bigvee_{n\in\mathbb{N}}\mathtt{H}^{n}_{\mathtt{F}\llbracket\Phi_{1}\rrbracket,\mathtt{F}\llbracket\Psi_{1}\rrbracket}(\mathtt{false})\end{array}$

where
$\mathtt{H}_{\varphi,\psi}(\theta)\coloneqq\psi\lor(\varphi\land\bigcirc(\theta))$.
(We silently included the case of $\Phi_{0}$ from the first layer.)

Let $\Phi_{1}\in G$. Given $x\in\llbracket\mathsf{Str}A\rrbracket$, we have
$x\in\llbracket\Phi_{1}\rrbracket$ if, and only if,
$\nu(x)\models\mathtt{F}\llbracket\Phi_{1}\rrbracket$.

Finally, the antecedent-free theory $\mathtt{T}\llbracket\Phi_{3}\rrbracket$
is defined by induction on $\Phi_{3}$ as follows:

$\begin{array}[]{l !{\deq} l !{\qquad} l !{\deq}
l}\mathtt{T}\llbracket\Phi_{1}\rrbracket\hfil\lx@intercol\coloneqq&\\{\vdash\mathtt{F}\llbracket\Phi_{1}\rrbracket\\}\par&\mathtt{T}\llbracket\bigcirc\Phi_{3}\rrbracket\hfil\lx@intercol\coloneqq&\bigcirc\mathtt{T}\llbracket\Phi_{3}\rrbracket\\\
\mathtt{T}\llbracket\Phi_{3}\land\Psi_{3}\rrbracket\hfil\lx@intercol\coloneqq&\mathtt{T}(\llbracket\Phi_{3}\rrbracket)\curlywedge\mathtt{T}(\llbracket\Psi_{3}\rrbracket)\par&\mathtt{T}\llbracket\Phi_{3}\mathrel{\mathsf{W}}\Psi_{3}\rrbracket\hfil\lx@intercol\coloneqq&\bigcurlywedge_{n\in\mathbb{N}}\mathtt{TH}^{n}_{\mathtt{T}\llbracket\Phi_{3}\rrbracket,\mathtt{T}\llbracket\Psi_{3}\rrbracket}(\\{\vdash\mathtt{true}\\})\\\
\mathtt{T}\llbracket\Phi_{3}\lor\Psi_{3}\rrbracket\hfil\lx@intercol\coloneqq&\mathtt{T}(\llbracket\Phi_{3}\rrbracket)\curlyvee\mathtt{T}(\llbracket\Psi_{3}\rrbracket)\par&\mathtt{T}\llbracket\Phi_{3}\mathrel{\mathsf{U}}\Psi_{3}\rrbracket\hfil\lx@intercol\coloneqq&\bigcurlyvee_{n\in\mathbb{N}}\mathtt{TH}^{n}_{\mathtt{T}\llbracket\Phi_{3}\rrbracket,\mathtt{T}\llbracket\Psi_{3}\rrbracket}(\\{\vdash\mathtt{false}\\})\end{array}$

where
$\mathtt{TH}_{\mathtt{T},\mathtt{U}}(\mathtt{V})\coloneqq\mathtt{U}\curlyvee(\mathtt{T}\curlywedge\bigcirc\mathtt{V})$.
(We silently included the case of $\Phi_{2}\in G_{\delta}$.)

Let $\Phi$ be negation-free. For $x\in\llbracket\mathsf{Str}A\rrbracket$, we
have $x\in\llbracket\Phi\rrbracket$ if, and only if,
$\nu(x)\in\mathbf{Mod}(\mathtt{T}\llbracket\Phi\rrbracket)$.

######  Remark 4.4.

A direct inspection reveals that $\mathtt{F}\llbracket\Phi_{0}\rrbracket$ is
indeed a finite geometric formula when $\Phi_{0}$ is from the first layer.
Similarly, the geometric theory $\mathtt{T}\llbracket\Phi_{2}\rrbracket$
contains only countably-many sequents when $\Phi_{2}\in G_{\delta}$.

######  Remark 4.5.

Recall that $\mathsf{LTL}$ formulae $\Phi,\Psi$ are _equivalent_ , notation
$\Phi\equiv\Psi$, when $\llbracket\Phi\rrbracket=\llbracket\Psi\rrbracket$.
The following standard equivalences are obtained similarly as in [BK08,
§5.1.4].

$\begin{array}[]{l !{\equiv} l !{\qquad} l !{\equiv} l !{\qquad} l !{\equiv}
l}\bigcirc\mathsf{False}&\mathsf{False}\par&\bigcirc(\Phi\lor\Psi)&\bigcirc\Phi\lor\bigcirc\Psi\par&\bigcirc(\Phi\mathrel{\mathsf{U}}\Psi)&(\bigcirc\Phi)\mathrel{\mathsf{U}}(\bigcirc\Psi)\\\
\bigcirc\mathsf{True}&\mathsf{True}\par&\bigcirc(\Phi\land\Psi)&\bigcirc\Phi\land\bigcirc\Psi\par&\bigcirc(\Phi\mathrel{\mathsf{W}}\Psi)&(\bigcirc\Phi)\mathrel{\mathsf{W}}(\bigcirc\Psi)\end{array}$

Hence, up to equivalence, we can push the $\bigcirc$’s to atoms $a\in A$. In
particular, we may assume that $\bigcirc$ occurs only in first layer’s
formulae of the form $\bigcirc^{n}a$.

Let $\Phi_{0}$ be an $\mathsf{LTL}$ formula from the first layer in Figure 1.
Up to equivalence (Remark 4.5), we can assume that $\Phi_{0}$ is in
disjunctive normal form, and actually that $\Phi_{0}$ is a disjunction of
conjunctions of formulae of the form $\bigcirc^{n}a$. Then
$\mathtt{F}\llbracket\Phi_{0}\rrbracket$ is simply a disjunction of
conjunctions of atomic propositions of the form $(\bot^{n}\cdot
a\cdot\bot^{\omega})\in\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$.

Consider the formula $\Phi_{1}\coloneqq\diamondsuit\Phi_{0}\in G$. Recall that
$\diamondsuit\Phi_{0}=(\mathsf{True}\mathrel{\mathsf{U}}\Phi_{0})$, and note
that
$\mathtt{H}_{\mathtt{true},\varphi}(\theta)=\varphi\lor(\mathtt{true}\land\bigcirc\theta)$.
Up to the replacement of $\mathtt{true}\land\bigcirc\theta$ by
$\bigcirc\theta$, we get that $\mathtt{F}\llbracket\Phi_{1}\rrbracket$ is the
geometric formula
$\bigvee_{m\in\mathbb{N}}\left(\mathtt{F}\llbracket\Phi_{0}\rrbracket\lor\bigcirc\mathtt{F}\llbracket\Phi_{0}\rrbracket\lor\dots\lor\bigcirc^{m}\mathtt{F}\llbracket\Phi_{0}\rrbracket\right)$.
This mirrors the formulation of Lemma 4.3.1(2) in Example 4.3.1.

We turn to the formula $\Phi_{2}\coloneqq\square\diamondsuit\Phi_{0}\in
G_{\delta}$. We have
$\square\Phi_{1}=(\Phi_{1}\mathrel{\mathsf{W}}\mathsf{False})$ and we simplify
$\mathtt{H}_{\varphi,\mathtt{false}}(\theta)$ to $\varphi\land\bigcirc\theta$.
The theory $\mathtt{T}\llbracket\Phi_{2}\rrbracket$ then consists of all the
following sequents

$\begin{array}[]{l l}\vdash&\bigwedge_{n\leq
N}\bigvee_{m\in\mathbb{N}}\bigcirc^{n}\mathtt{F}\llbracket\Phi_{0}\rrbracket\lor\bigcirc^{n+1}\mathtt{F}\llbracket\Phi_{0}\rrbracket\lor\dots\lor\bigcirc^{n+m}\mathtt{F}\llbracket\Phi_{0}\rrbracket\end{array}$

where $N$ ranges over $\mathbb{N}$. This mirrors the fact that
$\llbracket\square\diamondsuit\Phi_{0}\rrbracket$ is the set of those streams
$x\in\llbracket\mathsf{Str}A\rrbracket$ such that for each $n\in\mathbb{N}$,
there is some $m\in\mathbb{N}$ with
$x\mathord{\upharpoonright}(n+m)\in\llbracket\Phi_{0}\rrbracket$.

Continuing Example 4.3.1, we now consider the case of
$\Phi_{3}\coloneqq\diamondsuit\square a$ with $a\in A$. For this more involved
example, we allow ourselves some simplifications that we deliberately avoided
in Example 4.3.1. Namely, for $\mathtt{T}\llbracket\square\Phi\rrbracket$ and
$\mathtt{T}\llbracket\diamondsuit\Psi\rrbracket$ we take respectively
$\bigcurlywedge_{n\in\mathbb{N}}\bigcirc^{n}\mathtt{T}\llbracket\Phi\rrbracket$
and
$\bigcurlyvee_{m\in\mathbb{N}}\bigcirc^{m}\mathtt{T}\llbracket\Psi\rrbracket$.
Then we have

$\begin{array}[]{r c l}\mathtt{T}\llbracket\square
a\rrbracket&=&\left\\{\bigcirc^{n}\mathtt{F}\llbracket a\rrbracket\mid
n\in\mathbb{N}\right\\}\\\ \mathtt{T}\llbracket\diamondsuit\square
a\rrbracket&=&\left\\{\bigvee_{m\in\mathbb{N}}\bigcirc^{m+f(m)}\mathtt{F}\llbracket
a\rrbracket\mid f\colon\mathbb{N}\to\mathbb{N}\right\\}\end{array}$

The uncountable theory $\mathtt{T}\llbracket\diamondsuit\square a\rrbracket$
relies on the (classical) choice principle behind Proposition 6. It expresses
that given a stream $x\in\llbracket\mathsf{Str}A\rrbracket$, we have
$x\notin\llbracket\diamondsuit\square a\rrbracket$ if, and only if, there
exists a function $f\colon\mathbb{N}\to\mathbb{N}$ such that $x(m+f(m))\neq a$
for all $m\in\mathbb{N}$. In particular, if
$x\notin\llbracket\diamondsuit\square a\rrbracket$, then the function $g\colon
m\mapsto m+f(m)$ finds arbitrary large $n=g(m)$ such that $x(n)\neq a$.

By Theorem 4.3.1 and Proposition 5, the subspace of
$\llbracket\mathsf{Str}A\rrbracket$ induced by a negation-free $\mathsf{LTL}$
formula $\Phi$ is homeomorphic to the space of models
$\mathbf{Mod}_{\llbracket\mathsf{Str}A\rrbracket}(\mathtt{T}\llbracket\Phi\rrbracket)$.
Moreover, it follows from Theorem 4.2 that we can use
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}_{\llbracket\mathsf{Str}A\rrbracket}(\mathtt{T}\llbracket\Phi\rrbracket)$
to represent the quotient frame
$\Omega(\llbracket\mathsf{Str}A\rrbracket)\twoheadrightarrow\Omega(\llbracket\mathsf{Str}A\rrbracket)\mathord{\upharpoonright}\llbracket\Phi\rrbracket$
(cf. §3.3). Hence,
$\mathbf{Mod}_{\llbracket\mathsf{Str}A\rrbracket}(\mathtt{T}\llbracket\Phi\rrbracket)$
yields a topological notion of approximation for the subspace
$\llbracket\Phi\rrbracket$, which, in view of Examples 4.3.1 and 4.3.1,
explicitly represents the semantics of $\Phi$.

However, a limitation of this approach is that the frame
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}_{\llbracket\mathsf{Str}A\rrbracket}(\mathtt{T}\llbracket\Phi\rrbracket)$
is defined by purely semantic means. fullBefore discussing this, we comment on
potential extensions to $\mathsf{LTL}$ with negation.shortWe discuss this in
[rs23full, §A] (which gives an important role to the $G_{\delta}$ case). We
now comment on potential extensions to $\mathsf{LTL}$ with negation.longWe
discuss this in §A (which gives an important role to the $G_{\delta}$ case).
We now comment on potential extensions to $\mathsf{LTL}$ with negation.

######  Remark 4.6.

Say that an $\mathsf{LTL}$ formula $\Phi$ is an _$F$ formula_ if $\Phi$ is the
negation of a $G$ formula. The _$F_{\sigma}$_ formulae are the negations of
the $G_{\delta}$ ones. For instance, $\lnot a$ (with $a\in A$) is a simple
non-trivial $F$ formula, while $\lnot\square a\equiv\diamondsuit\lnot a$ is an
$F_{\sigma}$ formula. It follows from Remark 4.3 that $F$ formulae induce
Scott-_closed_ subsets of $\llbracket\mathsf{Str}A\rrbracket$, and that the
$F_{\sigma}$ ones induce countable unions of Scott-closed sets (i.e.
$F_{\sigma}$ sets).

Now, if $\Phi=\lnot\Phi_{1}$ with $\Phi_{1}\in G$, then the subspace
$\llbracket\Phi\rrbracket$ is represented by the geometric theory
$\\{\mathtt{F}\llbracket\Phi_{1}\rrbracket\vdash\mathtt{false}\\}$. Hence
Theorem 4.3.1 extends to $F$ formulae (so that Proposition 5 and Theorem 4.2
can be applied in this case). But beware that this does not hold in general
for $F_{\sigma}$-formulae, since the subspace $\llbracket\lnot\square
a\rrbracket=\llbracket\diamondsuit\lnot a\rrbracket$ is not representable in
geometric logic (in the sense of Example 4.2). In particular, there is no
geometric theory $\mathtt{T}$ such that
$\mathbf{Mod}(\mathtt{T})=\bigcup_{m\in\mathbb{N}}\mathbf{Mod}\\{\bigcirc^{m}\mathtt{F}\llbracket
a\rrbracket\vdash\mathtt{false}\\}$, and Proposition 6 does not extend to
infinitely many arbitrary theories.

full

##  5 Free Frames and Spatiality

Our approach to geometric logic in §4 focuses on _spaces_ of _models_.
However, the literature rather considers geometric logic as a formal way to
present frames by _generators and relations_. A customary tool for this is the
notion of _congruence preorder_ (see [Vic89, §4 and §6.1–2] and [Hec15, §3]).
It is folklore that congruence preorders can be presented using an
(infinitary) deduction system for geometric logic (in the spirit of e.g.
[Vic07, §2.2] and [Joh02, D1.1.7(m) and §D1.3]).

$\begin{array}[]{c}(\textsc{Th})\leavevmode\nobreak\
\dfrac{}{\varphi\vdash_{\mathtt{T}}\psi}\leavevmode\nobreak\ \text{(if
$(\varphi\vdash\psi)\in\mathtt{T}$)}\par\qquad\quad\par(\textsc{Ax})\leavevmode\nobreak\
\dfrac{}{\varphi\vdash_{\mathtt{T}}\varphi}\par\qquad\quad\par(\textsc{Cut})\leavevmode\nobreak\
\dfrac{\varphi\vdash_{\mathtt{T}}\theta\qquad\theta\vdash_{\mathtt{T}}\psi}{\varphi\vdash_{\mathtt{T}}\psi}\par\\\
\\\ (\textsc{$\land$-L${}_{1}$})\leavevmode\nobreak\
\dfrac{}{\varphi\land\psi\vdash_{\mathtt{T}}\varphi}\par\qquad\qquad\par(\textsc{$\land$-L${}_{2}$})\leavevmode\nobreak\
\dfrac{}{\varphi\land\psi\vdash_{\mathtt{T}}\psi}\par\qquad\qquad\par\par(\textsc{$\land$-R})\leavevmode\nobreak\
\dfrac{\theta\vdash_{\mathtt{T}}\varphi\qquad\theta\vdash_{\mathtt{T}}\psi}{\theta\vdash_{\mathtt{T}}\varphi\land\psi}\par\\\
\\\ (\textsc{$\mathtt{true}$-R})\leavevmode\nobreak\
\dfrac{}{\varphi\vdash_{\mathtt{T}}\mathtt{true}}\par\qquad\quad\par(\textsc{$\bigvee$-L})\leavevmode\nobreak\
\dfrac{\text{for all $i\in I$,
$\varphi_{i}\vdash_{\mathtt{T}}\psi$}}{\bigvee_{i\in
I}\varphi_{i}\vdash_{\mathtt{T}}\psi}\par\qquad\quad\par(\textsc{$\bigvee$-R})\leavevmode\nobreak\
\dfrac{}{\varphi_{i}\vdash_{\mathtt{T}}\bigvee_{i\in
I}\varphi_{i}}\par\end{array}$ Figure 2: Deduction rules for geometric logic
over a theory $\mathtt{T}$.

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. The _deduction
relation_ $\vdash_{\mathtt{T}}$ on $\mathtt{Geom}(\mathit{At})$ is defined by
the rules in Figure 3, using the constructs of Remark 4.1. The relation
$\vdash_{\mathtt{T}}$ is a preorder. Similarly as in §4.2, we quotient
$\mathtt{Geom}(\mathit{At})$ under the relation $\sim_{\mathtt{T}}$ of
_$\mathtt{T}$ -equivalence_ defined as $\varphi\sim_{\mathtt{T}}\psi$ iff
$\varphi\vdash_{\mathtt{T}}\psi$ and $\psi\vdash_{\mathtt{T}}\varphi$. We
write $[\varphi]_{\mathtt{T}}$ for the $\sim_{\mathtt{T}}$-class of $\varphi$
and $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ for the set of
$\sim_{\mathtt{T}}$-classes. We let $\leq_{\mathtt{T}}$ be the partial order
on $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ induced by $\vdash_{\mathtt{T}}$.
In contrast with [Joh02, §D1.3 and D1.4.14] (see also [Vic07, §2.2]), we do
not need to enforce frame distributivity in Figure 3, since it is hardwired in
the constructs of Remark 4.1.

$(\mathtt{Geom}(\mathit{At})/\mathtt{T},\leq_{\mathtt{T}})$ is a frame.

##### Spatiality.

How does $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ relate to the frame
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$ of §4.2? To answer this
question, we compare the preorders $\vdash_{\mathtt{T}}$ and
$\preceq_{\mathbf{Mod}(\mathtt{T})}$. First, an easy induction on derivations
proves the following _soundness_ property:

$\begin{array}[]{l l
l}\psi\vdash_{\mathtt{T}}\varphi&\Longrightarrow&\psi\preceq_{\mathbf{Mod}(\mathtt{T})}\varphi\end{array}$

The converse implication is a form of _completeness_ : if every model of
$\mathtt{T}$ is a model of the sequent $\psi\vdash\varphi$, then
$\psi\vdash_{\mathtt{T}}\varphi$ is derivable. This may fail in geometric
logic, by lack of spatiality. A frame $L$ is said to be _spatial_ if given
$a\not\leq b$ in $L$, there is a point $\mathcal{F}\in\mathrm{pt}(L)$ such
that $a\in\mathcal{F}$ and $b\notin\mathcal{F}$. A frame is spatial precisely
when it is isomorphic to $\Omega(X)$ for some space $X$, but not every frame
is spatial ([Joh82, §II.1.5]).

Assume now that $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial, and let
$\psi\not\vdash_{\mathtt{T}}\varphi$. Hence
$[\psi]_{\mathtt{T}}\not\leq_{\mathtt{T}}[\varphi]_{\mathtt{T}}$ and there is
a point $\mathcal{F}$ of $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ such that
$[\psi]_{\mathtt{T}}\in\mathcal{F}$ and
$[\varphi]_{\mathtt{T}}\notin\mathcal{F}$. Let
$\nu\colon\mathit{At}\to\mathbf{2}$ take $p\in\mathit{At}$ to $1$ iff
$[p]_{\mathtt{T}}\in\mathcal{F}$.

Let $\mathcal{F}$ and $\nu$ as above. Then for every
$\theta\in\mathtt{Geom}(\mathit{At})$, we have $\nu\models\theta$ if, and only
if, $[\theta]_{\mathtt{T}}\in\mathcal{F}$. In particular, $\nu$ is a model of
$\mathtt{T}$ with $\nu\models\psi$ and $\nu\not\models\varphi$.

Hence, when $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial, the preorders
$\vdash_{\mathtt{T}}$ and $\preceq_{\mathbf{Mod}(\mathtt{T})}$ coincide, and
$\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is thus isomorphic to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$. Since
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$ is always isomorphic to
the frame of opens of the space $\mathbf{Mod}(\mathtt{T})$ (Theorem 4.2), we
have the following.

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. Then the following
are equivalent.

  1. (i)

The frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial.

  2. (ii)

Deduction in $\vdash_{\mathtt{T}}$ is complete
($\psi\vdash_{\mathtt{T}}\varphi$ if, and only if,
$\psi\preceq_{\mathbf{Mod}(\mathtt{T})}\varphi$).

  3. (iii)

The frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is isomorphic to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$.

##### Free Frames and Congruence Preorders.

In view of Theorem A, it is interesting to know whether a frame
$\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial. We discuss this using the
following notions. Write $\mathtt{E}$ for the empty theory.

Let $\mathbf{U}\colon\mathbf{Frm}\to\mathbf{Set}$ be the forgetful functor. A
_free frame_ on $\mathit{At}$ is the data of a frame $L(\mathit{At})$ and of a
function $\eta_{\mathit{At}}\colon\mathit{At}\to\mathbf{U}L(\mathit{At})$ such
that for each frame $L$ and each function $f\colon\mathit{At}\to\mathbf{U}L$,
there is a unique frame morphism ${f}^{\star}\colon L(\mathit{At})\to L$
making the following diagram to commute.

${\mathit{At}}$${\mathbf{U}L}$${\mathbf{U}L(\mathit{At})}$$\scriptstyle{f}$$\scriptstyle{\eta_{\mathit{At}}}$$\scriptstyle{\mathbf{U}{f}^{\star}}$

######  Proposition 7.

$(\mathtt{Geom}(\mathit{At})/\mathtt{E},\leq_{\mathtt{E}})$ (with the function
$p\in\mathit{At}\mapsto[p]_{\mathtt{T}}$) is a free frame on $\mathit{At}$.

The operation $\mathit{At}\mapsto\mathtt{Geom}(\mathit{At})/\mathtt{E}$ thus
yields a left adjoint to $\mathbf{U}\colon\mathbf{Frm}\to\mathbf{Set}$ (see
e.g. [ML98, Theorem IV.1.2]). Actually, the set of Scott-opens of the cpo
$\mathcal{P}(\mathit{At})$ is also a free frame on $\mathit{At}$. See [Joh82,
Lemma VII.4.9] (see also [Hec15, Theorem 3.1] and [Joh02, C1.1.4 and C4.1.6]).
Since free frames are unique up to isomorphism, it follows that the frame
$\mathtt{Geom}(\mathit{At})/\mathtt{E}$ is spatial.

It is customary to present a frame by quotienting a free frame under a
congruence preorder. We refer to [Hec15, §3.4]. A _congruence preorder_ on a
frame $(L,\leq)$ is a preorder $\preceq$ on $L$ such that
${\leq}\subseteq{\preceq}$ and such that for each arbitrary (resp. finite)
$S\subseteq L$, we have $\bigvee S\preceq b$ whenever $a\preceq b$ for all
$a\in S$ (resp. $b\preceq\bigwedge S$ whenever $b\preceq a$ for all $a\in S$).
Given a congruence preorder $\preceq$ on $L$, let $a\sim b$ iff $a\preceq b$
and $b\preceq a$.

Each binary relation $R$ on $L$ is contained in a least congruence preorder
$\overline{R}$ on $L$.

######  Proposition 8.

Given geometric theories $\mathtt{T},\mathtt{U}$ over $\mathit{At}$, let
$R\coloneqq\\{([\varphi]_{\mathtt{T}},[\psi]_{\mathtt{T}})\mid(\varphi\vdash\psi)\in\mathtt{T}\cup\mathtt{U}\\}$.
Then $\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U})$ is isomorphic to
the quotient of $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ by
$\sim_{\overline{R}}$.

In particular, $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is isomorphic to the
quotient of the free frame $\mathtt{Geom}(\mathit{At})/\mathtt{E}$ under
$\sim_{\overline{R}}$, where
$R=\\{([\varphi]_{\mathtt{E}},[\psi]_{\mathtt{E}})\mid(\varphi\vdash\psi)\in\mathtt{T}\\}$.

[[Joh02, D1.1.7(m) and D1.4.14]] Each frame $(L,\leq_{L})$ is isomorphic to
the frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}(L)$, where $\mathtt{T}(L)$ is
the following theory over $\mathit{At}\coloneqq\\{\underline{a}\mid a\in
L\\}$.

$\begin{array}[]{r !{\thesis} l @{\quad} l !{\qquad} r !{\thesis}
l}\underline{a}\lx@intercol\vdash&\underline{b}&\text{(if
$a\leq_{L}b$)}\par&\lx@intercol\vdash&\underline{\top_{L}}\\\
\underline{\bigvee_{L}S}\lx@intercol\vdash&\bigvee\left\\{\underline{a}\mid
a\in S\right\\}&\text{(if $S\subseteq
L$)}\par&\underline{a}\land\underline{b}\lx@intercol\vdash&\underline{a\land_{L}b}\par\end{array}$

Hence, any frame is a quotient of a free frame by a geometric theory. It then
follows from [Joh82, §II.1.5] that $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ may
not be spatial. On the positive side, we have

[[Hec15, Corollary 3.15]] Let $R$ be a _countable_ binary relation on a free
frame $L(\mathit{At})$. Then the quotient of $L(\mathit{At})$ under
$\sim_{\overline{R}}$ is a spatial frame.

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. If $\mathtt{T}$ is
countable, then the frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial.
In particular, if $\Phi$ is a $G_{\delta}$ formula of $\mathsf{LTL}(A)$, then
$\mathtt{Geom}(\mathit{At})/\mathtt{T}\llbracket\Phi\rrbracket$ is spatial,
where $\mathit{At}=\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$.

Hence, when $\Phi$ is a $G_{\delta}$ formula of $\mathsf{LTL}$, deduction in
$\vdash_{\mathtt{T}\llbracket\Phi\rrbracket}$ completely axiomatizes
$\mathbf{Mod}(\mathtt{T}\llbracket\Psi\rrbracket)$, and the frame
$\mathtt{Geom}(\mathit{At})/\mathtt{T}\llbracket\Phi\rrbracket$ is isomorphic
to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T}\llbracket\Phi\rrbracket)$.

We must warn the reader on the following subtle points, which actually
motivate the explicit constructions of §4.3.1.

######  Remark 5.1.

Consider a space $(X,\Omega)$. It follows from Example 10 that there is a
theory $\mathtt{T}_{\Omega}$ over
$\mathit{At}_{\Omega}\coloneqq\\{\underline{U}\mid U\in\Omega\\}$ such that
$\Omega$ is isomorphic to
$\mathtt{Geom}(\mathit{At}_{\Omega})/\mathtt{T}_{\Omega}$ (so that
$\mathtt{Geom}(\mathit{At}_{\Omega})/\mathtt{T}_{\Omega}$ is spatial). But
beware that when $X$ is an algebraic dcpo, the theory
$\mathtt{T}\coloneqq\mathtt{T}(X)$ of §4.1 is over the set of atomic
propositions $\mathit{At}\coloneqq\mathrm{Fin}(X)$, which differs from
$\mathit{At}_{\Omega}$. In particular, the theories $\mathtt{T}$ and
$\mathtt{T}_{\Omega}$ differ, and there is _a priori_ no reason for $\Omega$
to be isomorphic to $\mathtt{Geom}(\mathit{At})/\mathtt{T}$.

An algebraic dcpo $X$ is said to be _$\omega$ -algebraic_ when
$\mathrm{Fin}(X)$ is (at most) countable. For instance,
$\llbracket\mathsf{Str}A\rrbracket$ is $\omega$-algebraic precisely when $A$
is (at most) countable.

Assume $X$ is $\omega$-algebraic. Set $\mathit{At}\coloneqq\mathrm{Fin}(X)$
and $\mathtt{T}\coloneqq\mathtt{T}(X)$ as above. The theory $\mathtt{T}$ is
countable, and Corollary A applies. Hence, the frame
$\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial and thus isomorphic to the
frame $\Omega$ (Theorem A, Theorem 4.2 and Proposition 4).

Consider now a subset $P\subseteq X$. Recall from §3.3 that the quotient frame
$\Omega\twoheadrightarrow\Omega\mathord{\upharpoonright}P$ can be represented
as the frame of $j$-fixpoints for a nucleus $j$ on $\Omega$. It is then a
consequence of Proposition 10 and [Hec15, §3.4] that the frame
$\Omega\mathord{\upharpoonright}P$ is isomorphic to
$\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U})$, where

$\begin{array}[]{l l
l}\mathtt{U}&\coloneqq&\left\\{\varphi\vdash\psi\mid[\varphi]_{\mathtt{T}}\leq_{\mathtt{T}}j([\psi]_{\mathtt{T}})\right\\}\end{array}$

In particular, the frame
$\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U})$ spatial and thus
isomorphic to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$. But beware
that this does _not_ imply that the _space_
$(P,\Omega\mathord{\upharpoonright}P)$ is represented by the space of models
$\mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$, unless
$(P,\Omega\mathord{\upharpoonright}P)$ is sober, since in this case we have

$(P,\Omega\mathord{\upharpoonright}P)\leavevmode\nobreak\
\cong\leavevmode\nobreak\
\mathrm{pt}(\Omega\mathord{\upharpoonright}P)\leavevmode\nobreak\
\cong\leavevmode\nobreak\
\mathrm{pt}(\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U}))\leavevmode\nobreak\
\cong\leavevmode\nobreak\
\mathrm{pt}(\mathtt{Geom}(\mathit{At})/\mathbf{Mod}_{\mathtt{T}}(\mathtt{U}))\leavevmode\nobreak\
\cong\leavevmode\nobreak\ \mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$

In the case of streams $\llbracket\mathsf{Str}A\rrbracket$ (with $A$
countable), it follows that for _any_
$P\subseteq\llbracket\mathsf{Str}A\rrbracket$ there is a geometric theory
$\mathtt{U}$ on $\mathit{At}$ which represents the _frame_
$\Omega\mathord{\upharpoonright}P$. For instance, with
$P\coloneqq\llbracket\lnot\square a\rrbracket$, the isomorphism
$\Omega\mathord{\upharpoonright}P\cong\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U})$
lifts to homeomorphisms

$\mathrm{pt}(\Omega\mathord{\upharpoonright}P)\leavevmode\nobreak\
\cong\leavevmode\nobreak\
\mathrm{pt}(\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U}))\leavevmode\nobreak\
\cong\leavevmode\nobreak\
\mathrm{pt}(\mathtt{Geom}(\mathit{At})/\mathbf{Mod}_{\mathtt{T}}(\mathtt{U}))\leavevmode\nobreak\
\cong\leavevmode\nobreak\ \mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$

But we have
$(P,\Omega\mathord{\upharpoonright}P)\not\cong\mathbf{Mod}_{\mathtt{T}}(\mathtt{U})$
since
$(P,\Omega\mathord{\upharpoonright}P)\not\cong\mathrm{pt}(\Omega\mathord{\upharpoonright}P)$
as $(P,\Omega\mathord{\upharpoonright}P)$ is not sober (Corollary 3.3).

##  6 A Specification for the Denotation of Filter

The core of this paper consists of the results presented above concerning
$\mathsf{LTL}$ on streams. However, the long term goal of this work is to
reason on input-output (negation-free) $\mathsf{LTL}$ properties of functions.
We now briefly sketch how our results can help to handle our motivating
example, namely the $\mathsf{filter}$ function on streams. This is mostly
preliminary; we leave as future work the elaboration of a general solution.

We work with the function $\llbracket\mathsf{filter}\rrbracket$ of Remark 2.2.
Fix a finite set $A$ and a Scott-continuous function $p\colon\llbracket
A\rrbracket\to\llbracket\mathsf{Bool}\rrbracket$. Assume that for all $a\in
A$, we have $p(a)\neq\bot_{\llbracket\mathsf{Bool}\rrbracket}$. Let
$\Psi=\Psi_{p}$ as in Example 2.2 and set $\Phi\coloneqq\bigvee_{a\in A}a$.
The specification (1) for $\mathsf{filter}$ leads to the following
specification for $\llbracket\mathsf{filter}\rrbracket$:

$\forall x\in\llbracket\mathsf{Str}A\rrbracket,\leavevmode\nobreak\ \text{$x$
total},\qquad
x\Vdash\square\diamondsuit\Psi\quad\Longrightarrow\quad(\llbracket\mathsf{filter}\rrbracket\
p\ x)\Vdash\square\Phi$ (2)

where we refrained from writing $x\Vdash\square\Phi$ for the assumption that
$x$ is total.

We use the notations of Remark 2.2. In particular,
$\llbracket\mathsf{filter}\rrbracket p$ is the least fixpoint of the Scott-
continuous function $f_{p}\colon X\to X$, where
$X\coloneqq\mathbf{CPO}[\llbracket\mathsf{Str}A\rrbracket,\llbracket\mathsf{Str}A\rrbracket]$.
In symbols, we have $\llbracket\mathsf{filter}\rrbracket
p=\mathsf{Y}(f_{p})=\bigvee_{n\in\mathbb{N}}f_{p}^{n}(\bot_{X})$.

The standard method to reason on such fixpoints is the rule of _fixpoint
induction_ (see e.g. [AC98, §6.2]). This rule asserts that given a subset $S$
of a cpo $X$, and a morphism $f\colon X\to_{\mathbf{CPO}}X$, we have
$\mathsf{Y}(f)\in S$ provided (i) $\bot_{X}\in S$, (ii) $S$ is stable under
sups of $\omega$-chains, and (iii) $f(x)\in S$ whenever $x\in S$. In our case,
the subset of interest is $S\coloneqq\left\\{f\mid\text{$x$ total and
$x\Vdash\square\diamondsuit\Psi$}\leavevmode\nobreak\
\Rightarrow\leavevmode\nobreak\ f(x)\Vdash\square\Phi\right\\}$. But fixpoint
induction cannot be applied since $\bot_{X}\notin S$ (as $\bot_{X}$ takes any
$x\in\llbracket\mathsf{Str}A\rrbracket$ to
$\bot^{\omega}\not\Vdash\square\Phi$).

We can proceed as follows, with the help of §4.3.1. Given $k,n\in\mathbb{N}$
with $k\leq n$, let

$\begin{array}[]{r c l}\psi_{n,k}&\coloneqq&\bigvee\left\\{\bigwedge_{1\leq
j\leq k}\bigcirc^{i_{j}}\mathtt{F}\llbracket\Psi\rrbracket\mid 0\leq
i_{1}<\dots<i_{k}<n\right\\}\\\
\varphi_{k}&\coloneqq&\bigwedge_{m<k}\bigcirc^{m}\mathtt{F}\llbracket\Phi\rrbracket\end{array}$

Note that
$\nu(x)\in\mathbf{Mod}\left(\mathtt{T}\llbracket\square\diamondsuit\Psi\rrbracket\right)$
if, and only if, $(\forall k\in\mathbb{N})(\exists n\geq
k)(\nu(x)\models\psi_{n,k})$. It follows that condition (2) can be obtained
from the following.

$\forall x\in\llbracket\mathsf{Str}A\rrbracket,\leavevmode\nobreak\ \text{$x$
total},\leavevmode\nobreak\ \forall k\in\mathbb{N},\leavevmode\nobreak\
\forall n\geq
k,\quad\nu(x)\models\psi_{n,k}\quad\Longrightarrow\quad\nu(\llbracket\mathsf{filter}\rrbracket\
p\ x)\models\varphi_{k}$ (3)

Condition (3) is a consequence of Lemma 6 below. The main inductive argument
is encapsulated in item (1).

Write $g_{n}$ for
$f_{p}^{n}(\bot_{X})\colon\llbracket\mathsf{Str}A\rrbracket\to_{\mathbf{CPO}}\llbracket\mathsf{Str}A\rrbracket$.
Let $x\in\llbracket\mathsf{Str}A\rrbracket$ be a total stream.

  1. (1)

Assume $k\leq n$. If $\nu(x)\models\psi_{n,k}$, then
$\nu(g_{n}(x))\models\varphi_{k}$.

  2. (2)

Let $n,k\in\mathbb{N}$. If $\nu(g_{n}(x))\models\varphi_{k}$, then
$\nu(\llbracket\mathsf{filter}\rrbracket\ p\ x)\models\varphi_{k}$.

##  7 Conclusion

In this paper, we conducted a semantic study of a logic $\mathsf{LTL}$ on a
domain of streams $\llbracket\mathsf{Str}A\rrbracket$. We showed that the
negation-free formulae of $\mathsf{LTL}$ induce sober subspaces of
$\llbracket\mathsf{Str}A\rrbracket$, and that this may fail in presence of
negation. We proposed an inductive translation of negation-free $\mathsf{LTL}$
to geometric logic. This translation reflects the semantics of $\mathsf{LTL}$,
and we use it to prove that the denotation of $\mathsf{filter}$ satisfies the
specification (1).

##### Further Works.

First, the logic $\mathsf{LTL}$ on $\llbracket\mathsf{Str}A\rrbracket$
deserves further studies, in particular regarding decidability and possible
axiomatizations.

short long

We think an important next step would be to propose a refinement type system
in the spirit of [JR21], but for an extension of $\mathrm{PCF}$ with streams.
More precisely, the system of [JR21] crucially relies on controlled unfoldings
of (formula level) fixpoints. We think that our translation to geometric logic
could provide a domain-theoretic analogue for that, yielding a system grounded
on DTLF (in the form of [Abr91, §4.3] or e.g. [AC98, §10.5]). This may rely on
a deduction system for either $\mathsf{LTL}$ or geometric
logic.short,long111111Actually, each $T_{1}$ space is $T_{D}$ ([PP11,
§I.2.1]). In any case, we expect to need an analogue of the iteration terms of
[JR21], which actually could simulate (enough of) the infinitary aspects of
geometric logic. Also, an important task in this direction would be to
formulate sufficiently general reasoning principles for program-level
fixpoints.

Further, we expect to handle alternation-free modal $\mu$-properties121212This
corresponds to “alternation depth $1$” in [BW18, §2.2]. See also [BS07, §7]
and [SV10]. on (finitary) polynomial types, thus targeting a system which as a
whole would be based on $\mathrm{FPC}$. But polynomial types involve sums, and
sums are not universal in $\mathbf{CPO}$, in contrast with $\mathbf{DCPO}$ and
with the category $\mathbf{CPO}_{\bot}$ of _strict_ functions. We think of
working with Call-By-Push-Value (CBPV) [Lev03, Lev22] for the usual adjunction
between $\mathbf{DCPO}$ and $\mathbf{CPO}_{\bot}$. On the long run, it would
be nice if this basis could extend to enriched models of CBPV, so as to handle
further computational effects. Print and global store are particularly
relevant, as an important trend in proving temporal properties considers
programs generating streams of events. Major works in this line include
[SSVH08, HC14, HL17, NUKT18, KT14, UST18, NUKT18, SU23]. In contrast with
ours, these approaches are based on trace semantics of syntactic expressions
rather than denotational domains.131313See e.g. [NUKT18, Theorem 4.1 (and
Figure 6)] or [SU23, Theorem 1 (and Definition 20 from the full version)].

In a different direction, we think our approach based on geometric logic could
extend to linear types [HJK00], for instance targeting systems like [NG03,
Win04], and relying on the categorical study of [BF06].

##### Acknowledgements.

This work was partially supported by the ANR-14-CE25-0007 - RAPIDO and by the
LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon. It started as a spin-
off of ongoing work with Guilhem Jaber and Kenji Maillard. G. Jaber proposed
the $\mathsf{filter}$ function as a motivating example. full,longThomas
Streicher pointed to us the reference [Hec15].shortThomas Streicher pointed to
us the reference [Hec15] (see [rs23full, §A]).

## References

  * [Abr91] S. Abramsky :  Domain Theory in Logical Form.  Ann. Pure Appl. Log., 51(1-2):1–77, 1991\.
  * [AC98] R. M. Amadio et P.-L. Curien :  Domains and Lambda-Calculi.  Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1998.
  * [BBT20] T.-D. Bradley, T. Bryson et J. Terilla :  Topology: A Categorical Approach.  The MIT Press, Cambridge (Mass.) London, 2020.
  * [BF06] M. Bunge et J. Funk :  Singular Coverings of Toposes.  Lecture Notes in Mathematics. Springer Berlin Heidelberg, 2006.
  * [BK08] C. Baier et J.-P. Katoen :  Principles of Model Checking.  The MIT Press, 2008.
  * [BS07] J. Bradfield et C. Stirling :  Modal Mu-Calculi.  _In_ P. Blackburn, J. Van Benthem et F. Wolter, éditeurs : Handbook of Modal Logic, volume 3 de Studies in Logic and Practical Reasoning, pages 721–756. Elsevier, 2007.
  * [BW18] J. C. Bradfield et I. Walukiewicz :  The mu-calculus and Model Checking.  _In_ E. M. Clarke, T. A. Henzinger, H. Veith et R. Bloem, éditeurs : Handbook of Model Checking, pages 871–919. Springer, 2018.
  * [CZ00] T. Coquand et G.-Q. Zhang :  Sequents, Frames, and Completeness.  _In_ Proceedings of the 14th Annual Conference of the EACSL on Computer Science Logic, pages 277–291, London, UK, UK, 2000. Springer-Verlag.
  * [DL22] I. Di Liberti :  General Facts on the Scott Adjunction.  Applied Categorical Structures, 30:569–591, 2022.
  * [DP02] B.A. Davey et H.A. Priestley :  Introduction to Lattices and Order.  Cambridge University Press, 2nd édition, 2002.
  * [DST19] M. Dickmann, N. Schwartz et M. Tressl :  Spectral Spaces.  New Mathematical Monographs. Cambridge University Press, Cambirdge, 2019\.
  * [GL13] J. Goubault-Larrecq :  Non-Hausdorff Topology and Domain Theory: Selected Topics in Point-Set Topology.  New Mathematical Monographs. Cambridge University Press, Cambridge, 2013\.
  * [GvG23] M Gehrke et S. van Gool :  Topological duality for distributive lattices: Theory and applications, 2023.  To appear in the book series Cambridge Tracts in Theoretical Computer Science, Cambridge University Press. Available on arXiv (2203.03286).
  * [HC14] M. Hofmann et W. Chen :  Abstract interpretation from büchi automata.  _In_ T. A. Henzinger et D. Miller, éditeurs : Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014, pages 51:1–51:10. ACM, 2014.
  * [Hec15] R. Heckmann :  Spatiality of countably presentable locales (proved with the Baire category theorem).  Mathematical Structures in Computer Science, 25(7):1607–1625, 2015.
  * [HJK00] M. Huth, A. Jung et K. Keimel :  Linear types and approximation.  Mathematical Structures in Computer Science, 10(6):719–745, 2000.
  * [HL17] M. Hofmann et J. Ledent :  A cartesian-closed category for higher-order model checking.  _In_ 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017, pages 1–12. IEEE Computer Society, 2017.
  * [HR07] I. Hodkinson et M. Reynolds :  Temporal Logic.  _In_ P. Blackburn, J. Van Benthem et F. Wolter, éditeurs : Handbook of Modal Logic, volume 3 de Studies in Logic and Practical Reasoning, pages 655–720. Elsevier, 2007.
  * [Jec06] T. Jech :  Set Theory: The Third Millennium Edition, revised and expanded.  Springer Monographs in Mathematics. Springer, 2006.
  * [Joh82] P.T. Johnstone :  Stone Spaces.  Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1982.
  * [Joh83] P.T. Johnstone :  The point of pointless topology.  Bulletin (New Series) of the American Mathematical Society, 8(1):41 – 53, 1983.
  * [Joh02] P.T. Johnstone :  Sketches of an Elephant: A Topos Theory Compendium.  Oxford Logic Guides. Clarendon Press, 2002.
  * [JR21] G. Jaber et C. Riba :  Temporal Refinements for Guarded Recursive Types.  _In_ N. Yoshida, éditeur : Proceedins of ESOP’21, volume 12648 de Lecture Notes in Computer Science, pages 548–578. Springer, 2021.
  * [Kec95] A. S. Kechris :  Classical Descriptive Set Theory, volume 156 de Graduate Texts in Mathematics.  Springer, 1995.
  * [KT14] E. Koskinen et T. Terauchi :  Local Temporal Reasoning.  _In_ Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS’14, New York, NY, USA, 2014. Association for Computing Machinery.
  * [KTU10] N. Kobayashi, N. Tabuchi et H. Unno :  Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification.  _In_ POPL ’10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 495–508, New York, NY, USA, 2010. Association for Computing Machinery.
  * [Lev03] P. B. Levy :  Call-By-Push-Value.  Semantics Structures in Computation. Springer, Dordrecht, 2003.
  * [Lev22] P. B. Levy :  Call-by-Push-Value.  ACM SIGLOG News, 9(2):7–29, may 2022.
  * [ML98] S. Mac Lane :  Categories for the Working Mathematician.  Springer, 2nd édition, 1998.
  * [NG03] M. Nygaard et W. Glynn :  Full Abstraction for HOPLA.  _In_ R.M. Amadio et D. Lugiez, éditeurs : CONCUR 2003 - Concurrency Theory, 14th International Conference, Marseille, France, September 3-5, 2003, Proceedings, volume 2761 de Lecture Notes in Computer Science, pages 378–392. Springer, 2003.
  * [NUKT18] Y. Nanjo, H. Unno, E. Koskinen et T. Terauchi :  A Fixpoint Logic and Dependent Effects for Temporal Property Verification.  _In_ Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS’18, pages 759–768, New York, NY, USA, 2018. Association for Computing Machinery.
  * [Pie02] B. C. Pierce :  Types and Programming Languages.  The MIT Press, 1st édition, 2002.
  * [Plo77] G. Plotkin :  LCF Considered as a Programming Language.  Theoretical Computer Science, 5:223–256, 1977.
  * [PP04] D. Perrin et J.-É. Pin :  Infinite Words: Automata, Semigroups, Logic and Games.  Pure and Applied Mathematics. Elsevier, 2004.
  * [PP11] J Picado et A. Pultr :  Frames and Locales: Topology without points.  Frontiers in Mathematics. Birkhäuser Basel, 2011.
  * [PP21] J Picado et A. Pultr :  Separation in Point-Free Topology.  Birkhäuser Cham, 2021.
  * [SSVH08] C. Skalka, S. Smith et D. Van Horn :  Types and Trace Effects of Higher Order Programs.  J. Funct. Program., 18(2):179–249, mars 2008.
  * [SU23] T. Sekiyama et H. Unno :  Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.  Proc. ACM Program. Lang., 7(POPL), jan 2023.  Full version available on arXiv at https://arxiv.org/abs/2207.10386.
  * [SV10] L. Santocanale et Y. Venema :  Completeness for flat modal fixpoint logics.  Ann. Pure Appl. Logic, 162(1):55–82, 2010\.
  * [UST18] H. Unno, Y. Satake et T. Terauchi :  Relatively complete refinement type system for verification of higher-order non-deterministic programs.  Proc. ACM Program. Lang., 2(POPL):12:1–12:29, 2018.
  * [Vic89] S. Vickers :  Topology via Logic.  Cambridge University Press, USA, 1989.
  * [Vic07] S. Vickers :  Locales and Toposes as Spaces.  _In_ M. Aiello, I. Pratt-Hartman et J. van Benthem, éditeurs : Handbook of Spatial Logics, chapitre 8, pages 429–496. Springer, 2007.
  * [VVK05] H. Völzer, D. Varacca et E. Kindler :  Defining Fairness.  _In_ Martín Abadi et Luca de Alfaro, éditeurs : CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings, volume 3653 de Lecture Notes in Computer Science, pages 458–472. Springer, 2005.
  * [Win04] G. Winskel :  Linearity and nonlinearity in distributed computation.  _In_ T. Ehrhard, J.-Y. Girard et P. Ruet, éditeurs : Linear Logic in Computer Science, London Mathematical Society Lecture Note Series. Cambridge University Press, 2004.
  * [Zha91] G. Zhang :  Logic of Domains.  Progress in Theoretical Computer Science. Birkhäuser, Boston, MA, 1991\.

full,long

full,long

long long

##  Appendix A Free Frames and Spatiality

Our approach to geometric logic in §4 focuses on _spaces_ of _models_.
However, the literature rather considers geometric logic as a formal way to
present frames by _generators and relations_. A customary tool for this is the
notion of _congruence preorder_ (see [Vic89, §4 and §6.1–2] and [Hec15, §3]).
It is folklore that congruence preorders can be presented using an
(infinitary) deduction system for geometric logic (in the spirit of e.g.
[Vic07, §2.2] and [Joh02, D1.1.7(m) and §D1.3]).

$\begin{array}[]{c}(\textsc{Th})\leavevmode\nobreak\
\dfrac{}{\varphi\vdash_{\mathtt{T}}\psi}\leavevmode\nobreak\ \text{(if
$(\varphi\vdash\psi)\in\mathtt{T}$)}\par\qquad\quad\par(\textsc{Ax})\leavevmode\nobreak\
\dfrac{}{\varphi\vdash_{\mathtt{T}}\varphi}\par\qquad\quad\par(\textsc{Cut})\leavevmode\nobreak\
\dfrac{\varphi\vdash_{\mathtt{T}}\theta\qquad\theta\vdash_{\mathtt{T}}\psi}{\varphi\vdash_{\mathtt{T}}\psi}\par\\\
\\\ (\textsc{$\land$-L${}_{1}$})\leavevmode\nobreak\
\dfrac{}{\varphi\land\psi\vdash_{\mathtt{T}}\varphi}\par\qquad\qquad\par(\textsc{$\land$-L${}_{2}$})\leavevmode\nobreak\
\dfrac{}{\varphi\land\psi\vdash_{\mathtt{T}}\psi}\par\qquad\qquad\par\par(\textsc{$\land$-R})\leavevmode\nobreak\
\dfrac{\theta\vdash_{\mathtt{T}}\varphi\qquad\theta\vdash_{\mathtt{T}}\psi}{\theta\vdash_{\mathtt{T}}\varphi\land\psi}\par\\\
\\\ (\textsc{$\mathtt{true}$-R})\leavevmode\nobreak\
\dfrac{}{\varphi\vdash_{\mathtt{T}}\mathtt{true}}\par\qquad\quad\par(\textsc{$\bigvee$-L})\leavevmode\nobreak\
\dfrac{\text{for all $i\in I$,
$\varphi_{i}\vdash_{\mathtt{T}}\psi$}}{\bigvee_{i\in
I}\varphi_{i}\vdash_{\mathtt{T}}\psi}\par\qquad\quad\par(\textsc{$\bigvee$-R})\leavevmode\nobreak\
\dfrac{}{\varphi_{i}\vdash_{\mathtt{T}}\bigvee_{i\in
I}\varphi_{i}}\par\end{array}$ Figure 3: Deduction rules for geometric logic
over a theory $\mathtt{T}$.

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. The _deduction
relation_ $\vdash_{\mathtt{T}}$ on $\mathtt{Geom}(\mathit{At})$ is defined by
the rules in Figure 3, using the constructs of Remark 4.1. The relation
$\vdash_{\mathtt{T}}$ is a preorder. Similarly as in §4.2, we quotient
$\mathtt{Geom}(\mathit{At})$ under the relation $\sim_{\mathtt{T}}$ of
_$\mathtt{T}$ -equivalence_ defined as $\varphi\sim_{\mathtt{T}}\psi$ iff
$\varphi\vdash_{\mathtt{T}}\psi$ and $\psi\vdash_{\mathtt{T}}\varphi$. We
write $[\varphi]_{\mathtt{T}}$ for the $\sim_{\mathtt{T}}$-class of $\varphi$
and $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ for the set of
$\sim_{\mathtt{T}}$-classes. We let $\leq_{\mathtt{T}}$ be the partial order
on $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ induced by $\vdash_{\mathtt{T}}$.
In contrast with [Joh02, §D1.3 and D1.4.14] (see also [Vic07, §2.2]), we do
not need to enforce frame distributivity in Figure 3, since it is hardwired in
the constructs of Remark 4.1.

$(\mathtt{Geom}(\mathit{At})/\mathtt{T},\leq_{\mathtt{T}})$ is a frame.

##### Spatiality.

How does $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ relate to the frame
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$ of §4.2? To answer this
question, we compare the preorders $\vdash_{\mathtt{T}}$ and
$\preceq_{\mathbf{Mod}(\mathtt{T})}$. First, an easy induction on derivations
proves the following _soundness_ property:

$\begin{array}[]{l l
l}\psi\vdash_{\mathtt{T}}\varphi&\Longrightarrow&\psi\preceq_{\mathbf{Mod}(\mathtt{T})}\varphi\end{array}$

The converse implication is a form of _completeness_ : if every model of
$\mathtt{T}$ is a model of the sequent $\psi\vdash\varphi$, then
$\psi\vdash_{\mathtt{T}}\varphi$ is derivable. This may fail in geometric
logic, by lack of spatiality. A frame $L$ is said to be _spatial_ if given
$a\not\leq b$ in $L$, there is a point $\mathcal{F}\in\mathrm{pt}(L)$ such
that $a\in\mathcal{F}$ and $b\notin\mathcal{F}$. A frame is spatial precisely
when it is isomorphic to $\Omega(X)$ for some space $X$, but not every frame
is spatial ([Joh82, §II.1.5]).

Assume now that $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial, and let
$\psi\not\vdash_{\mathtt{T}}\varphi$. Hence
$[\psi]_{\mathtt{T}}\not\leq_{\mathtt{T}}[\varphi]_{\mathtt{T}}$ and there is
a point $\mathcal{F}$ of $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ such that
$[\psi]_{\mathtt{T}}\in\mathcal{F}$ and
$[\varphi]_{\mathtt{T}}\notin\mathcal{F}$. Let
$\nu\colon\mathit{At}\to\mathbf{2}$ take $p\in\mathit{At}$ to $1$ iff
$[p]_{\mathtt{T}}\in\mathcal{F}$.

Let $\mathcal{F}$ and $\nu$ as above. Then for every
$\theta\in\mathtt{Geom}(\mathit{At})$, we have $\nu\models\theta$ if, and only
if, $[\theta]_{\mathtt{T}}\in\mathcal{F}$. In particular, $\nu$ is a model of
$\mathtt{T}$ with $\nu\models\psi$ and $\nu\not\models\varphi$.

Hence, when $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial, the preorders
$\vdash_{\mathtt{T}}$ and $\preceq_{\mathbf{Mod}(\mathtt{T})}$ coincide, and
$\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is thus isomorphic to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$. Since
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$ is always isomorphic to
the frame of opens of the space $\mathbf{Mod}(\mathtt{T})$ (Theorem 4.2), we
have the following.

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. Then the following
are equivalent.

  1. (i)

The frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial.

  2. (ii)

Deduction in $\vdash_{\mathtt{T}}$ is complete
($\psi\vdash_{\mathtt{T}}\varphi$ if, and only if,
$\psi\preceq_{\mathbf{Mod}(\mathtt{T})}\varphi$).

  3. (iii)

The frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is isomorphic to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T})$.

##### Free Frames and Congruence Preorders.

In view of Theorem A, it is interesting to know whether a frame
$\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial. We discuss this using the
following notions. Write $\mathtt{E}$ for the empty theory.

Let $\mathbf{U}\colon\mathbf{Frm}\to\mathbf{Set}$ be the forgetful functor. A
_free frame_ on $\mathit{At}$ is the data of a frame $L(\mathit{At})$ and of a
function $\eta_{\mathit{At}}\colon\mathit{At}\to\mathbf{U}L(\mathit{At})$ such
that for each frame $L$ and each function $f\colon\mathit{At}\to\mathbf{U}L$,
there is a unique frame morphism ${f}^{\star}\colon L(\mathit{At})\to L$
making the following diagram to commute.

${\mathit{At}}$${\mathbf{U}L}$${\mathbf{U}L(\mathit{At})}$$\scriptstyle{f}$$\scriptstyle{\eta_{\mathit{At}}}$$\scriptstyle{\mathbf{U}{f}^{\star}}$

######  Proposition 9.

$(\mathtt{Geom}(\mathit{At})/\mathtt{E},\leq_{\mathtt{E}})$ (with the function
$p\in\mathit{At}\mapsto[p]_{\mathtt{T}}$) is a free frame on $\mathit{At}$.

The operation $\mathit{At}\mapsto\mathtt{Geom}(\mathit{At})/\mathtt{E}$ thus
yields a left adjoint to $\mathbf{U}\colon\mathbf{Frm}\to\mathbf{Set}$ (see
e.g. [ML98, Theorem IV.1.2]). Actually, the set of Scott-opens of the cpo
$\mathcal{P}(\mathit{At})$ is also a free frame on $\mathit{At}$. See [Joh82,
Lemma VII.4.9] (see also [Hec15, Theorem 3.1] and [Joh02, C1.1.4 and C4.1.6]).
Since free frames are unique up to isomorphism, it follows that the frame
$\mathtt{Geom}(\mathit{At})/\mathtt{E}$ is spatial.

It is customary to present a frame by quotienting a free frame under a
congruence preorder. We refer to [Hec15, §3.4]. A _congruence preorder_ on a
frame $(L,\leq)$ is a preorder $\preceq$ on $L$ such that
${\leq}\subseteq{\preceq}$ and such that for each arbitrary (resp. finite)
$S\subseteq L$, we have $\bigvee S\preceq b$ whenever $a\preceq b$ for all
$a\in S$ (resp. $b\preceq\bigwedge S$ whenever $b\preceq a$ for all $a\in S$).
Given a congruence preorder $\preceq$ on $L$, let $a\sim b$ iff $a\preceq b$
and $b\preceq a$.

Each binary relation $R$ on $L$ is contained in a least congruence preorder
$\overline{R}$ on $L$.

######  Proposition 10.

Given geometric theories $\mathtt{T},\mathtt{U}$ over $\mathit{At}$, let
$R\coloneqq\\{([\varphi]_{\mathtt{T}},[\psi]_{\mathtt{T}})\mid(\varphi\vdash\psi)\in\mathtt{T}\cup\mathtt{U}\\}$.
Then $\mathtt{Geom}(\mathit{At})/(\mathtt{T}\cup\mathtt{U})$ is isomorphic to
the quotient of $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ by
$\sim_{\overline{R}}$.

In particular, $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is isomorphic to the
quotient of the free frame $\mathtt{Geom}(\mathit{At})/\mathtt{E}$ under
$\sim_{\overline{R}}$, where
$R=\\{([\varphi]_{\mathtt{E}},[\psi]_{\mathtt{E}})\mid(\varphi\vdash\psi)\in\mathtt{T}\\}$.

[[Joh02, D1.1.7(m) and D1.4.14]] Each frame $(L,\leq_{L})$ is isomorphic to
the frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}(L)$, where $\mathtt{T}(L)$ is
the following theory over $\mathit{At}\coloneqq\\{\underline{a}\mid a\in
L\\}$.

$\begin{array}[]{r !{\thesis} l @{\quad} l !{\qquad} r !{\thesis}
l}\underline{a}\lx@intercol\vdash&\underline{b}&\text{(if
$a\leq_{L}b$)}\par&\lx@intercol\vdash&\underline{\top_{L}}\\\
\underline{\bigvee_{L}S}\lx@intercol\vdash&\bigvee\left\\{\underline{a}\mid
a\in S\right\\}&\text{(if $S\subseteq
L$)}\par&\underline{a}\land\underline{b}\lx@intercol\vdash&\underline{a\land_{L}b}\par\end{array}$

Hence, any frame is a quotient of a free frame by a geometric theory. It then
follows from [Joh82, §II.1.5] that $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ may
not be spatial. On the positive side, we have

[[Hec15, Corollary 3.15]] Let $R$ be a _countable_ binary relation on a free
frame $L(\mathit{At})$. Then the quotient of $L(\mathit{At})$ under
$\sim_{\overline{R}}$ is a spatial frame.

Let $\mathtt{T}$ be a geometric theory over $\mathit{At}$. If $\mathtt{T}$ is
countable, then the frame $\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial.
In particular, if $\Phi$ is a $G_{\delta}$ formula of $\mathsf{LTL}(A)$, then
$\mathtt{Geom}(\mathit{At})/\mathtt{T}\llbracket\Phi\rrbracket$ is spatial,
where $\mathit{At}=\mathrm{Fin}(\llbracket\mathsf{Str}A\rrbracket)$.

Hence, when $\Phi$ is a $G_{\delta}$ formula of $\mathsf{LTL}$, deduction in
$\vdash_{\mathtt{T}\llbracket\Phi\rrbracket}$ completely axiomatizes
$\mathbf{Mod}(\mathtt{T}\llbracket\Psi\rrbracket)$, and the frame
$\mathtt{Geom}(\mathit{At})/\mathtt{T}\llbracket\Phi\rrbracket$ is isomorphic
to
$\mathtt{Geom}(\mathit{At})/\mathbf{Mod}(\mathtt{T}\llbracket\Phi\rrbracket)$.

We must warn the reader on the following subtle points, which actually
motivate the explicit constructions of §4.3.1.

######  Remark A.1.

Consider a space $(X,\Omega)$. It follows from Example 10 that there is a
theory $\mathtt{T}_{\Omega}$ over
$\mathit{At}_{\Omega}\coloneqq\\{\underline{U}\mid U\in\Omega\\}$ such that
$\Omega$ is isomorphic to
$\mathtt{Geom}(\mathit{At}_{\Omega})/\mathtt{T}_{\Omega}$ (so that
$\mathtt{Geom}(\mathit{At}_{\Omega})/\mathtt{T}_{\Omega}$ is spatial). But
beware that when $X$ is an algebraic dcpo, the theory
$\mathtt{T}\coloneqq\mathtt{T}(X)$ of §4.1 is over the set of atomic
propositions $\mathit{At}\coloneqq\mathrm{Fin}(X)$, which differs from
$\mathit{At}_{\Omega}$. In particular, the theories $\mathtt{T}$ and
$\mathtt{T}_{\Omega}$ differ, and there is _a priori_ no reason for $\Omega$
to be isomorphic to $\mathtt{Geom}(\mathit{At})/\mathtt{T}$.

An algebraic dcpo $X$ is said to be _$\omega$ -algebraic_ when
$\mathrm{Fin}(X)$ is (at most) countable. For instance,
$\llbracket\mathsf{Str}A\rrbracket$ is $\omega$-algebraic precisely when $A$
is (at most) countable.

Assume $X$ is $\omega$-algebraic. Set $\mathit{At}\coloneqq\mathrm{Fin}(X)$
and $\mathtt{T}\coloneqq\mathtt{T}(X)$ as above. The theory $\mathtt{T}$ is
countable, and Corollary A applies. Hence, the frame
$\mathtt{Geom}(\mathit{At})/\mathtt{T}$ is spatial and thus isomorphic to the
frame $\Omega$ (Theorem A, Theorem 4.2 and Proposition 4).

Consider now a subset $P\subseteq X$. Recall from §3.3 that the quotient frame
$\Omega\twoheadrightarrow\Omega\mathord{\upharpoonright}P$ can be represented