1 Introduction
The genesis of many connections between logic and geometry is rooted in the discovery of topological semantics for intuitionistic and modal logic, as pioneered by Stone [Reference Stone30], Tsao-Chen [Reference Tsao-Chen32], Tarski [Reference Tarski31], and McKinsey [Reference McKinsey20]. This semantics is now well-known. In short, one starts with a topological space X, and interprets intuitionistic formulas inside the Heyting algebra of open sets of X, and modal formulas inside the modal algebra of subsets of X with
$\square $
interpreted as the topological interior operator. A celebrated result due to Tarski [Reference Tarski31] states that this provides a complete semantics for intuitionistic propositional logic
$(\mathbf {IPC})$
on the one hand, and the modal logic
$\mathbf {S4}$
on the other. Moreover, one can even obtain completeness with respect to certain individual spaces. Specifically, McKinsey and Tarski showed [Reference McKinsey and Tarski21] that for any separable metric space X without isolated points, if
$\mathbf {IPC} \nvdash \phi $
, then
$\phi $
has a countermodel based on X, and similarly with
$\mathbf {S4}$
in place of
$\mathbf {IPC}$
. Later, Rasiowa and Sikorski showed that one can do without the assumption of separability [Reference Rasiowa and Sikorski25].
This result traces out an elegant interplay between topology and logic; however, it simultaneously establishes limits on the expressive power of this kind of interpretation. Indeed, examples of separable metric spaces without isolated points are the n-dimensional Euclidean space
$\mathbb {R}^n$
and the Cantor space
$2^{\omega }$
. What McKinsey and Tarski’s result shows, then, is that these spaces have the same logic, namely
$\mathbf {IPC}$
(or
$\mathbf {S4}$
). The upshot is that topological semantics does not allow logic to capture much of the geometric content of a space.
A natural idea is that, if we want to remedy the situation and allow for the capture of more information about a space, then we need an algebra finer than the Heyting algebra of open sets, or the modal algebra of arbitrary subsets with the interior operator. For example, Aiello, van Benthem, Bezhanishvili, and Gehrke consider the modal logic of chequered subsets of
$\mathbb {R}^n$
: finite unions of sets of the form
$\prod _{i=1}^n C_i$
, where each
$C_i \subseteq \mathbb {R}$
is convex ([Reference Aiello, van Benthem and Bezhanishvili3, Reference van Benthem, Bezhanishvili and Gehrke7]; see also [Reference van Benthem, Bezhanishvili, Aiello, Pratt-Hartmann and van Benthem6]). In [Reference Bezhanishvili, Marra, McNeill and Pedrini13, Reference Gabelaia, Gogoladze, Jibladze, Kuznetsov, Uridia, Silva, Staton, Sutton and Umbach15, Reference Gabelaia, Gogoladze, Jibladze, Kuznetsov and Marx16], this algebra-refinement idea is taken one step further. To be able to capture some of the geometric content of a space, one may restrict attention to topological spaces and subsets which are polyhedra (of arbitrary dimension). Indeed, the set
$\mathrm {Sub}_{\mathrm {o}}(P)$
of open subpolyhedra of P is a Heyting algebra under
$\subseteq $
(and a similar result holds in the modal case). This allows for an interpretation of intuitionistic and modal formulas in
$\mathrm {Sub}_{\mathrm {o}}(P)$
. The main result of [Reference Bezhanishvili, Marra, McNeill and Pedrini13] is that more is true. A polyhedral analogue of Tarski’s theorem holds: these polyhedral semantics are complete for
$\mathbf {IPC}$
and
$\mathbf {S4.Grz}$
. Furthermore, this approach delivers that logic can capture the dimension of the polyhedron in which it is interpreted, via the bounded depth formulas
${\textsf {bd}}_n$
[Reference Chagrov and Zakharyaschev14, Section 2.4]. In particular, the polyhedron P is n-dimensional if, and only if, P validates
${\textsf {bd}}_{n+1}$
and does not validate
${\textsf {bd}}_{n+2}$
for
$n\in \omega $
[Reference Bezhanishvili, Marra, McNeill and Pedrini13].
In this paper we make further advances in the study of polyhedral semantics. We introduce and study polyhedral completeness for intermediate logics. We say that an intermediate logic L is polyhedrally complete if there is a class
$\mathcal {C}$
of polyhedra such that L is the logic of
$\mathcal {C}$
. It follows from [Reference Bezhanishvili, Marra, McNeill and Pedrini13] that
$\mathbf {IPC}$
and the logic
$\mathbf {BD}_n$
of bounded depth n, for each n, are polyhedrally complete. We construct infinitely many polyhedrally complete logics, and show that there are continuum many polyhedrally incomplete ones all of which have the finite model property.
To this end we employ a time-honoured tool from combinatorial and polyhedral geometry, the nerve of a poset (=partially ordered set). The nerve will be our key concept relating logic with polyhedral geometry. In detail, the nerve
$\mathcal {N}(F)$
of the poset F is the collection of finite non-empty chains in F ordered by inclusion. As was already noted in [Reference Bezhanishvili, Marra, McNeill and Pedrini13], given a polyhedron P, a triangulation of P corresponds to a validity-preserving map from P onto the poset F of the faces of the triangulation. Through Esakia duality, in turn, this validity-preserving map corresponds to an embedding of the Heyting algebra of upsets of F into the Heyting algebra of open subpolyhedra of P. Nerves are closely related to barycentric subdivisions of triangulations. Indeed, if a finite poset F is the face poset of some triangulation
$\Sigma $
of a polyhedron P, then
$\mathcal {N}(F)$
corresponds to a barycentric subdivision of
$\Sigma $
.
Applying methods and results from rational polyhedral geometry we present a proof of our first main result, the Nerve Criterion for polyhedral completeness (Theorem 4.1): A logic L is complete with respect to some class of polyhedra if and only if it is the logic of a class of finite posets closed under taking nerves. Thus, we obtain that the logic of any given polyhedron is the logic of the iterated nerves of any one of its triangulations. The criterion yields many negative results, showing in particular that there are continuum-many non-polyhedrally complete logics with the finite model property (Theorem 5.4).
As to positive results, we consider logics defined using starlike trees—trees which only branch at the root—as forbidden configurations. Starlike logics are then those defined by the Jankov–Fine formulas of a collection of starlike trees. Exploiting the Nerve Criterion, and a result by Zakharyaschev [Reference Zakharyaschev34] that all these logics have the finite model property, we prove our second main result (Theorem 6.15): Every starlike logic is polyhedrally complete. This yields a countably infinite class of polyhedrally complete logics of each finite height and of infinite height. (For instance, Scott’s well-known logic
$\mathbf {SL}$
is in this class.) As forbidden configurations, starlike trees have a natural geometric meaning, expressing connectedness properties of polyhedral spaces.
The paper is organised as follows. In Section 2, we give the required background on intermediate logics and polyhedral geometry. Section 3 presents the polyhedral semantics first defined in [Reference Bezhanishvili, Marra, McNeill and Pedrini13]. In Section 4, we present and prove the Nerve Criterion for polyhedral completeness (Theorem 4.1). Making use of this criterion, Section 5 establishes that all stable logics (as defined in [Reference Bezhanishvili and Bezhanishvili9]) of height at least
$2$
are polyhedrally incomplete. Then in Section 6, we define the class of starlike logics, and prove that each one is polyhedrally complete. The techniques in these two sections are entirely combinatorial.
Finally, let us briefly comment on further research. One major problem already mentioned in [Reference Bezhanishvili, Marra, McNeill and Pedrini13] is to characterise the logic of piecewise-linear manifolds of a fixed dimension. Here we announce significant progress on this question; the results will appear in a forthcoming paper. A second relevant goal would be a complete classification of polyhedrally complete logics. At the time of writing, we do not know how to attain this goal. One might wonder if our results on starlike logics extend to arbitrary trees, or even to a wider class of posets. As to the latter, some negative results are obtained in [Reference Adam-Day1, Corollary 4.12]. For the former, the situation is rather obscure to us at the time of writing (cf. the discussion on ‘general trees’ in [Reference Adam-Day1, p. 61]). Identifying further classes of polyhedrally complete logics beyond the starlike ones introduced in this paper would be the next immediate task in the direction of obtaining a classification of polyhedrally complete logics.Footnote 1
2 Preliminaries
In this section we remind the reader of the relational and algebraic semantics for intermediate logics, and survey the definitions and results which will play their part in the forthcoming. As a main reference we use [Reference Chagrov and Zakharyaschev14]. We assume rather less familiarity with polyhedral geometry, and thus present in more detail the material we need.
2.1 Posets as Kripke frames
A (Kripke) frame for intuitionistic logic is simply a poset. We thus use the term ‘frame’ in this paper as a synonym of ‘poset’. The validity relation
$\vDash $
between frames and formulas is defined in the usual way (see, e.g., [Reference Chagrov and Zakharyaschev14, Chapter 2]). Given a class of frames
$\mathbf {C}$
, its logic is
Conversely, given a logic
$\mathcal {L}$
, define
A logic
$\mathcal {L}$
has the finite model property (fmp) if it is the logic of a class of finite frames. Equivalently, if
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\operatorname {{\mathrm {Frames}_{\mathrm {fin}}}}(\mathcal {L}))$
.
Fix a poset F. For any
$x \in F$
, its upset, downset, strict upset, and strict downset are defined, respectively, as follows:
For any set
$S \subseteq F$
, its upset and downset are defined, respectively, as follows:
A subframe is a subposet. A subframe
$U \subseteq F$
is upwards-closed or a generated subframe if
$U = \operatorname {\mathrm {\uparrow }} U$
, and it is downwards-closed if
$\operatorname {\mathrm {\downarrow }} U = U$
. The Alexandrov topology on F is the set
$\operatorname {{\mathrm {Up}}} F$
of its upwards-closed subsets. This constitutes a topology on F. In the sequel, we will freely switch between thinking of F as a poset and as a topological space. Note that the closed sets in this topology correspond to downwards-closed sets.
A chain in F is
$X \subseteq F$
which as a subposet is linearly ordered. The length of the chain X is
$\mathopen |X\mathclose |$
. A chain
$X \subseteq F$
is maximal if there is no chain
$Y \subseteq F$
such that
$X \subset Y$
(i.e., such that X is a proper subset of Y). The height of F is the element of
$\mathbb N \cup \{\infty \}$
defined by
For notational uniformity, say that this value is also the depth of F,
$\operatorname {\mathrm {\mathsf {depth}}}(F)$
. For any
$x \in F$
, define its height and depth as follows:
The height of a logic
$\mathcal {L}$
is the element of
$\mathbb N \cup \{\infty \}$
given by
A top element of F is
$t \in F$
such that
$\operatorname {\mathrm {\mathsf {depth}}}(t)=0$
. For any
$x,y \in F$
, say that x is an immediate predecessor of y, and that y is an immediate successor of x, if
$x < y$
and there is no
$z \in F$
such that
$x < z < y$
. Write
$\operatorname {{\mathrm {Succ}}}(x)$
for the collection of immediate successors of x.
The poset F is rooted if it has a minimum element, which is called the root, and is usually denoted by
$\bot $
. Define
An antichain in F is a subset
$Z \subseteq F$
in which no two elements are comparable. The width, notation
$\operatorname {\mathrm {\mathsf {width}}}(F)$
, of F is the cardinality of the largest antichain in F.
A function
$f \colon F \to G$
is a p-morphism if for every
$x \in F$
we have
$$ \begin{align*} f({\uparrow}(x) ) = {\Uparrow} (f(x)). \end{align*} $$
Equivalently, f should satisfy the following conditions:
$$ \begin{align} \forall x,y \in F\colon(x\leqslant y \Rightarrow f(x) \leqslant f(y)), \end{align} $$
$$ \begin{align} \forall x \in F \colon \forall z \in G \colon (f(x) \leqslant z \Rightarrow \exists y \in F \colon (x \leqslant y \wedge f(y)=z)). \end{align} $$
An up-reduction from F to G is a surjective p-morphism f from an upwards-closed set
$U \subseteq F$
to G. Write
$f \colon F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} G$
.
Proposition 2.1. If there is an up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} G$
then
$\operatorname {{\mathrm {Logic}}}(F) \subseteq \operatorname {{\mathrm {Logic}}}(G)$
. In other words, if
$G \nvDash \phi $
then
$F \nvDash \phi $
.
Proof See [Reference Chagrov and Zakharyaschev14, Corollary 2.8, p. 30, and Corollary 2.17, p. 32].
Corollary 2.2. If
$\mathbf {C}$
is any collection of frames and
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {C})$
, then
$$ \begin{align*} \mathcal{L} = \operatorname{{\mathrm{Logic}}}(\operatorname{{\mathrm{Frames}_{\bot}}}(\mathcal{L})). \end{align*} $$
Proof First,
$\mathcal {L} \subseteq \operatorname {{\mathrm {Logic}}}(\operatorname {{\mathrm {Frames}_{\bot }}}(\mathcal {L}))$
. Conversely, suppose
$\mathcal {L} \nvdash \phi $
. Then there exists
$F \in \mathbf {C}$
such that
$F \nvDash \phi $
, and hence there is
$x \in F$
such that
$x \nvDash \phi $
(for some valuation on F), meaning that
${\uparrow }(x) \nvDash \phi $
. Now,
${\uparrow }(x)$
is upwards-closed in F, and hence
$\mathsf {id}_{{\uparrow }(x)}$
is an up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} {\uparrow }(x)$
. Then by Proposition 2.1, we get that
${\uparrow }(x) \vDash \mathcal {L}$
, so that
${\uparrow }(x) \in \operatorname {{\mathrm {Frames}_{\bot }}}(\mathcal {L})$
.
2.2 Heyting algebras, topological semantics
A Heyting algebra is a bounded lattice equipped with a Heyting implication
$\rightarrow $
that satisfies
$$ \begin{align*} c \leqslant a \rightarrow b \quad\Leftrightarrow\quad c \wedge a \leqslant b. \end{align*} $$
The validity relation
$\vDash $
between Heyting algebras and formulas is defined in the usual way; the notation
$\operatorname {{\mathrm {Logic}}}(-)$
is extended appropriately. The logic of a Heyting algebra is exactly the logic of its finitely generated subalgebras. Say that A is locally finite if for every
$S \subseteq A$
finite, the algebra
${\langle S \rangle }$
generated by S is finite. If F is any poset, the bounded distributive lattice
$\operatorname {{\mathrm {Up}}} F$
is a Heyting algebra, and:
Proposition 2.3. If F is a poset,
$\operatorname {{\mathrm {Logic}}}(F) = \operatorname {{\mathrm {Logic}}}(\operatorname {{\mathrm {Up}}} F)$
.
Proof See [Reference Chagrov and Zakharyaschev14, Corollary 8.5, p. 238].
Co-Heyting algebras are the order-duals of Heyting algebras. Specifically, a co-Heyting algebra is a bounded lattice equipped with a co-Heyting implication
$\leftarrow $
that satisfies
$$ \begin{align*} a \leftarrow b \leqslant c \quad\Leftrightarrow\quad a \leqslant b \vee c. \end{align*} $$
For more information on co-Heyting algebras, the reader is referred to [Reference McKinsey and Tarski22, Section 1] and [Reference Rauszer26], where they are called ‘Brouwerian algebras’.
Given a topological space X, we regard the collection of open sets
$\operatorname {\mathrm {\mathcal {O}}}(X)$
of X as a Heyting algebra in the standard manner (cf. [Reference Chagrov and Zakharyaschev14, Proposition 8.31, p. 247]). (Recall that
$$ \begin{align*} U \rightarrow V = \operatorname{{\mathrm{Int}}}(U^{\mathsf{C}} \cup V), \end{align*} $$
where
$\operatorname {{\mathrm {Int}}}$
denotes the topological interior operator, and
$-^{\mathsf {C}}$
is set-theoretic complement.) We can thus interpret formulas in topological spaces. Write
$X \vDash \phi $
for
$\operatorname {\mathrm {\mathcal {O}}}(X) \vDash \phi $
, and extend the remaining notations accordingly.
The topological space X also comes with a co-Heyting algebra, namely its collection of closed sets
$\operatorname {\mathrm {\mathcal {C}}}(X)$
. The co-Heyting implication on
$\operatorname {\mathrm {\mathcal {C}}}(X)$
satisfies
where
$\operatorname {{\mathrm {Cl}}}$
denotes the topological closure operator. If a Heyting algebra A is regarded as a poset category
$(A, \leqslant )$
, then its opposite category
$A^{\mathrm {op}} = (A, \geqslant )$
is a co-Heyting algebra. In the case of the Heyting algebra
$\operatorname {\mathrm {\mathcal {O}}}(X)$
of open sets of X,
$\operatorname {\mathrm {\mathcal {O}}}(X)^{\mathrm {op}}$
is isomorphic to the co-Heyting algebra
$\operatorname {\mathrm {\mathcal {C}}}(X)$
of closed subsets of X.
2.3 Jankov–Fine formulas as forbidden configurations
To every finite, rooted frame Q, we associate a formula
$\chi (Q)$
, the Jankov–Fine formula of Q (also called its Jankov–De Jongh formula). The precise definition of
$\chi (Q)$
is somewhat involved, but the exact details of this syntactical form are not relevant for our considerations. What matters to us is its notable semantic property.
Theorem 2.4. For any frame F, we have that
$F \vDash \chi (Q)$
if and only if F does not up-reduce to Q.
Proof See [Reference Chagrov and Zakharyaschev14, Section 9.4, p. 310] for a treatment in which Jankov–Fine formulas are considered as specific instances of more general ‘canonical formulas’. An alternative proof can be found in [Reference Bezhanishvili12, Section 3.3, p. 56], which gives a complete definition of
$\chi (Q)$
. See also [Reference Bezhanishvili and Bezhanishvili9] for an algebraic version of this result.
Jankov–Fine formulas formalise the intuition of ‘forbidden configurations’. The formula
$\chi (Q)$
‘forbids’ the configuration Q from its frames.
The following consequence of Theorem 2.4 will come in handy later on.
Corollary 2.5. Let
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {C})$
where
$\mathbf {C}$
is a class of frames. Then
$$ \begin{align*} \operatorname{{\mathrm{Frames}_{\bot,\mathrm{fin}}}}(\mathcal{L}) = \{F \text{ finite, rooted frame} \mid \exists G \in \mathbf{C} \colon G {\mathrel{{\circ}\mkern-3mu{\rightarrow}}} F\}. \end{align*} $$
Proof First, if F is a finite, rooted frame such that there is
$G \in \mathbf {C}$
and an up-reduction
$G {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} F$
, then by Proposition 2.1 we have that
$F \in \operatorname {{\mathrm {Frames}_{\bot ,\mathrm {fin}}}}(\mathcal {L})$
. Conversely take F finite and rooted, and assume that there is no
$G \in \mathbf {C}$
with
$G {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} F$
. Then by Theorem 2.4,
$G \vDash \chi (F)$
for every
$G \in \mathbf {C}$
; whence
$\mathcal {L} \vdash \chi (F)$
. By Theorem 2.4,
$F \nvDash \chi (F)$
implying
$F \nvDash \mathcal {L}$
. This yields
$F \notin \operatorname {{\mathrm {Frames}_{\bot ,\mathrm {fin}}}}(\mathcal {L})$
.
2.4 Intermediate logics
The logic
$\mathbf {IPC}$
is intuitionistic propositional logic. An intermediate logic is any consistent logic extending
$\mathbf {IPC}$
. Classical logic,
$\mathbf {CPC}$
, is the largest intermediate logic.
Proposition 2.6.
$\mathbf {IPC}$
is the logic of the class of all finite frames, i.e.,
$\mathbf {IPC}$
has the fmp.
Proof See [Reference Chagrov and Zakharyaschev14, Theorem 2.57, p. 49].
For every
$n \in \mathbb N$
, let
$\mathbf {BD}_n$
be the logic of all finite frames of height at most n. This has the following axiomatisation in terms of Jankov–Fine formulas.
Proposition 2.7.
$\mathbf {BD}_n$
is the logic axiomatised by
$\mathbf {IPC}$
plus the Jankov–Fine formula of the chain (linear order) on
$n+1$
elements.
Proof See [Reference Chagrov and Zakharyaschev14, Table 9.7, p. 317, and Section 9].
Scott’s Logic,
$\mathbf {SL}$
, is usually axiomatised by the Scott sentence:
$$ \begin{align*} \mathbf{SL} = \mathbf{IPC} + \mathbf{IPC} + ((\neg\neg p \rightarrow p) \rightarrow p \vee \neg p) \rightarrow \neg p \vee \neg\neg p. \end{align*} $$
This logic can also be axiomatised using a forbidden configuration, as follows.
Proposition 2.8.
Proof See [Reference Chagrov and Zakharyaschev14, Table 9.7, p. 317, and Section 9].
2.5 Polytopes, polyhedra, and simplices
Polyhedra are certain subsets of finite-dimensional real affine spaces
$\mathbb {R}^n$
. An affine combination of
$x_0, \ldots , x_d \in \mathbb {R}^n$
is a point
$r_0 x_0 + \cdots + r_d x_d$
, where
$r_0, \ldots , r_d \in \mathbb {R}$
are such that
$r_0 + \cdots + r_d = 1$
. A convex combination is an affine combination in which additionally each
$r_i \geqslant 0$
. Given a set
$S \subseteq \mathbb {R}^n$
, its convex hull, notation
$\operatorname {{\mathrm {Conv}}} S$
, is the collection of convex combinations of its elements. (We stress that each convex combination involves, by definition, a finite subset of S only.) A subspace
$S \subseteq \mathbb {R}^n$
is convex if
$\operatorname {{\mathrm {Conv}}} S = S$
. A polytope is the convex hull of a finite set. A polyhedron in
$\mathbb {R}^n$
is a set which can be expressed as the finite union of polytopes. A subpolyhedron of a polyhedron P in
$\mathbb {R}^n$
is a subset of P which is itself a polyhedron. Note that every polyhedron is closed and bounded, hence compact, in the canonical (Euclidean) topology carried by the real affine space
$\mathbb {R}^n$
. All topological notions pertaining to polyhedra in the following refer to this topology.
A set of points
$x_0, \ldots , x_d$
is affinely independent if whenever
$$ \begin{align*} r_0 x_0 + \cdots + r_d x_d = \mathbf 0 \quad\text{and}\quad r_0 + \cdots + r_d = 0, \end{align*} $$
we must have that
$r_0, \ldots , r_d = 0$
. This is equivalent to saying that the vectors
$$ \begin{align*} x_1 - x_0, \ldots, x_d - x_0 \end{align*} $$
are linearly independent. A d-simplex is the convex hull
$\sigma $
of
$d+1$
affinely independent points
$x_0, \ldots , x_d$
, which we call its vertices. Write
$\sigma = x_0\cdots x_d$
; the dimension of
$\sigma $
is d.
Proposition 2.9. Every simplex determines its vertex set: two simplices coincide if and only if they share the same vertex set.
Proof See [Reference Maunder19, Proposition 2.3.3, p. 32].
A face of
$\sigma $
is the convex hull
$\tau $
of some non-empty subset of
$\{x_0, \ldots , x_d\}$
(note that
$\tau $
is then a simplex too). Write
$\tau \preccurlyeq \sigma $
, and
$\tau \prec \sigma $
if
$\tau \neq \sigma $
.
Since
$x_0, \ldots , x_d$
are affinely independent, every point
$x \in \sigma $
can be expressed uniquely as a convex combination
$x = r_0 x_0 + \cdots + r_d x_d$
with
$r_0, \ldots , r_d \geqslant 0$
and
$r_0 + \cdots + r_d = 1$
. Call the tuple
$(r_0, \ldots , r_d)$
the barycentric coordinates of x in
$\sigma $
. The barycentre
$\widehat \sigma $
of
$\sigma $
is the special point whose barycentric coordinates are
$(\frac {1}{d+1}, \ldots , \frac {1}{d+1})$
. The relative interior of
$\sigma $
is defined:
The relative interior of
$\sigma $
is ‘
$\sigma $
without its boundary’ in the following sense. The affine subspace spanned by
$\sigma $
is the set of all affine combinations of
$x_0, \ldots , x_d$
. Then the relative interior of
$\sigma $
coincides with the topological interior of
$\sigma $
inside this affine subspace, the latter being equipped with the subspace topology it inherits from
$\mathbb {R}^n$
. Note that
$\operatorname {{\mathrm {Cl}}}\operatorname {{\mathrm {Relint}}}\sigma = \sigma $
, the closure being taken in the ambient space
$\mathbb {R}^n$
.
2.6 Triangulations
A simplicial complex in
$\mathbb {R}^n$
is a finite set
$\Sigma $
of simplices satisfying the following conditions.
-
(a)
$\Sigma $
is
$\prec $
-downwards-closed: whenever
$\sigma \in \Sigma $
and
$\tau \prec \sigma $
we have
$\tau \in \Sigma $
. -
(b) If
$\sigma ,\tau \in \Sigma $
, then
$\sigma \cap \tau $
is either empty or a common face of
$\sigma $
and
$\tau $
.
The support of
$\Sigma $
is the set
. Note that by definition this set is automatically a polyhedron. We say that
$\Sigma $
is a triangulation of the polyhedron
$\mathopen |\Sigma \mathclose |$
. The set
$\Sigma $
is a poset under
$\prec $
, called the face poset of the triangulation. A subcomplex of
$\Sigma $
is subset which is itself a simplicial complex. Note that a subcomplex, as a poset, is precisely a downwards-closed set. Given
$\sigma \in \Sigma $
, its open star is defined:
Proposition 2.10. The relative interiors of the simplices in a simplicial complex
$\Sigma $
partition
$\mathopen |\Sigma \mathclose |$
. That is, for every
$x \in \mathopen |\Sigma \mathclose |$
, there is exactly one
$\sigma \in \Sigma $
such that
$x \in \operatorname {{\mathrm {Relint}}}\sigma $
.
Proof See [Reference Maunder19, Proposition 2.3.6, p. 33].
In light of Proposition 2.10, for any
$x \in \mathopen |\Sigma \mathclose |$
let us write
$\sigma ^x$
for the unique
$\sigma \in \Sigma $
such that
$x \in \operatorname {{\mathrm {Relint}}}\sigma $
. The simplex
$\sigma ^x$
is known as the carrier of x.
Proposition 2.11. Let
$\Sigma $
be a simplicial complex, take
$\tau \in \Sigma $
and
$x \in \operatorname {{\mathrm {Relint}}}\tau $
. Then no proper face
$\sigma \prec \tau $
contains x. This means that
$\sigma ^x$
is the inclusion-smallest simplex containing x.
Proof See [Reference Bezhanishvili, Marra, McNeill and Pedrini13, Lemma 3.1].
The next result is a basic fact of polyhedral geometry, and is of fundamental importance in its connection with logic. For
$\Sigma $
a triangulation and S a subset of the ambient space
$\mathbb {R}^n$
, define
This, being a downwards-closed subset of
$\Sigma $
, is a subcomplex of
$\Sigma $
.
Lemma 2.12 (Triangulation Lemma).
Any polyhedron admits a triangulation which simultaneously triangulates each of any fixed finite set of subpolyhedra. That is, for a collection of polyhedra
$P, Q_1, \ldots , Q_m$
such that each
$Q_i \subseteq P$
, there is a triangulation
$\Sigma $
of P such that
$\Sigma _{Q_i}$
triangulates
$Q_i$
for each i.
Proof See [Reference Rourke and Sanderson27, Theorem 2.11 and Addendum 2.12, p. 16].
2.7 Stellar and barycentric subdivisions
For
$\Sigma $
and
$\Delta $
simplicial complexes,
$\Delta $
is a subdivision or refinement of
$\Sigma $
, notation
$\Delta \lhd \Sigma $
, if
$\mathopen |\Sigma \mathclose |=\mathopen |\Delta \mathclose |$
and every simplex of
$\Delta $
is contained in a simplex of
$\Sigma $
.
Lemma 2.13. If
$\Delta \lhd \Sigma $
then for every
$\sigma \in \Sigma $
we have
$$ \begin{align*} \sigma = \bigcup\{\tau \in \Delta \mid \tau \subseteq \sigma\}. \end{align*} $$
Proof Let
. Clearly
$\bigcup S \subseteq \sigma $
. Conversely, for
$x \in \sigma $
, let
$\tau ^x \in \Delta $
be such that
$x \in \operatorname {{\mathrm {Relint}}}\tau ^x$
. Since
$\Delta $
refines
$\Sigma $
, there is some
$\rho \in \Sigma $
such that
$\tau ^x \subseteq \rho $
; assume that
$\rho $
is inclusion-minimal with this property. It follows from [Reference Spanier28, Section 3, Lemma 3, p. 121] that
$\operatorname {{\mathrm {Relint}}}\tau ^x \subseteq \operatorname {{\mathrm {Relint}}}\rho $
, meaning that
$x \in \sigma \cap \operatorname {{\mathrm {Relint}}} \rho $
. By condition (b) in the definition of a simplicial complex, we have that
$\sigma \cap \rho $
is face of
$\rho $
. But then by Proposition 2.11,
$\rho \preccurlyeq \sigma $
, since otherwise
$\sigma \cap \rho $
would be a proper face of
$\rho $
containing
$x \in \operatorname {{\mathrm {Relint}}} \rho $
. Therefore
$\tau ^x \subseteq \rho \subseteq \sigma $
so that
$x \in \bigcup S$
.
We now introduce a special class of subdivisions, for which the original source [Reference Alexander4] remains a fundamental reference. Let
$\Sigma $
be a simplicial complex, and let
$c\in |\Sigma |$
. The elementary stellar subdivision of
$\Sigma $
at c is the set of simplices
$\Delta $
obtained from
$\Sigma $
via the following transformation: Replace each simplex
$\sigma \in \Sigma $
that contains c by the set of all simplices
$\operatorname {{\mathrm {Conv}}}{\{\tau \cup \{c\}\}}$
, where
$\tau $
ranges over all faces of
$\sigma $
that do not contain c. It can then be proved that
$\Delta $
is again a triangulation, and a subdivision of
$\Sigma $
. The equality
$\Sigma =\Delta $
holds precisely when the chosen c is a vertex of
$\Sigma $
. If
$\Delta $
is a subdivision of
$\Sigma $
that is obtained via a finite number of successive elementary subdivisions of
$\Sigma $
, then
$\Delta $
is a stellar subdivision of
$\Sigma $
. See Figure 1.
Examples of elementary stellar subdivisions.
If
$\Delta $
is obtained from
$\Sigma $
via an elementary stellar subdivision at
$c\in |\Sigma |$
, and c is moreover the barycentre of the vertices of its carrier simplex
$\sigma ^c\in \Sigma $
(see Proposition 2.10 and the comments following it), then
$\Delta $
is an elementary barycentric subdivision of
$\Sigma $
(at the barycentre c).
The barycentric subdivision
$\operatorname {{\mathrm {Sd}}}\Sigma $
of
$\Sigma $
is then defined as the refinement of
$\Sigma $
obtained by successively applying elementary barycentric subdivisions at each simplex of
$\Sigma $
, proceeding in decreasing order of dimension. It can be proved that
$\operatorname {{\mathrm {Sd}}}\Sigma $
does not depend on the chosen ordering of the simplices of
$\Sigma $
. See the examples in Figure 2. In the literature,
$\operatorname {{\mathrm {Sd}}}\Sigma $
is also often called the first derived subdivision of
$\Sigma $
(cf., e.g., [Reference Rourke and Sanderson27]). We inductively define, for each
$k\in \mathbb {N}$
, the
$k^{\mathrm {th}}$
derived subdivision of
$\Sigma $
:
; and
$\Sigma ^{(k)} =\operatorname {{\mathrm {Sd}}} \Sigma ^{(k-1)}$
.
Examples of barycentric subdivision. Each simplex in the simplicial complex is divided at its barycentre, proceeding in decreasing order of dimension. The bottom right tetrahedron is drawn without filled-in faces to aid clarity.
3 The algebra of open subpolyhedra
With the preliminaries in place, we relate intuitionistic logic and polyhedra. For further details please see [Reference Bezhanishvili, Marra, McNeill and Pedrini13].
3.1 Polyhedral semantics
Given a polyhedron P, let
$\mathrm {Sub} P$
denote the set of its subpolyhedra.
Theorem 3.1.
$\mathrm {Sub} P$
is a co-Heyting algebra, and a subalgebra of
$\operatorname {\mathrm {\mathcal {C}}}(P)$
.
Proof See [Reference Bezhanishvili, Marra, McNeill and Pedrini13, Corollary 3.4]. The proof makes fundamental use of the Triangulation Lemma.
By an open subpolyhedron of a polyhedron P in this paper we mean the complement (in P) of a subpolyhedron of P. Denote by
$\mathrm {Sub}_{\mathrm {o}} P$
the collection of open subpolyhedra in P. Evidently, there is an isomorphism
$\mathrm {Sub}_{\mathrm {o}} P\cong (\mathrm {Sub} P)^{\mathrm {op}}$
, and Theorem 3.1 yields the following.
Theorem 3.2. For any polyhedron P,
$\mathrm {Sub}_{\mathrm {o}} P$
is a Heyting algebra, and a subalgebra of
$\operatorname {\mathrm {\mathcal {O}}}(P)$
.
For any formula
$\phi $
and polyhedron P, say that
$P \vDash \phi $
if and only if
$\mathrm {Sub}_{\mathrm {o}} P \vDash \phi $
as a Heyting algebra. Call an intermediate logic polyhedrally complete if it is the logic of some class of polyhedra. In [Reference Bezhanishvili, Marra, McNeill and Pedrini13], it is shown that
$\mathbf {IPC}$
is polyhedrally complete, being the logic of all polyhedra, while
$\mathbf {BD}_n$
is the logic of all polyhedra of dimension at most n. It is also shown that all polyhedrally complete logics must have the finite model property (cf. Theorem 3.7).
3.2 Triangulation subalgebras
Let
$\Sigma $
be a triangulation of the polyhedron P. Then
$\Sigma \subseteq \mathrm {Sub} P$
. Let
$\mathrm {P}_{\mathrm {c}}(\Sigma )$
be the sublattice of
$\mathrm {Sub} P$
generated by
$\Sigma $
.
Lemma 3.3.
$\mathrm {P}_{\mathrm {c}}(\Sigma )$
is a co-Heyting subalgebra of
$\mathrm {Sub} P$
.
Proof See [Reference Bezhanishvili, Marra, McNeill and Pedrini13, Lemma 3.6].
Call any algebra of the form
$\mathrm {P}_{\mathrm {c}}(\Sigma )$
a triangulation subalgebra.
Lemma 3.4. Every finitely generated subalgebra of
$\mathrm {Sub} P$
is contained in some triangulation algebra.
Proof See [Reference Bezhanishvili, Marra, McNeill and Pedrini13, Lemma 3.2]. Essentially, this is the content of the Triangulation Lemma 2.12.
Turning now to the dual, every triangulation
$\Sigma $
of a polyhedron P gives rise to a Heyting subalgebra
$\mathrm {P}_{\mathrm {o}}(\Sigma )$
of
$\mathrm {Sub}_{\mathrm {o}} P$
, which we also call a triangulation subalgebra, generated by the complements of the simplices in
$\Sigma $
.
Corollary 3.5. For any polyhedron P,
$\mathrm {Sub}_{\mathrm {o}} P$
is a locally finite Heyting algebra.
Proof This follows from the dual of Lemma 3.4 and the fact that triangulation subalgebras are finite.
The algebra
$\mathrm {P}_{\mathrm {o}}(\Sigma )$
, though not necessarily easy to visualise geometrically, is in fact precisely the algebra of upsets of the poset
$\Sigma $
.
Lemma 3.6. The map
$$ \begin{align*} \gamma^\uparrow \colon \operatorname{{\mathrm{Up}}} \Sigma &\to \mathrm{P}_{\mathrm{o}}(\Sigma) \\ U &\mapsto \bigcup_{\sigma \in U}\operatorname{{\mathrm{Relint}}}(\sigma) \end{align*} $$
is an isomorphism of Heyting algebras.
Proof See [Reference Bezhanishvili, Marra, McNeill and Pedrini13, Lemma 4.3].
As a consequence of the preceding results, we have:
Theorem 3.7. The logic of a polyhedron is the logic of its triangulations.
The following additional facts about triangulation algebras will be useful later on.
Lemma 3.8.
-
(1) Triangulation algebras determine their corresponding triangulations. That is, for any two triangulations
$\Sigma $
and
$\Delta $
, if
$\mathrm {P}_{\mathrm {o}}(\Sigma )=\mathrm {P}_{\mathrm {o}}(\Delta )$
then
$\Sigma =\Delta $
. -
(2) If
$\Sigma $
and
$\Delta $
are triangulations which are isomorphic as posets then
$\mathrm {P}_{\mathrm {o}}(\Sigma ) \cong \mathrm {P}_{\mathrm {o}}(\Delta )$
. -
(3) If
$\Delta $
refines
$\Sigma $
, then
$\mathrm {P}_{\mathrm {o}}(\Sigma )$
is a subalgebra of
$\mathrm {P}_{\mathrm {o}}(\Delta )$
.
Proof
-
(1) It follows from conditions (a) and (b) on simplicial complexes that
$\mathrm {P}_{\mathrm {c}}(\Sigma )$
consists exactly of the unions of elements of
$\Sigma $
, and similarly for
$\Delta $
. Assume
$\mathrm {P}_{\mathrm {o}}(\Sigma ) = \mathrm {P}_{\mathrm {o}}(\Delta )$
, so that
$\mathrm {P}_{\mathrm {c}}(\Sigma ) = \mathrm {P}_{\mathrm {c}}(\Delta )$
, and take
$\sigma \in \Sigma $
. Then
$\sigma \in \mathrm {P}_{\mathrm {c}}(\Delta )$
, so
$\sigma = \bigcup S$
for some
$S \subseteq \Delta $
, and similarly each
$\tau \in S$
is
$\tau = \bigcup T_{\tau }$
for some
$T_{\tau } \subseteq \Sigma $
. Hence
$$ \begin{align*} \sigma = \bigcup\bigcup_{\tau \in S} T_{\tau}. \end{align*} $$
But then by condition (b) on
$\Sigma $
, every
$\rho \in \bigcup _{\tau \in S} T_{\tau }$
must either be equal to
$\sigma $
or be a proper face of
$\sigma $
. Since
$\operatorname {{\mathrm {Relint}}} \sigma $
contains no proper face of
$\sigma $
, we must have
$\sigma \in T_{\tau }$
for some
$\tau \in S$
. But then
$\sigma \subseteq \tau \subseteq \sigma $
, and so
$\sigma \in \Delta $
. Applying this argument also in the other direction, we get that
$\Sigma = \Delta $
. -
(2) This follows from Lemma 3.6.
-
(3) By Lemma 2.13, every
$\sigma \in \Sigma $
is the union of simplices in
$\Delta $
. Whence
$\Sigma \subseteq \mathrm {P}_{\mathrm {c}}(\Delta )$
. Therefore, by definition
$\mathrm {P}_{\mathrm {c}}(\Sigma ) \subseteq \mathrm {P}_{\mathrm {c}}(\Delta )$
. From this it follows that
$\mathrm {P}_{\mathrm {o}}(\Sigma ) \subseteq \mathrm {P}_{\mathrm {o}}(\Delta )$
.
3.3 PL homeomorphisms
Let
$P\subseteq \mathbb {R}^m$
and
$Q\subseteq \mathbb {R}^n$
be polyhedra. A continuous function
$f\colon P\to Q$
is piecewise-linear, or is a PL map, if the graph of f is a polyhedron in the product space
$\mathbb {R}^m\times \mathbb {R}^n$
. A PL homeomorphism is a PL map that is a homeomorphism.
Proposition 3.9. The inverse of a PL homeomorphism is a PL homeomorphism.
Proof See [Reference Rourke and Sanderson27, p. 6].
Proposition 3.10. If P and Q are PL homeomorphic then
$\mathrm {Sub}_{\mathrm {o}}{Q}$
and
$\mathrm {Sub}_{\mathrm {o}}{P}$
are isomorphic Heyting algebras, and
$\operatorname {{\mathrm {Logic}}}(P)=\operatorname {{\mathrm {Logic}}}(Q)$
.
Proof It is obvious that any homeomorphism between P and Q induces an isomorphism of their open-set lattices by taking inverse images. Since the inverse image of a subpolyhedron under a PL homeomorphism is again a subpolyhedron [Reference Rourke and Sanderson27, Corollary 2.5, p. 13], and in light of Proposition 3.9, we see that when the homeomorphism is PL this isomorphism of open-set lattices descends to an isomorphism of distributive lattices between
$\mathrm {Sub}_{\mathrm {o}} P$
and
$\mathrm {Sub}_{\mathrm {o}} Q$
. This implies that
$\mathrm {Sub}_{\mathrm {o}} P$
and
$\mathrm {Sub}_{\mathrm {o}} Q$
are isomorphic as Heyting algebras, too, because the Heyting implication is uniquely determined by the underlying lattice structure, and the proof is complete.
4 The Nerve Criterion
Given a poset F, its nerve,
$\mathcal {N}(F)$
, is the collection of finite non-empty chains in F ordered by inclusion. The following theorem is the first main contribution of the paper:
Theorem 4.1 (The Nerve Criterion).
A logic is polyhedrally complete if, and only if, it is the logic of a class of finite posets closed under the nerve operator
$\mathcal {N}$
.
The utility of the Nerve Criterion is that it transforms logico-geometric questions into questions about finite posets, to which finite combinatorial methods are applicable.
Remark 4.2. We cannot strengthen the left-to-right direction to the following. “If a logic
$\mathcal {L}$
is polyhedrally complete then
$\operatorname {{\mathrm {Frames}_{\mathrm {fin}}}}(\mathcal {L})$
is closed under the nerve operator
$\mathcal {N}$
”. By Corollary 6.16 Scott’s Logic
$\mathbf {SL}$
is polyhedrally complete. However
$\operatorname {{\mathrm {Frames}_{\mathrm {fin}}}}(\mathbf {SL})$
contains the frame F given in Figure 3. As can be seen there, the nerve
$\mathcal {N}(F)$
does not validate
$\mathbf {SL}$
, since there is an up-reduction
. Using the terminology introduced in Section 6, the problem is that while F is
$(2 \cdot 1)$
-connected, it is not
$(2 \cdot 1)$
-diamond-connected.
An example showing that the
$\operatorname {{\mathrm {Frames}_{\mathrm {fin}}}}(\mathbf {SL})$
is not closed under
$\mathcal {N}$
, even though
$\mathbf {SL}$
is polyhedrally complete.
Achieving a proof of the Nerve Criterion will require considerable work with rational triangulations and their subdivisions. We next state the key intermediate result to be obtained. Let A be a triangulation subalgebra of
$\mathrm {Sub}_{\mathrm {o}} P$
, for some polyhedron P. By Lemma 3.8((1)), there is a unique triangulation
$\Sigma $
of P such that
$A = \mathrm {P}_{\mathrm {o}}(\Sigma )$
. For any
$k \in \mathbb N$
, let
, where
$\Sigma ^{(k)}$
is the k-th derived subdivision of
$\Sigma $
(see Section 2.7).
Theorem 4.3. Let P be a polyhedron, and let A be any triangulation subalgebra of
$\mathrm {Sub}_{\mathrm {o}} P$
. For any finitely generated subalgebra B of
$\mathrm {Sub}_{\mathrm {o}}{P}$
, there is
$k \in \mathbb N$
such that B is isomorphic to a subalgebra of
$A^{(k)}$
.
Sections 4.1–4.4 will be devoted to proving Theorem 4.3. The proof of the Nerve Criterion is completed in Section 4.6.
4.1 Rational polyhedra and unimodular triangulations
The geometric intuition behind Theorem 4.3 is that any triangulation can be approximated from any other by taking iterated barycentric subdivisions. One difficulty with spelling out such an intuition is that if we start with a triangulation
$\Sigma $
on vertices with irrational coordinates, and try to approximate it using the iterated barycentric subdivisions of a triangulation on vertices with rational coordinates, the approximations can never quite capture (a refinement of)
$\Sigma $
. The approach taken here is effectively to show that it suffices to restrict attention to the rational case. In order to make this idea precise, we need tools on rational triangulations that go beyond the standard polyhedral topology handbooks, which typically deal with the real case only. For these tools we mainly use [Reference Mundici23] as a background reference.
A polytope in
$\mathbb {R}^n$
is rational if it may be written as the convex hull of finitely many points in
$\mathbb {Q}^n \subseteq \mathbb {R}^n$
. A polyhedron in
$\mathbb {R}^n$
is rational if it may be written as a union of a finite collection of rational polytopes. A simplicial complex
$\Sigma $
is rational if it consists of rational simplices. Note that when this is the case,
$\mathopen |\Sigma \mathclose |$
is a rational polyhedron.
For any
$x \in \mathbb {Q}^n \subseteq \mathbb {R}^n$
, there is a unique way to write out x in coordinates as
$x = (\frac {p_1}{q_1},\ldots ,\frac {p_n}{q_n})$
such that for each i, we have
$p_i,q_i \in \mathbb {Z}$
coprime. The denominator of x is defined:
Thus,
$\operatorname {{\mathrm {Den}}}(x)=1$
if and only if x has integer coordinates. Letting
$q = \operatorname {{\mathrm {Den}}}(x)$
, the homogeneous correspondent of x is defined to be the integer vector:
A rational d-simplex
$\sigma = x_0 \cdots x_d$
is unimodular if there is an
$(n+1)\times (n+1)$
matrix with integer entries whose first
$d+1$
columns are
$\widetilde {x}_0,\ldots ,\widetilde {x}_d$
, and whose determinant is
$\pm 1$
. This is equivalent to requiring that the set
$\{\widetilde {x}_0,\ldots ,\widetilde {x}_d\}$
can be completed to a
$\mathbb {Z}$
-module basis of
$\mathbb {Z}^{d+1}$
. A simplicial complex is unimodular if each one of its simplices is unimodular.
4.2 Farey subdivisions
Proposition 4.4. Given a rational simplex
$\sigma $
with vertices
$x_0, \ldots , x_d \in \mathbb {Q}^n\subseteq \mathbb {R}^n$
, there is a unique
$m \in \mathbb {Q}^n$
such that
$\widetilde m = \sum _{i=0}^d\widetilde {x}_i$
. Moreover,
$m\in \operatorname {{\mathrm {Relint}}}{\sigma }$
.
Proof Let
$H_{n+1} \subseteq \mathbb {R}^{n+1}$
be the hyperplane specified by
Identify
$\mathbb {Q}^n$
with the set of rational points of
$H_{n+1}$
via the map
$(q_1,\ldots ,q_n)\mapsto (q_1,\ldots ,q_n,1)$
. Under this identification,
$\widetilde m$
lies in the rational cone:
$$ \begin{align*} \left\{\sum_{i=0}^d c_i\widetilde x_i\mid c_i\in\mathbb{R}, c_i \geqslant 0\right\}. \end{align*} $$
A routine computation then proves the geometrically evident fact that m is the point of intersection of the line spanned in
$\mathbb {R}^{n+1}$
by the vector
$\widetilde m$
, with the hyperplane
$H_{n+1}$
; from which the result follows.
The element
$m \in \mathbb {Q}^n$
in Proposition 4.4 is called the Farey mediant of (the vertices of) the simplex
$\sigma $
. Note that when
$d=0$
, i.e., when
$\sigma $
is a vertex of
$\Sigma $
, then m coincides with the vertex
$\sigma $
. Also observe that the Farey mediant and the barycentre of
$\sigma $
are in general distinct, though both lie in
$\operatorname {{\mathrm {Relint}}}{\sigma }$
.
We can now define a specific type of stellar subdivision based on Farey mediants (cf. [Reference Mundici23, Section 5.1, p. 55]). Let
$\Sigma $
be a simplicial complex, let
$\sigma \in \Sigma $
, and let m be the Farey mediant of
$\sigma $
. The elementary Farey subdivision of
$\Sigma $
at m is the elementary stellar subdivision of
$\Sigma $
at m. In general, the triangulation
$\Delta $
is a Farey subdivision of
$\Sigma $
if it is obtained from the latter via finitely many successive elementary Farey subdivisions.
At the combinatorial level, Farey and barycentric subdivisions are indiscernible:
Lemma 4.5. Let
$\Sigma , \Delta $
be simplicial complexes with
$\Sigma $
rational, assume that
$\gamma \colon \Sigma \to \Delta $
is an isomorphism of
$\Sigma $
and
$\Delta $
as posets, let
$\sigma \in \Sigma $
, and let m be the Farey mediant of
$\sigma $
. Then the elementary Farey subdivision of
$\Sigma $
at m and the elementary barycentric subdivision of
$\Delta $
at the barycentre of
$\gamma (\sigma )$
are isomorphic as posets.
Proof Indeed, at the level of posets, elementary Farey subdivision and elementary barycentric subdivision are the same operation, as direct inspection of the definitions confirms. For further details see also [Reference Alexander4, Section III].
However, going beyond the combinatorial level, the construction of universal approximations of arbitrary rational polyhedra does require Farey subdivisions and cannot be done with barycentric ones. This is made precise in the following fundamental fact of rational polyhedral geometry.
Lemma 4.6 (The De Concini–Procesi Lemma).
Let P be a rational polyhedron, and let
$\Sigma $
be a unimodular triangulation of P. There exists a sequence
$(\Sigma _i)_{i \in \mathbb N}$
of unimodular triangulations of P with
$\Sigma _0=\Sigma $
such that:
-
(a) for each
$i\in \mathbb N$
,
$\Sigma _{i+1}$
is an elementary Farey subdivision of
$\Sigma _i$
, and -
(b) for any rational polyhedron
$Q\subseteq P$
, there is
$i\in \mathbb N$
such that
$\Sigma _i$
triangulates Q.
Proof See [Reference Mundici23, Theorem 5.3, p. 57].
4.3 From
$\mathbb {R}$
to
$\mathbb {Q}$
To deploy the power of Lemma 4.6, we need to relate general polyhedra to rational polyhedra, and general triangulations to unimodular ones.
Lemma 4.7. Let P be a polyhedron, and let
$\Sigma $
be a triangulation of P. There exist an integer
$n\in \mathbb N$
, a rational polyhedron
$Q\subseteq \mathbb {R}^n$
, and a unimodular triangulation
$\Delta $
of Q such that P and Q are PL-homeomorphic via a map that induces an isomorphism of
$\Sigma $
and
$\Delta $
as posets.
Proof This is a standard argument. Fix a bijection
$\beta $
from the vertices of
$\Sigma $
to the standard basis of
$\mathbb {R}^n$
, where n is the number of vertices in
$\Sigma $
. Take a simplex
$\sigma = x_0 \cdots x_d$
in
$\Sigma $
. Note that the points
$\beta (x_0), \ldots , \beta (x_d)$
are affinely independent; let
$\alpha (\sigma )$
be the d-simplex spanned by their convex hull:
. Since the vertices of
$\alpha (\sigma )$
are standard basis elements,
$\alpha (\sigma )$
is a unimodular simplex by definition. Let
$f_{\sigma } \colon \sigma \to \alpha (\sigma )$
be the linear map determined by
$f_{\sigma }(x_i) = \beta (x_i)$
for each i, and let
$g_{\sigma } \colon \alpha (\sigma ) \to \sigma $
be its inverse, determined by
$g_{\sigma }(\beta (x_i)) = x_i$
.
Now, let
. For any simplices
$\sigma \preccurlyeq \tau $
, the map
$f_{\sigma }$
agrees with
$f_{\tau }$
on
$\sigma $
. Hence we may glue these maps together to form a map
$f \colon P \to Q$
, i.e.,
$f(x)=f_{\sigma }(x)$
, where
$\sigma $
is any simplex of
$\Sigma $
containing x. Similarly, we may glue together the maps
$g_{\sigma }$
for
$\sigma \in \Sigma $
to form an inverse to f. By definition f is a PL homeomorphism. Finally, note that
is a triangulation of Q, and that f induces the poset isomorphism
$\sigma \mapsto \alpha (\sigma )$
between
$\Sigma $
and
$\Delta $
.
Lemma 4.8. Let
$\Sigma $
be a unimodular triangulation of the rational polyhedron P, and suppose
$\Sigma '$
is a Farey subdivision of
$\Sigma $
. There is a triangulation
$\Delta $
of P which is isomorphic as a poset to
$\Sigma '$
, and
$k \in \mathbb N$
such that
$\Sigma ^{(k)}$
refines
$\Delta $
.
Proof The proof works by replacing each elementary Farey subdivision by an elementary barycentric subdivision. We induct on the number
$m \in \mathbb N^{>0}$
of elementary Farey subdivisions needed to obtain
$\Sigma '$
from
$\Sigma $
. If
$m=1$
, let
$\sigma $
be the simplex of
$\Sigma $
being subdivided at its Farey mediant. Then the first barycentric subdivision
$\Sigma ^{(1)}$
of
$\Sigma $
refines the elementary barycentric subdivision
$\Sigma ^*$
of
$\Sigma $
at the barycentre of
$\sigma $
. By Lemma 4.5,
$\Sigma ^*$
and
$\Sigma '$
are isomorphic.
For the induction step, suppose
$m>1$
, and write
$(\Sigma _i)_{i=0}^m$
for the finite sequence of triangulations connecting
$\Sigma =\Sigma _0$
to
$\Sigma '=\Sigma _m$
through elementary Farey subdivisions. By the induction hypothesis, there is
$k\in \mathbb N$
such that
$\Sigma ^{(k)}$
refines a triangulation
$\Delta $
isomorphic to
$\Sigma _{m-1}$
; let us fix one such isomorphism
$\gamma $
. Let
$\sigma $
be the d-simplex of
$\Sigma _{m-1}$
that must be subdivided through its Farey mediant in order to obtain
$\Sigma _m$
. Let further
$\delta $
be the simplex of
$\Delta $
that corresponds to
$\sigma $
through the isomorphism
$\gamma $
. Since the d-simplices are exactly the height-d elements of
$\Delta $
, we get that
$\delta $
is a d-simplex. Then
$\Sigma ^{(k+1)}$
refines
$\Delta ^*$
, the latter denoting the elementary barycentric subdivision of
$\Delta $
at the barycentre of
$\delta $
. But
$\Delta $
is isomorphic to
$\Sigma _{m-1}$
, and therefore by Lemma 4.5,
$\Delta ^*$
is isomorphic to
$\Sigma _{m}$
.
Finally, we shall need the non-trivial fact that arbitrary triangulations of a rational polyhedron realise no more combinatorial types than its rational triangulations; this is due to Meurig Beynon:
Lemma 4.9 (Beynon’s Lemma).
Let P be a rational polyhedron, and let
$\Sigma $
be a triangulation of P. There exists a rational triangulation of P which is isomorphic as a poset to
$\Sigma $
.
Proof This is the main result of [Reference Beynon8].
4.4 End of proof of Theorem 4.3
Proof of Theorem 4.3
Let
$\Sigma $
be the triangulation of P such that
$A=\mathrm {P}_{\mathrm {o}}{(\Sigma )}$
. Using Lemma 4.7, Lemma 3.8
(2), and Proposition 3.10 we may assume without loss of generality that P is rational and
$\Sigma $
is unimodular. By Lemma 3.4, there is a triangulation
$\Delta $
of P such that B is isomorphic to a subalgebra of
$\mathrm {P}_{\mathrm {o}}{(\Delta )}$
. By Beynon’s Lemma 4.9 and Lemma 3.8
(2), we may assume that
$\Delta $
is rational (and hence each member of B is, too). By the De Concini–Procesi Lemma 4.6, there is a Farey subdivision
$\Sigma '$
of
$\Sigma $
that refines
$\Delta $
. Therefore by Lemma 3.8
(3), B is isomorphic to a subalgebra of
$\mathrm {P}_{\mathrm {o}}{(\Sigma ')}$
. By Lemma 4.8, there is
$k\in \mathbb N$
such that
$\Sigma ^{(k)}$
refines
$\Sigma '$
up to isomorphism. Hence by Lemma 3.8
(3) again,
$A^{(k)}$
contains a subalgebra isomorphic to
$\mathrm {P}_{\mathrm {o}}{(\Sigma ')}$
, and therefore also a subalgebra isomorphic to B. This completes the proof.
4.5 Nerves, subdivisions, and geometric realisations
The reason that Theorem 4.3 is relevant to the Nerve Criterion is the following classical connection between nerves of posets and derived subdivisions, which is deeply rooted in the work of Pavel S. Alexandrov.
Proposition 4.10. Let
$\Sigma $
be a simplicial complex, regarded as a poset under inclusion of faces. Then the barycentric subdivision of
$\Sigma $
is isomorphic as a poset to the nerve of
$\Sigma $
:
$$ \begin{align*} \operatorname{{\mathrm{Sd}}} \Sigma \cong \mathcal{N}(\Sigma). \end{align*} $$
Proof The proof flows readily from the definitions, and is in any case available from multiple sources (see, e.g., [Reference Alexandrov5, Chapter IV, Section 2.2] [Alexandrov’s own textbook treatment], or [Reference Maunder19, Proposition 2.5.10, p. 51], or [Reference Ranicki and Weiss24, Section 3]). Details are left to the reader.
Corollary 4.11. For P a polyhedron and
$\Sigma $
a triangulation of P we have
$$ \begin{align*} \operatorname{{\mathrm{Logic}}}(P) = \operatorname{{\mathrm{Logic}}}(\mathcal{N}^k(\Sigma) \mid k \in \mathbb N). \end{align*} $$
Proof Indeed
$$ \begin{align} \operatorname{{\mathrm{Logic}}}(P) &= \operatorname{{\mathrm{Logic}}}(\mathrm{Sub}_{\mathrm{o}} P) \nonumber \\ &= \operatorname{{\mathrm{Logic}}} (A \mid A\text{ finitely generated subalgebra of } \mathrm{Sub}_{\mathrm{o}} P) \end{align} $$
$$ \begin{align} &= \operatorname{{\mathrm{Logic}}}(\mathrm{P}_{\mathrm{o}}(\Sigma^{(k)}) \mid k \in \mathbb N)\qquad \end{align} $$
$$ \begin{align} &\hspace{-21pt}= \operatorname{{\mathrm{Logic}}}(\Sigma^{(k)} \mid k \in \mathbb N)\qquad\qquad\qquad\quad\ \ \ \end{align} $$
$$ \begin{align} &= \operatorname{{\mathrm{Logic}}}(\mathcal{N}^k(\Sigma) \mid k \in \mathbb N).\ \ \kern1pt \end{align} $$
In order to complete a proof of the Nerve Criterion, we will also need to use geometric realisations of finite posets via nerves, another classical tool. Let
$F = \{x_1, \ldots , x_m\}$
be a finite poset, and let
$e_1, \ldots , e_m$
be the standard basis vectors of
$\mathbb {R}^m$
. The set
can be proved to be a triangulation by elementary arguments; its underlying polyhedron
$\mathopen |\nabla F\mathclose |$
is the geometric realisation of F. For us, the key fact about geometric realisations is:
Lemma 4.12. Let F be a finite poset. The map
$\max \colon \mathcal {N}(F) \to F$
, which sends a chain to is maximum element, is a p-morphism, and
$\operatorname {{\mathrm {Logic}}}(\mathopen |\nabla F\mathclose |) \subseteq \operatorname {{\mathrm {Logic}}}(F)$
.
Proof The first statement is easy to verify by direct inspection, and a detailed proof was already given in [Reference Bezhanishvili, Marra, McNeill and Pedrini13, p. 389]. For the second statement, observe first that
$\nabla F$
and
$\mathcal {N}(F)$
are isomorphic as posets (under inclusion), by their definitions. Thus, by Proposition 2.1, the surjective p-morphism
$\nabla F \to F$
yields
$\operatorname {{\mathrm {Logic}}}(\nabla F)\subseteq \operatorname {{\mathrm {Logic}}}(F)$
. But
$\operatorname {{\mathrm {Up}}}(\nabla F)$
is a subalgebra of
$\mathrm {Sub}_{\mathrm {o}}(\mathopen |\nabla (F)\mathclose |)$
by Lemma 3.6 together with Lemma 3.3, so that
$\operatorname {{\mathrm {Logic}}}(\mathopen |\nabla F\mathclose |) \subseteq \operatorname {{\mathrm {Logic}}}(\nabla F) \subseteq \operatorname {{\mathrm {Logic}}}(F)$
, as was to be shown.
4.6 End of proof of the Nerve Criterion
Proof of Theorem 4.1, the Nerve Criterion.
Assume that
$\mathcal {L}$
is the logic of a class
$\mathbf {C}$
of polyhedra. For each
$P \in \mathbf {C}$
fix a triangulation
$\Sigma _P$
, and let
Then
$$ \begin{align} \operatorname{{\mathrm{Logic}}}(\mathbf{C}^*) &= \bigcap_{P \in \mathbf{C}}\operatorname{{\mathrm{Logic}}}(\mathcal{N}^k(\Sigma_P) \mid k \in \mathbb N)\nonumber \\ &= \bigcap_{p \in \mathbf{C}}\operatorname{{\mathrm{Logic}}}(P) \\ &= \operatorname{{\mathrm{Logic}}}(\mathbf{C}) = \mathcal{L}.\nonumber \end{align} $$
Conversely, assume that
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {D})$
, where
$\mathbf {D}$
is a class of finite frames closed under
$\mathcal {N}$
. Let
where
$\mathopen |\nabla (F)\mathclose |$
is the geometric realisation of F as in Section 4.5. We will show that
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {D}_*)$
. First suppose that
$\mathcal {L} \nvdash \phi $
, so that
$F \nvDash \phi $
for some
$F \in \mathbf {D}$
. Then we have that
$\mathopen |\nabla (F)\mathclose | \nvDash \phi $
, so that
$\operatorname {{\mathrm {Logic}}}(\mathbf {D}_*) \nvdash \phi $
. Conversely, suppose that
$\operatorname {{\mathrm {Logic}}}(\mathbf {D}_*) \nvdash \phi $
, so that
$\mathopen |\nabla (F)\mathclose | \nvDash \phi $
for some
$F \in \mathbf {D}$
. By definition
$\nabla (F)$
is a triangulation of
$\mathopen |\nabla (F)\mathclose |$
, and hence by Corollary 4.11 there is
$k \in \mathbb N$
such that
$\nabla (F)^{(k)} \nvDash \phi $
. But
$\nabla (F) \cong \mathcal {N}(F)$
by definition, and so by Proposition 4.10 we get
$\mathcal {N}^{k+1}(F) \cong \nabla (F)^{(k)}$
. Thus, as
$\mathbf {D}$
is closed under
$\mathcal {N}$
, we get that
$\mathcal {L} \nvdash \phi $
.
5 Polyhedrally incomplete logics
In this section, we apply the Nerve Criterion to show that every stable logic other than
$\mathbf {IPC}$
is polyhedrally incomplete. A logic
$\mathcal {L}$
is stable if
$\operatorname {{\mathrm {Frames}_{\bot }}}(\mathcal {L})$
is closed under monotone images. (We point out that the original definition of [Reference Bezhanishvili and Bezhanishvili10, Definition 6.6] used Esakia spaces. However, it can be shown that these definitions are equivalent [Reference Ilin18, Theorem 3.3.17].)
Proposition 5.1. The following well-known logicsFootnote 2 are all stable.
-
(i) The logic of weak excluded middle,
$\mathbf {KC} = \mathbf {IPC} + (\neg p \vee \neg \neg p)$
. -
(ii) Gödel–Dummett logic,
$\mathbf {LC} = \mathbf {IPC} + (p \rightarrow q) \vee (q \rightarrow p)$
. -
(iii)
$\mathbf {LC}_n = \mathbf {LC} + \mathbf {BD}_n$
. -
(iv) The logic of bounded width n,
$\mathbf {BW}_n = \mathbf {IPC} + \bigvee _{i=0}^n(p_i \rightarrow \bigvee _{j \neq i} p_j)$
. -
(v) The logic of bounded top width n, defined:
-
(vi) The logic of bounded cardinality n, defined:
Proof See [Reference Bezhanishvili and Bezhanishvili10, Theorem 7.3].
In fact:
Theorem 5.2. There are continuum-many stable logics.
Proof See [Reference Bezhanishvili and Bezhanishvili10, Theorem 6.13].
Theorem 5.3. Every stable logic has the finite model property.
Proof See [Reference Bezhanishvili and Bezhanishvili10, Theorem 6.8].
However, Theorem 5.3 notwithstanding:
Theorem 5.4. If
$\mathcal {L}$
is a stable logic other than
$\mathbf {IPC}$
, and
$\operatorname {{\mathrm {Frames}}}(\mathcal {L})$
contains a frame of height at least
$2$
, then
$\mathcal {L}$
is not polyhedrally complete.
Proof Let
$\mathcal {L}$
be a polyhedrally complete stable logic of height at least 2. We show that
$\mathcal {L} = \mathbf {IPC}$
.
By the Nerve Criterion 4.1, there is a class
$\mathbf {C}$
of finite frames closed under
$\mathcal {N}$
such that
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {C})$
. Since
$\operatorname {{\mathrm {Frames}}}(\mathcal {L})$
contains a frame of height at least
$2$
, we must have
$\mathcal {L} \nvdash \mathbf {BD}_1$
. Since
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {C})$
, there is therefore
$F \in \mathbf {C}$
such that
$\operatorname {\mathrm {\mathsf {height}}}(F) \geqslant 2$
. This means there are
$x_0, x_1, x_2 \in F$
with
$x_0 < x_1 < x_2$
. Without loss of generality, we may assume that
$x_2$
is a top element and that
$x_1$
is an immediate predecessor of
$x_2$
and
$x_0$
an immediate predecessor of
$x_1$
. Now, by assumption
$\mathcal {N}^k(F) \in \mathbf {C}$
for every
$k \in \mathbb N$
. Let us examine the structure of these frames a little. Note that
$\{x_0,x_1,x_2\}$
is a chain. Let X be a maximal chain in
$\Downarrow (x_0)$
. We have the following relations occurring in
$\mathcal {N}(F)$
.
Moreover, by assumptions on
$x_0, x_1, x_2$
and X, we have that
$X \cup \{x_0,x_1,x_2\}$
is a top element of
$\mathcal {N}(F)$
, with
$X \cup \{x_0,x_1\}$
and
$X \cup \{x_0,x_2\}$
immediate predecessors, and
$X \cup \{x_0\}$
an immediate predecessor of those. So, we may apply this argument once more, to obtain the following structure sitting at the top of
$\mathcal {N}^2(F)$
.
Iterating, we see that at the top of
$\mathcal {N}^k(F)$
we have the following structure.
Let z be the base element of this structure, as indicated. Now, take
$k \in \mathbb N$
and let
$\{t_1, \ldots , t_m\}$
be the top nodes of
$\mathcal {N}^k(F)$
produced by this construction, where
$m = 2^{k-1}$
. By Proposition 2.1,
${\Uparrow} (z) \in \operatorname {{\mathrm {Frames}_{\bot }}}(\mathcal {L})$
.
Let now G be an arbitrary poset with up to m elements
$\{y_1, \ldots , y_m\}$
(possibly with duplicates) plus a root
$\bot $
. Define
$f \colon {\Uparrow} (z) \to G$
as follows.
$$ \begin{align*} x \mapsto \left\{ \begin{array}{ll} y_i, & \text{if }x=t_i, \\ \bot, & \text{otherwise}. \end{array} \right. \end{align*} $$
Then f is monotonic. Since
$\mathcal {L}$
is stable, this means that
$G \in \operatorname {{\mathrm {Frames}_{\bot }}}(\mathcal {L})$
. Thus (since, by Proposition 2.6 and Corollary 2.2,
$\mathbf {IPC}$
is the logic of finite rooted frames) we get that
$\mathcal {L} = \mathbf {IPC}$
.
6 Polyhedrally complete logics: starlike completeness
In this section, we use the Nerve Criterion to establish a class of logics which are polyhedrally complete. This constitutes the second main result of the paper.
6.1 Starlike trees
A finite poset T is a tree if it has a root
$\bot $
, and every other
$x \in T \setminus \{\bot \}$
has exactly one immediate predecessor. A branch in T is a maximal chain. Say that T is a starlike tree if every
$x \in T \setminus \{\bot \}$
has at most one immediate successor. (The terminology ‘starlike’ comes from graph theory [see [Reference Watanabe and Schwenk33]].) A starlike tree is determined by the multiset of its branch heights, which motivates the following notation.
Let
$n_1, \ldots , n_k, m_1, \ldots , m_k \in \mathbb N^{>0}$
, with
$n_1, \ldots , n_k$
distinct. Then let us define
$T={\langle {n_1^{m_1} \cdots n_k^{m_k}} \rangle }$
as the starlike tree, uniquely determined to within an isomorphism, with the property that if we remove the root
$\bot $
we are left with exactly, for each i,
$m_i$
chains of length
$n_i$
. Let
${\langle {\epsilon } \rangle } = \bullet $
, the singleton poset. Call
$\alpha = n_1^{m_1} \cdots n_k^{m_k}$
(or
$\epsilon $
) the signature of T. We will always assume that
$n_1> n_2 > \cdots > n_k$
. See Figure 4 for some examples of starlike trees together with their signatures. We will sometimes write
$1^0$
for
$\epsilon $
.
Some examples of starlike trees.
The length of a signature
$\alpha = n_1^{m_1} \cdots n_k^{m_k}$
is defined as
. Let
. For
$j \leqslant \mathopen |\alpha \mathclose |$
, the jth height,
$\alpha (j)$
, is
$n_i$
, where
$$ \begin{align*} m_1 + \cdots + m_{i-1} \leqslant j < m_1 + \cdots + m_i. \end{align*} $$
Let
$\alpha $
and
$\beta $
be signatures. Say that
$\alpha \leqslant \beta $
if
$\mathopen |\alpha \mathclose | \leqslant \mathopen |\beta \mathclose |$
and for every
$j \leqslant \mathopen |\alpha \mathclose |$
we have
$\alpha (j) \leqslant \beta (j)$
. Considering the examples in Figure 4, we have the following relations:
$$ \begin{align*} 1^3 < 3 \cdot 1^2 < 3^2 \cdot 2 \cdot 1, \quad 2 < 3 \cdot 1^2. \end{align*} $$
Note that if
$\alpha = n_1^{m_1} \cdots n_k^{m_k}$
, we have
$\alpha \leqslant \beta $
if and only if
$\mathopen |\alpha \mathclose | \leqslant \mathopen |\beta \mathclose |$
and for every
$i \leqslant k$
, we have
$$ \begin{align*} \beta(m_1 + \cdots + m_i) \geqslant n_i. \end{align*} $$
Proposition 6.1. If
$\alpha \leqslant \beta $
then there is a p-morphism
${\langle {\beta } \rangle } \to {\langle {\alpha } \rangle }$
.
Proof We can realise
${\langle {\alpha } \rangle }$
as a downwards-closed subset of
${\langle {\beta } \rangle }$
. The p-morphism
$f \colon {\langle {\alpha } \rangle } \to {\langle {\beta } \rangle }$
is then defined as follows. First, f is the identity on
${\langle {\alpha } \rangle }$
. Second, for any branch of
${\langle {\beta } \rangle }$
which contains a branch of
${\langle {\alpha } \rangle }$
, we let f send any remaining elements to the maximum of the branch of
${\langle {\alpha } \rangle }$
. Finally, any remaining elements of
${\langle {\beta } \rangle }$
are mapped to the maximum element of some fixed branch in
${\langle {\alpha } \rangle }$
. A routine calculation shows that f is a p-morphism.
Note that the starlike tree
${\langle {k} \rangle }$
is the chain on
$k+1$
elements; we will use this notation for chains from now on. We will write the signature as
$k^1$
, to disambiguate it from k as a number. For
$k \in \mathbb N^{>0}$
, the k-fork is the starlike tree
${\langle {1^k} \rangle }$
.
6.2 Starlike logics
We are now in a position to define the principal class of logics that will be investigated in this section. Let
. Take
$\Lambda \subseteq \mathcal S$
(possibly infinite). The starlike logic
$\mathbf {SFL}(\Lambda )$
based on
$\Lambda $
is the logic axiomatised by
$\mathbf {IPC}$
plus
$\chi ({\langle {\alpha } \rangle })$
for each
$\alpha \in \Lambda $
. Write
$\mathbf {SFL}(\alpha _1, \ldots , \alpha _k)$
for
$\mathbf {SFL}(\{\alpha _1, \ldots , \alpha _k\})$
.
Remark 6.2. For an explanation as to why the difork
${\langle {1^2} \rangle }$
is omitted, see Proposition 6.22 and the preceding discussion.
Proposition 6.3.
$\mathbf {SL} = \mathbf {SFL}(2 \cdot 1)$
. So Scott’s Logic is a starlike logic.
Proof See [Reference Chagrov and Zakharyaschev14, Section 9 and Table 9.7, p. 317].
Let us examine what
$\mathbf {SFL}(\Lambda )$
‘means’ in terms of its class of frames. The formula
$\chi ({\langle {\alpha } \rangle })$
turns out to express a kind of connectedness property. We make this precise using the following definitions.
Let F be a finite poset. A path in F is a sequence
$p=x_0\cdots x_k$
of elements of F such that for each i we have
$x_i < x_{i+1}$
or
$x_i> x_{i+1}$
. Write
$p \colon x_0 \rightsquigarrow x_k$
. The path p is closed if
$x_0=x_k$
. The poset F is path-connected if between any two points there is a path.
Lemma 6.4. A poset is path-connected if, and only if, it is connected as a topological space.
Proof See [Reference Bezhanishvili and Gabelaia11, Lemma 3.4].
A connected component of F is a subposet
$U \subseteq F$
which is connected as a topological subspace and is such that there is no connected V with
$U \subset V$
.
Lemma 6.5. Let F be a poset.
-
(1) The connected components of F partition F.
-
(2) The connected components of F are downwards-closed and upwards-closed.
Proof These results follow straightforwardly from the fact that by Lemma 6.4 the connected components are exactly the equivalence classes under the relation ‘there is a path from x to y’.
Define
$\mathrm {ConComps}(F)$
to be the set of connected components of F. The connectedness type
$\mathrm {ConType}(F)$
of F is the signature
$n_1^{m_1} \cdots n_k^{m_k}$
such that
$\mathrm {ConComps}(F)$
contains for each i exactly
$m_i$
sets of height
$n_i-1$
, and nothing else. Let
.
Remark 6.6. Note that when F is connected,
$\mathrm {ConType}(F)=n+1$
, where
$n = \operatorname {\mathrm {\mathsf {height}}}(F)$
.
Let
$\alpha> \epsilon $
be a signature. An
$\alpha $
-partition of F is an open partition in which the number and heights of the connected components are specified by
$\alpha $
. In other words, it is a partition:
$$ \begin{align*} F = C_1 \sqcup \cdots \sqcup C_{\mathopen|\alpha\mathclose|} \end{align*} $$
into open sets such that
$C_j$
has height at least
$\alpha (j)-1$
. For notational uniformity, say that F has an
$\epsilon $
-partition if
$F=\varnothing $
. The following lemma is a straightforward consequence of the definitions.
Lemma 6.7. A finite poset F has an
$\alpha $
-partition if and only if
$\alpha \leqslant \mathrm {ConType}(F)$
.
Corollary 6.8. When F is connected, F has an
$\alpha $
-partition if and only if
$\alpha = k^1$
, where
$k \leqslant \operatorname {\mathrm {\mathsf {height}}}(F)+1$
.Footnote
3
Let F be a poset and
$\alpha $
be a signature. F is
$\alpha $
-connected if there is no
$x \in F$
such that there is an
$\alpha $
-partition of
${\Uparrow} (x)$
. By Lemma 6.7, this is equivalent to requiring that
$\alpha \not \leqslant \mathrm {ConType}({\Uparrow} (x))$
for each
$x \in F$
.
We can now express the meaning of
$\chi ({\langle {\alpha } \rangle })$
on frames.
Theorem 6.9. For F a finite poset and
$\alpha $
any signature,
$F \vDash \chi ({\langle {\alpha } \rangle })$
if and only if F is
$\alpha $
-connected.
To prove this result, we make use of the following slight strengthening of Theorem 2.4. Let F and Q be finite posets, and assume that Q has root
$\bot $
. An up-reduction
$f \colon F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} Q$
is pointed with apex
$x \in F$
if we have
$\mathrm {dom}(f) = {\uparrow }(x)$
and
${f}^{-1}\{\bot \} = \{x\}$
.
Lemma 6.10. If there is an up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} Q$
then there is a pointed up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} Q$
.
Proof Take
$f \colon F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} Q$
, and choose
$x \in {f}^{-1}\{\bot \}$
maximal. Then
$f |_{{\uparrow }(x)}$
is still a p-morphism, and is moreover a pointed up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} Q$
.
Corollary 6.11. Let
$F, Q$
be finite posets, with Q rooted. Then
$F \vDash \chi (Q)$
if and only if there is no pointed up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} Q$
.
Proof of Theorem 6.9
Assume that
$F \nvDash \chi ({\langle {\alpha } \rangle })$
. Then by Corollary 6.11 there is a pointed up-reduction
$f \colon F \to {\langle {\alpha } \rangle }$
with apex x. This means that
${f}^{-1}[{\langle {\alpha } \rangle } \setminus \{\bot \}] = {\Uparrow} (x)$
. Let
$C_j$
be the preimage of the jth branch of
${\langle {\alpha } \rangle } \setminus \{\bot \}$
under f, for each
$j \leqslant \mathopen |\alpha \mathclose |$
. Since f is a p-morphism,
$C_j$
is upwards-closed. Note that the
$C_j$
’s are disjoint and hence they form an open partition of
${\Uparrow} (x)$
. Now, since
$C_j$
is the preimage of a chain of length
$\alpha (j)$
, we can find a chain of the same length inside
$C_j$
. From this it follows that
$C_j$
has height at least
$\alpha (j)-1$
. But then
$(C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
is an
$\alpha $
-partition of
${\Uparrow} (x)$
, meaning that F is not
$\alpha $
-connected.
Conversely, assume that F is not
$\alpha $
-connected, so that there is
$x \in F$
and an
$\alpha $
-partition
$(C_j \mid j \leqslant k)$
of
${\Uparrow} (x)$
. For each
$C_j$
, we have, by definition, that
$\operatorname {\mathrm {\mathsf {height}}}(C_j) \geqslant \alpha (j)-1$
. Hence by Proposition 2.7 there is a p-morphism
$f_j \colon C_j \to {\langle {\alpha (j)-1} \rangle }$
. Define
$f \colon {\uparrow }(x) \to {\langle {\alpha } \rangle }$
as follows:
$$ \begin{align*} y \mapsto \left\{ \begin{array}{ll} \bot, & \text{if }y = x, \\ f_j(y), & \text{if }y \in C_j. \end{array} \right. \end{align*} $$
Then f is a p-morphism, so an up-reduction
$F {\mathrel {{\circ }\mkern -3mu{\rightarrow }}} {\langle {\alpha } \rangle }$
.
Remark 6.12. In particular it follows that
$\mathbf {BD}_n = \mathbf {IPC} + \chi ({\langle {n+1} \rangle })$
. This is just Proposition 2.7 of course.
The last matter to resolve before moving on to consider the completeness of starlike logics is their number. For this we make use of Higman’s Lemma. A quasi-well-order is a preorder which is well-founded and has no infinite antichain. Given a preorder I, let
$I^{<\omega }$
be the set of finite sequences of elements of I ordered by
$(x_1, \ldots , x_n) \leqslant (y_1, \ldots , y_m)$
if and only if there is
$f \colon \{1, \ldots n\} \to \{1,\ldots ,m\}$
injective such that for each
$k \leqslant n$
we have
$x_k \leqslant y_{f(k)}$
.
Lemma 6.13 (Higman’s Lemma [Reference Higman17]).
If I is a quasi-well-order then so is
$I^{<\omega }$
.
Proposition 6.14.
-
(1) Every starlike logic is finitely axiomatizable.
-
(2) There are exactly countably many starlike logics.
Proof
-
(1) As every starlike logic is axiomatizable by Jankov formulas of starlike trees, it suffices to show that there is no infinite antichain of starlike trees with respect to p-morphic reduction. In light of Proposition 6.1, it therefore suffices to show that there is no infinite antichain of signatures with respect to the ordering defined on them. Now, we can recast signatures as (monotonic decreasing) finite sequences of integers. Indeed, the signature
$\alpha $
is determined by the sequence
$(\alpha (1), \ldots , \alpha (\mathopen |\alpha \mathclose |))$
. In this way, the set of signatures is seen to be a suborder of
$\omega ^{<\omega }$
. Now,
$(\omega , \leqslant )$
is clearly a quasi-well-order, and hence by Higman’s Lemma 6.13, so is
$\omega ^{<\omega }$
. Thus there is no infinite antichain of signatures, as required. -
(2) The result follows from (1) as there are only countably many finitely axiomatizable logics.
6.3 Starlike completeness
The main theorem to be proved in this section is the following.
Theorem 6.15. Every starlike logic is polyhedrally complete.
As an immediate consequence, we obtain:
Corollary 6.16. Scott’s Logic is polyhedrally complete.
Remark 6.17. The starlike logic
$\mathbf {SFL}(2 \cdot 1, 1^3)$
is particularly important geometrically. In [Reference Adam-Day, Bezhanishvili, Gabelaia and Marra2], it is shown that this is the logic of all convex polyhedra.
In order to prove Theorem 6.15, we introduce the following new validity concept on frames. Let F be a poset and
$\phi $
be a formula. F nerve-validates
$\phi $
, notation
$F \mathrel {{\vDash }_{\mathcal {N}}} \phi $
, if for every
$k \in \mathbb N$
we have
$\mathcal {N}^k(F) \vDash \phi $
.
Remark 6.18. Since for every G we have the p-morphism
$\max \colon \mathcal {N}(G) \to G$
(see Lemma 4.12), by Proposition 2.1 this is equivalent to requiring that
$\mathcal {N}^k(F) \vDash \phi $
for infinitely many
$k \in \mathbb N$
.
Lemma 6.19. A logic
$\mathcal {L}$
is polyhedrally complete if and only if it has the finite model property and every rooted finite frame of
$\mathcal {L}$
is the up-reduction of a poset which nerve-validates
$\mathcal {L}$
.
Proof Assume that
$\mathcal {L}$
is polyhedrally complete. Then by the Nerve Criterion 4.1 it is the logic of a class
$\mathbf {C}$
of finite frames which is closed under
$\mathcal {N}$
, and so has the fmp. Then by Corollary 2.5, every finite rooted frame F of
$\mathcal {L}$
is the up-reduction of some
$F' \in \mathbf {C}$
. Since
$\mathbf {C} \subseteq \operatorname {{\mathrm {Frames}}}(\mathcal {L})$
and is closed under
$\mathcal {N}$
, such an
$F'$
nerve-validates
$\mathcal {L}$
.
Conversely, let
$\mathbf {C}$
be the class of all finite rooted frames which nerve-validate
$\mathcal {L}$
. Note that
$\mathbf {C}$
is closed under
$\mathcal {N}$
. Further, clearly
$\mathcal {L} \subseteq \operatorname {{\mathrm {Logic}}}(\mathbf {C})$
. To see the reverse inclusion, suppose that
$\mathcal {L} \nvdash \phi $
. Since
$\mathcal {L}$
has the fmp, there is
$F \in \operatorname {{\mathrm {Frames}_{\bot ,\mathrm {fin}}}}(\mathcal {L})$
such that
$F \nvDash \phi $
. By assumption, F is the up-reduction of
$F' \in \mathbf {C}$
. Then by Proposition 2.1,
$F' \nvDash \phi $
, meaning that
$\operatorname {{\mathrm {Logic}}}(\mathbf {C}) \nvdash \phi $
.
Lemma 6.20. Every starlike logic has the finite model property.
Proof In [Reference Zakharyaschev34, Corollary 0.11], Zakharyaschev shows that every logic axiomatised by the Jankov–Fine formulas of trees has the finite model property.
Now, as every finitely axiomatizable logic with the finite model property is decidable we obtain from Proposition 6.14 (1) and Lemma 6.20 the following.
Corollary 6.21. Every starlike logic is decidable.
With Lemma 6.20, we can now use Lemma 6.19 to produce a proof of Theorem 6.15. Given a rooted finite frame F of
$\mathbf {SFL}(\Lambda )$
, we proceed as follows.
-
(1) We examine what it means for a frame to nerve-validate
$\chi ({\langle {\alpha } \rangle })$
. -
(2) We see that it can be assumed that F is graded (a structural property of posets defined below).
-
(3) Using this additional structure, we construct a frame
$F'$
and the p-morphism
$F' \to F$
, with the property that
$F' \mathrel {{\vDash }_{\mathcal {N}}} \mathbf {SFL}(\Lambda )$
.
The reader will have noticed that the difork
${\langle {1^2} \rangle }$
is omitted from the definition of a starlike logic, and consequently from Theorem 6.15. In fact, polyhedral semantics is quite fond of this tree: when we take it as a forbidden configuration, the resulting landscape of polyhedrally complete logics is as sparse as possible, as is shown below.
Proposition 6.22. Let
$\mathcal {L}$
be a polyhedrally complete logic containing
$\mathbf {SFL}(1^2)$
. Then
$\mathcal {L} = \mathbf {CPC}$
, the maximum logic.
Proof Suppose for a contradiction that
$\mathcal {L}$
is a polyhedrally complete logic containing
$\mathbf {SFL}(1^2)$
other than
$\mathbf {CPC}$
. By the Nerve Criterion 4.1,
$\mathcal {L} = \operatorname {{\mathrm {Logic}}}(\mathbf {C})$
where
$\mathbf {C}$
is a class of finite posets closed under
$\mathcal {N}$
. Since
$\mathcal {L} \neq \mathbf {CPC}$
, there must be
$F \in \mathbf {C}$
with
$\operatorname {\mathrm {\mathsf {height}}}(F) \geqslant 1$
. This means that F has a chain
$x_0 < x_1$
. As in the proof of Theorem 5.4, we may assume that
$x_1$
is a top element of F and that
$x_0$
is an immediate predecessor of
$x_1$
. Take X a maximal chain in
$\Downarrow (x_0)$
. Then, as in that proof, we obtain the following structure lying at the top of
$\mathcal {N}(F)$
.
Applying the nerve once more, we obtain the following structure at the top of
$\mathcal {N}^2(F)$
.
Since
$\mathbf {C}$
is closed under
$\mathcal {N}$
, we get that
$\mathcal {N}^2(F) \in \operatorname {{\mathrm {Frames}}}(\mathcal {L})$
. But
${\uparrow}(Z)$
maps p-morphically onto
${\langle {1^2} \rangle }$
, contradicting that
$\mathcal {L} \vdash \chi ({\langle {1^2} \rangle })$
. #
We now proceed with the proof of Theorem 6.15.
6.4 Nerve-validation
While validating
$\chi ({\langle {\alpha } \rangle })$
corresponds to
$\alpha $
-connectedness (as shown in Theorem 6.9), nerve-validating
$\chi ({\langle {\alpha } \rangle })$
corresponds to
$\alpha $
-nerve-connectedness. Let F be a poset and
$x<y$
in F. The diamond and strict diamond of x and y are defined, respectively:
A poset F is
$\alpha $
-diamond-connected if there are no
$x < y$
in F such that there is an
$\alpha $
-partition of
${\Updownarrow} (x,y)$
. The poset F is
$\alpha $
-nerve-connected if it is
$\alpha $
-connected and
$\alpha $
-diamond-connected.
With a slight conceptual change,
$\alpha $
-connectedness and
$\alpha $
-diamond-connectedness can be harmonised as follows. For any poset F, we take a new element
$\infty $
, and let
, where
$\infty $
lies above every element of F. Then F is
$\alpha $
-nerve-connected if and only if there are no
$x < y$
in
$\check F$
for which there is an
$\alpha $
-partition of
${\Updownarrow} (x,y)$
.
The following result shows that
$\alpha $
-nerve-connectedness is exactly the notion we want.
Theorem 6.23. Let F be a finite poset and take
$\alpha \in \mathcal S$
. Then
$F \mathrel {{\vDash }_{\mathcal {N}}} \chi ({\langle {\alpha } \rangle })$
if and only if F is
$\alpha $
-nerve-connected.
Proof Assume that F is not
$\alpha $
-nerve-connected with the aim of showing
$F \mathrel {{\nvDash }_{\mathcal {N}}} \chi ({\langle {\alpha } \rangle })$
. Choose
$x<y$
in
$\check F$
such that
${\Updownarrow} (x,y)$
has an
$\alpha $
-partition. That is, there is an open partition
$(C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
of
${\Updownarrow} (x,y)$
such that
$\operatorname {\mathrm {\mathsf {height}}}(C_j) = \alpha (j)$
. Choose a chain
$X \subseteq F$
such that:
-
(i)
$x,y \in X \cup \{\infty \}$
, and -
(ii)
$X \cap {\Updownarrow} (x,y) = \varnothing $
,
which is moreover maximal with respect to these requirements. We will show that
${\Uparrow} (X)^{\mathcal {N}(F)}$
has an
$\alpha $
-partition. Note that by maximality of X, elements
$Y \in {\Uparrow} (X)^{\mathcal {N}(F)}$
are determined by their intersection
$Y \cap {\Updownarrow}(x,y)$
. For
$j \leqslant \mathopen |\alpha \mathclose |$
, let
Take
$j,l \leqslant \mathopen |\alpha \mathclose |$
distinct. Since both
$C_j$
and
$C_l$
are upwards- and downwards-closed in
${\Updownarrow} (x,y)$
, there is no chain
$Y \in {\Uparrow} (X)^{\mathcal {N}(F)}$
such that
$Y \cap C_j \neq \varnothing $
and
$Y \cap C_l \neq \varnothing $
. This means that
-
(1)
$\widehat C_j$
and
$\widehat C_l$
are disjoint. -
(2) For any
$Y \in {\Uparrow} (X)^{\mathcal {N}(F)}$
we have
$Y \in \widehat C_j$
if and only if
$Y \cap {\Updownarrow} (x,y) \subseteq C_j$
. Hence each
$\widehat C_j$
is upwards- and downwards-closed in
${\Uparrow} (X)^{\mathcal {N}(F)}$
.
Furthermore, since
$(C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
covers
${\Updownarrow} (x,y)$
, we get that
$(\widehat C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
covers
${\Uparrow} (X)^{\mathcal {N}(F)}$
. Finally, any maximal chain in
$\widehat C_j$
is a sequence of chains
$Y_0 \subset \cdots \subset Y_l$
such that
$\mathopen |Y_{i+1} \setminus Y_i\mathclose | = 1$
; this then corresponds to a maximal chain in
$C_j$
. Therefore
$$ \begin{align*} \operatorname{\mathrm{\mathsf{height}}}(\widehat C_j) = \operatorname{\mathrm{\mathsf{height}}}(C_j). \end{align*} $$
Ergo
$(\widehat C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
is an
$\alpha $
-partition of
${\Uparrow} (X)^{\mathcal {N}(F)}$
, meaning that
$\mathcal {N}(F)$
is not
$\alpha $
-connected. Then, by Theorem 6.9,
$\mathcal {N}(F) \nvDash \chi ({\langle {\alpha } \rangle })$
, hence by definition
$F \mathrel {{\nvDash }_{\mathcal {N}}} \chi ({\langle {\alpha } \rangle })$
.
For the converse direction, we will show that if F is
$\alpha $
-nerve-connected, then so is
$\mathcal {N}(F)$
, which will give the result by induction (note that
$\alpha $
-nerve-connectedness is stronger than
$\alpha $
-connectedness, and hence by Theorem 6.9 if
$\mathcal {N}^k(F)$
is
$\alpha $
-nerve-connected then
$\mathcal {N}^k(F) \vDash \chi ({\langle {\alpha } \rangle })$
). So assume that F is
$\alpha $
-nerve-connected. We will first prove
$\alpha $
-connectedness. Take
$X \in \mathcal {N}(F)$
with the aim of showing that
${\Uparrow} (X)^{\mathcal {N}(F)}$
has no
$\alpha $
-partition.
Firstly, assume that X has more than one ‘gap’; that is, there are distinct
$w_1,w_2 \in F \setminus X$
such that
$X \cup \{w_1\}$
and
$X \cup \{w_2\}$
are still chains, but such that there exists
$z \in X$
with
$w_1 < z < w_2$
. Take
$Y,Z \in {\Uparrow} (X)^{\mathcal {N}(F)}$
. We will use the two gaps to juggle elements between the two sets so as to provide a path
$Y \rightsquigarrow Z$
which never touches X (i.e., lies in
${\Uparrow} (X)^{\mathcal {N}(F)}$
). For
$i \in \{1,2\}$
, let
$u_i \in X \cap \Downarrow ({w_i})$
be greatest and
$v_i \in X \cap {\Uparrow} (w_i)$
be least. See Figure 5 for a representation of the situation. Now, without loss of generality, we may assume that
$Y \cap {\Updownarrow} (u_1,v_1) \neq \varnothing $
(we may add
$w_1$
to Y, noting that
$w_1 \in {\Updownarrow} (u_1,v_1)$
). Similarly, we may assume that
$Y \cap {\Updownarrow} (u_2,v_2) \neq \varnothing $
, and likewise for Z. We then have the following path in
${\Uparrow} (X)^{\mathcal {N}(F)}$
(note that some of the sets along the path may be equal, but in all cases the path is still there):
Here, the gap
${\Updownarrow} (u_2,v_2)$
is used to ensure that
$Y \setminus {\Updownarrow} (u_1,v_1)$
and
$Z \setminus {\Updownarrow} (u_1,v_1)$
are not equal to X, and the fact that we have
$v_1 \leqslant z \leqslant u_2$
ensures that all these sets are indeed in
$\mathcal {N}(F)$
. Hence,
${\Uparrow} (X)^{\mathcal {N}(F)}$
is path-connected so connected. Therefore, by Corollary 6.8, it suffices to show that
$\operatorname {\mathrm {\mathsf {height}}}({\Uparrow} (X)^{\mathcal {N}(F)}) < \operatorname {\mathrm {\mathsf {height}}}(F)$
. But this is immediate from the definition of
$\mathcal {N}$
.
The set-up when X has more than one gap.
Hence we may assume that X has exactly one gap (when X has no gaps,
${\Uparrow} (X)^{\mathcal {N}(F)} = \varnothing $
). This means that there are
$x,y \in X$
with
$x<y$
such that
$X \cap {\Updownarrow} (x,y) = \varnothing $
and X is maximal outside of
${\Updownarrow} (x,y)$
. As before then, elements
$Y \in {\Uparrow} (X)^{\mathcal {N}(F)}$
are determined by their intersection
$Y \cap {\Updownarrow} (x,y)$
. Suppose that
${\Uparrow} (X)^{\mathcal {N}(F)}$
has an
$\alpha $
-partition
$(\widehat C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
. For each
$j \leqslant \mathopen |\alpha \mathclose |$
, let
Note that
$\bigcup _{j \leqslant \mathopen |\alpha \mathclose |}C_j = {\Updownarrow} (x,y)$
. For each
$j \leqslant \mathopen |\alpha \mathclose |$
, since
$\widehat C_j$
is downwards-closed, we have that, for
$z \in {\Updownarrow} (x,y)$
,
$$ \begin{align*} z \in C_j \quad\Leftrightarrow\quad \exists Y \in \widehat C_j \colon z \in Y \quad\Leftrightarrow\quad X \cup \{z\} \in \widehat C_j. \end{align*} $$
This means in particular that the
$C_j$
’s are pairwise disjoint. Further, if
$z \in C_j$
and
$w \in {\Updownarrow} (x,y)$
with
$w < z$
, then
$X \cup \{w,z\}$
is a chain, and so as
$\widehat C_j$
is upwards-closed, we have
$X \cup \{w,z\} \in \widehat C_j$
, meaning that
$w \in C_j$
; similarly when
$w> z$
. Whence each
$C_j$
is upwards- and downwards-closed. Finally, as above, maximal chains in
$\widehat C_j$
correspond to maximal chains in
$C_j$
of the same length, whence
$$ \begin{align*} \operatorname{\mathrm{\mathsf{height}}}(\widehat C_j) = \operatorname{\mathrm{\mathsf{height}}}(C_j). \end{align*} $$
But then
$(C_j \mid j \leqslant \mathopen |\alpha \mathclose |)$
is an
$\alpha $
-partition of
${\Updownarrow} (x,y)$
, contradicting the fact that F is
$\alpha $
-nerve-connected. #
This shows that
$\mathcal {N}(F)$
is
$\alpha $
-connected. What about
$\alpha $
-diamond-connectedness? In fact we can show this without using any assumptions on F. Take
$X,Y \in \mathcal {N}(F)$
with
$X \subset Y$
. We will show that
${\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
has no
$\alpha $
-partition. We may assume that
$\mathopen |Y \setminus X\mathclose | \geqslant 2$
, otherwise
${\Updownarrow} (X,Y)^{\mathcal {N}(F)} = \varnothing $
. Note that this means in particular that
$\alpha> 1$
, since F is
$\alpha $
-connected. If
$\mathopen |Y \setminus X\mathclose | = 2$
, then
${\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
is the antichain on two elements, which, since
$\alpha \neq 1^2$
by assumption, has no
$\alpha $
-partition. So assume that
$\mathopen |Y \setminus X\mathclose | \geqslant 3$
; we will show that in fact
${\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
is connected. Take distinct
$Z,W \in {\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
. Choose
$z \in Z \setminus X$
and
$w \in W \setminus X$
. Since
$\mathopen |Y \setminus X\mathclose | \geqslant 3$
, we have that
$X \cup \{z,w\} \in {\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
. Hence the following is a path in
${\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
:
Therefore,
${\Updownarrow} (X,Y)^{\mathcal {N}(F)}$
is connected. Finally, note that
$$ \begin{align*} \operatorname{\mathrm{\mathsf{height}}}({\Updownarrow} (X,Y)^{\mathcal{N}(F)}) \leqslant \operatorname{\mathrm{\mathsf{height}}}(\mathcal{N}(F)) = \operatorname{\mathrm{\mathsf{height}}}(F). \\[-34pt] \end{align*} $$
Remark 6.24. Note that the proof shows an interesting property of the formulas
$\chi ({\langle {\alpha } \rangle })$
: we have
$F \mathrel {{\vDash }_{\mathcal {N}}} \chi ({\langle {\alpha } \rangle })$
if and only if
$\mathcal {N}(F) \vDash \chi ({\langle {\alpha } \rangle })$
. This is not true in general. For example, formulas expressing bounded width can take many iterations of the nerve construction to become falsified.
6.5 Graded posets
The next step is to show that we can put
$F \in \operatorname {{\mathrm {Frames}_{\bot ,\mathrm {fin}}}}(\mathbf {SFL}(\Lambda ))$
into a special form. The following definition comes from combinatorics (see, e.g., [Reference Stanley29, p. 99]).
Definition 6.25 (Graded poset).
A rank function on a poset F is a map
$\rho \colon F \to \mathbb N$
such that:
-
(i) whenever x is minimal in F, we have
$\rho (x)=0$
, -
(ii) whenever y is the immediate successor of x, we have
$\rho (y)=\rho (x)+1$
.
If F is non-empty and has a rank function, then it is graded.
The notion of gradedness has a strong visual connection. When a poset is graded, we can draw it out in well-defined layers such that any element’s immediate successors lie entirely in the next layer up.
Lemma 6.26. Let F be a finite poset.
-
(1) F is graded if and only if for every
$x \in F$
, all maximal chains in
$\downarrow (x)$
have the same length. -
(2) When F is graded,
$\rho (x) = \operatorname {\mathrm {\mathsf {height}}}(x)$
for every
$x \in F$
, and
$\operatorname {\mathrm {\mathsf {height}}}(F) = \max \rho [F]$
. -
(3) Rank functions, when they exist, are unique.
Proof
-
(1) See [Reference Stanley29, p. 99]. Assume that F is graded, and take X a maximal chain in
$\downarrow (x)$
for some
$x \in F$
. Let
$k = \rho (x)$
. We will show that
$\mathopen |X\mathclose | = k+1$
. Since X is a chain, the ranks of each of its elements are distinct. Since X is maximal,
$x \in X$
. Suppose for a contradiction that there is
$j < k$
such that there is no
$x \in X$
of rank j. We may assume that j is minimal with this property. We can’t have
$j=0$
, since otherwise X wouldn’t contain any minimal element, so wouldn’t be a maximal chain. Hence, there is
$y \in X$
with
$\rho (y) = j-1$
. Let z be next in X after y. Then y has an immediate successor w such that
$w \leqslant z$
. By definition,
$\rho (w) = j$
, so
$w \notin X$
. But
$X \cup \{w\}$
is a chain, contradicting the maximality of X. # Therefore,
$\mathopen |X\mathclose | = k+1$
.Conversely, define
$\rho \colon F \to \mathbb N$
by
$$ \begin{align*} x \mapsto \operatorname{\mathrm{\mathsf{height}}}(x). \end{align*} $$
Let us check that
$\rho $
is a rank function.-
(i) Clearly, when x is minimal,
$\rho (x) = 0$
. -
(ii) Suppose for a contradiction that there are
$x, y \in F$
, with y an immediate successor of x, such that
$\rho (y) \neq \rho (x) + 1$
. First, by definition,
$\rho (y)> \rho (x)$
, so we must have
$\rho (y)> \rho (x) + 1$
. Choose maximal chains
$X \subseteq \downarrow (x)$
,
$Y \subseteq \downarrow (y)$
. Note that by assumption
$$ \begin{align*} \mathopen|Y\mathclose|> \mathopen|X\mathclose| + 1. \end{align*} $$
But now, since y is an immediate successor of x, both
$X \cup \{y\}$
and Y are maximal chains in
$\downarrow (y)$
of different heights. #
-
-
(2) This follows from the proof of (1).
-
(3) This follows from (2).
Corollary 6.27.
-
(1) Every tree is graded.
-
(2) For any finite poset F, its nerve
$\mathcal {N}(F)$
is graded, with rank function given by
$\rho (X) = \mathopen |X\mathclose |-1$
.
Proof For (2), note that for any
$X \in \mathcal {N}(F)$
we have
$\operatorname {\mathrm {\mathsf {height}}}(X) = \mathopen |X\mathclose |-1$
.
What we will show in the proceeding two subsections is that any frame
$\mathbf {SFL}(\Lambda )$
can be assumed to be graded. In other words, we prove the following ‘gradification’ theorem.
Theorem 6.28. Take
$\Lambda \subseteq \mathcal S$
and let F be a finite rooted poset such that
$F \vDash \mathbf {SFL}(\Lambda )$
. Then there is a finite graded rooted poset
$F'$
and a p-morphism
$f \colon F' \to F$
such that
$F' \vDash \mathbf {SFL}(\Lambda )$
.
The proof of the theorem works differently depending on whether we have Scott’s tree
${\langle {2\cdot 1} \rangle }$
present. Theorem 6.29 deals with the case
$2 \cdot 1 \in \Lambda $
, while Theorem 6.33 deals with the case
$2 \cdot 1 \notin \Lambda $
.
6.6 Gradification in the presence of Scott’s tree
Let us first consider the gradification theorem in the case
$2 \cdot 1 \in \Lambda $
.
Theorem 6.29. Let
$\Lambda \subseteq \mathcal S$
be such that
$2 \cdot 1 \in \Lambda $
. Let F be a finite rooted poset such that
$F \vDash \mathbf {SFL}(\Lambda )$
. Then there is a finite graded rooted poset
$F'$
and a p-morphism
$f \colon F' \to F$
such that
$F' \vDash \mathbf {SFL}(\Lambda )$
.
To begin with, the following lemmas show us that this case is not too complicated.
Lemma 6.30. Take
$\Lambda \subseteq \mathcal S$
such that
$2\cdot 1 \in \Lambda $
but
$n \notin \Lambda $
for any
$n \in \mathbb N$
.
-
(1) If there is no
$k \in \mathbb N^{>0}$
such that
$1^k \in \Lambda $
, then
$\mathbf {SFL}(\Lambda ) = \mathbf {SFL}(2 \cdot 1)$
. -
(2) Otherwise, let
$k \in \mathbb N^{>0}$
be minimal such that
$1^k \in \Lambda $
. Then
$\mathbf {SFL}(\Lambda ) = \mathbf {SFL}(2 \cdot 1,1^k)$
.
Proof
-
(1) Take
$\alpha \in \Lambda $
. Then by assumption
$\alpha (1) \geqslant {2}$
, and hence, as
$\alpha \neq n$
, we have
${2 \cdot 1} \leqslant \alpha $
. Then by Proposition 6.1 there is a p-morphism
${\langle {\alpha } \rangle } \to {\langle {2 \cdot 1} \rangle }$
. Hence by the semantic meaning of Jankov–Fine formulas, Theorem 2.4, we have that any frame validating
$\chi ({\langle {2 \cdot 1} \rangle })$
will also validate
$\chi ({\langle {\alpha } \rangle })$
. This means that
$\mathbf {SFL}(\Lambda ) \subseteq \mathbf {SFL}(2 \cdot 1)$
. The converse direction is immediate. -
(2) Take
$\alpha \in \Lambda $
. If
$\alpha (1) \geqslant 2$
then by Proposition 6.1 there is a p-morphism
${\langle {\alpha } \rangle } \to {\langle {2 \cdot 1} \rangle }$
. Assume that
$\alpha (1) \not \geqslant 2$
. Since
$\alpha \neq \epsilon $
, we have
$\alpha (1)=1$
, meaning that
$\alpha =1^l$
for some
$l \in \mathbb N^{>0}$
. By assumption
$k \leqslant l$
. But then
$1^k \leqslant \alpha $
, giving that there is a p-morphism
${\langle {\alpha } \rangle } \to {\langle {1^k} \rangle }$
. It follows that for any
$\alpha \in \Lambda $
,
${\langle {\alpha } \rangle }$
up-reduces to either
${\langle {2 \cdot 1} \rangle }$
or
${\langle {1^k} \rangle }$
. By Theorem 2.4, any frame validating
$\chi ({\langle {2 \cdot 1} \rangle })$
and
$\chi ({\langle {1^k} \rangle })$
will also validate
$\chi ({\langle {\alpha } \rangle })$
. This implies that
$\mathbf {SFL}(\Lambda ) \subseteq \mathbf {SFL}(2 \cdot 1,1^k)$
. The converse direction is obvious.
Corollary 6.31. Take
$\Lambda \subseteq \mathcal S$
such that
$2\cdot 1 \in \Lambda $
and there is
$n \in \mathbb N$
with
$n \in \Lambda $
; assume that n is the minimal such natural number.
-
(1) If there is no
$k \in \mathbb N^{>0}$
such that
$1^k \in \Lambda $
, then
$\mathbf {SFL}(\Lambda ) = \mathbf {SFL}(n, 2 \cdot 1)$
. -
(2) Otherwise, let
$k \in \mathbb N^{>0}$
be minimal with
$1^k \in \Lambda $
. Then
$\mathbf {SFL}(\Lambda ) = \mathbf {SFL}(n, 2 \cdot 1,1^k)$
.
Proof This follows from Lemma 6.30 and the fact that when
$n_1 < n_2$
every frame validating
$\chi ({\langle {n_1} \rangle })$
also validates
$\chi ({\langle {n_2} \rangle })$
.
Using this, the ‘meaning’ of
$\mathbf {SFL}(\Lambda )$
can be expressed relatively simply. Note that this meaning is expressed in terms of the depth of elements
$x \in F$
. Up until this point we have mainly been concerned with the height of elements.
Lemma 6.32. Take
$\Lambda \subseteq \mathcal S$
such that
$2\cdot 1 \in \Lambda $
, and let F be a finite poset. Let
$n \in \mathbb N$
be minimal such that
$n \in \Lambda $
, or
$\infty $
if no such signature is present. Similarly, let
$k \in \mathbb N^{>0}$
be minimal with
$1^k \in \Lambda $
, or
$\infty $
. Then
$F \vDash \mathbf {SFL}(\Lambda )$
if and only if the following three conditions are satisfied for every
$x \in F$
.
-
(i) We have
$\operatorname {\mathrm {\mathsf {height}}}(F) < n$
. -
(ii) Whenever
$\operatorname {\mathrm {\mathsf {depth}}}(x) = 1$
, we have
$\mathopen |{\Uparrow} (x)\mathclose | < k$
. -
(iii) Whenever
$\operatorname {\mathrm {\mathsf {depth}}}(x)> 1$
, the set
${\Uparrow} (x)$
is connected.
Proof By Corollary 6.31 and the fact that
$F \vDash \chi ({\langle {n} \rangle })$
if and only if
$\operatorname {\mathrm {\mathsf {height}}}(F) \leqslant n-1$
, it suffices to treat the case
$n=\infty $
. Now by Lemma 6.30,
$\mathbf {SFL}(\Lambda ) = \mathbf {SFL}(2 \cdot 1, 1^k)$
when
$k < \infty $
, and
$\mathbf {SFL}(\Lambda ) = \mathbf {SFL}(2 \cdot 1)$
otherwise.
Assume that
$F \vDash \mathbf {SFL}(\Lambda )$
.
-
(ii) In the case
$k < \infty $
, take
$x \in F$
with
$\operatorname {\mathrm {\mathsf {depth}}}(x) = 1$
. Note that
${\Uparrow} (x)$
is an antichain, so
$(\{y\} \mid y \in {\Uparrow} (x))$
is an open partition of
${\Uparrow} (x)$
. Since
$x \vDash \chi ({\langle {1^k} \rangle })$
, by Lemma 6.7 and Theorem 6.9 we must have
$\mathopen |{\Uparrow} (x)\mathclose | < k$
. -
(iii) Now take
$x \in F$
with
$\operatorname {\mathrm {\mathsf {depth}}}(x)> 1$
, and suppose for a contradiction that
${\Uparrow} (x)$
is disconnected. Then we can partition
${\Uparrow} (x)$
into disjoint upwards-closed sets
$U,V$
. Since
$\operatorname {\mathrm {\mathsf {depth}}}(x)> 1$
, one of U and V (say U) must have height at least
$1$
. But then
$(U,V)$
is a
$(2 \cdot 1)$
-partition of
${\Uparrow} (x)$
, contradicting that
$F \vDash \chi ({\langle {2 \cdot 1} \rangle })$
by Theorem 6.9. #
Conversely, assume that
$F \nvDash \mathbf {SFL}(\Lambda )$
We will show that one of (ii) and (iii) is violated. If
$F \nvDash \chi ({\langle {2 \cdot 1} \rangle })$
, then by Theorem 6.9 there is
$x \in F$
and a
$(2 \cdot 1)$
-partition
$(U,V)$
of
${\Uparrow} (x)$
. But then
$\operatorname {\mathrm {\mathsf {height}}}(U) \geqslant 1$
, meaning that
$\operatorname {\mathrm {\mathsf {depth}}}(x)> 1$
, and furthermore
${\Uparrow} (x)$
is disconnected, violating (iii). So let us assume that
$k<\infty $
, that
$F \vDash \chi ({\langle {2 \cdot 1} \rangle })$
but that
$F \nvDash \chi ({\langle {1^k} \rangle })$
. Again, we get
$x \in F$
and a
$1^k$
-partition
$(C_1, \ldots , C_k)$
of
${\Uparrow} (x)$
. We must have that
$\operatorname {\mathrm {\mathsf {height}}}(C_1) = 0$
, otherwise
$(C_1,C_2 \cup \cdots \cup C_k)$
is a
$(2 \cdot 1)$
-partition of
${\Uparrow} (x)$
. Similarly
$\operatorname {\mathrm {\mathsf {height}}}(C_i) = 0$
for every
$i \leqslant k$
. This means that
$\operatorname {\mathrm {\mathsf {depth}}}(x) = 1$
, and that
$\mathopen |{\Uparrow} (x)\mathclose | \geqslant k$
, violating (ii).
Let us turn now to the proof of Theorem 6.29. We first outline the construction before coming to the full proof.
-
• We first split F up into its tree unravelling
$\operatorname {{\mathrm {Tree}}}(F)$
(defined below). -
• We then lengthen branches so that every top element has the same height.
-
• Lastly, we join top nodes of this tree in order to recover any
$\alpha $
-connectedness that we lost.
See Figure 6 for an example of this process.
An example of gradification in the presence of Scott’s tree.
Given any finite, rooted poset F, its tree unravelling
$\operatorname {{\mathrm {Tree}}}(F)$
is the set of chains X in F such that X is maximal in
$\downarrow (\max (X))$
, ordered by subset inclusion. Define the function
$\mathsf {last} \colon \operatorname {{\mathrm {Tree}}}(F) \to F$
by
$$ \begin{align*} X \mapsto \max (X). \end{align*} $$
Then
$\operatorname {{\mathrm {Tree}}}(F)$
is a tree and
$\mathsf {last}$
is a p-morphism (see [Reference Chagrov and Zakharyaschev14, Theorem 2.19, p. 32]).
We make use of the following abbreviations. For any poset F, the set of top elements (i.e., elements of depth
$0$
) in F is denoted by
$\operatorname {\mathrm {\mathsf {Top}}}(F)$
; let
.
Proof of Theorem 6.29
Let
. We may assume
$\epsilon \notin \Lambda $
. If
$2 \in \Lambda $
, then by Remark 6.12,
$n \leqslant 1$
, so F is already graded. So assume that
$2 \notin \Lambda $
.
Start with the tree unravelling
$T=\operatorname {{\mathrm {Tree}}}(F)$
of F. Form a new tree
$T_0$
by replacing each top node
$t \in \operatorname {\mathrm {\mathsf {Top}}}(T)$
with a chain of new elements
${t^{*}(0)}, \ldots , {t^{*}(m_t)}$
, where
$m_t = n-\operatorname {\mathrm {\mathsf {height}}}(t)$
. The relations between these new elements and the rest of T are as follows:
$$ \begin{gather*} {t^*(0)} < \cdots < {t^{*}(m_t)}, \\ x < {t^{*}(0)} \quad \Leftrightarrow \quad x < t \qquad \forall x \in T. \end{gather*} $$
Note that in
$T_0$
all branches have the same length
$n+1$
. Define the p-morphism
$g \colon T_0 \to T$
by
$$ \begin{align*} x \mapsto \left\{ \begin{array}{ll} x, & \text{ if }x \in \operatorname{\mathrm{\mathsf{Trunk}}}(T), \\ \mathsf{last}(t), & \text{ if }x={t^{*}(i)}\text{ for some }t \in \operatorname{\mathrm{\mathsf{Top}}}(T)\text{ and }i \leqslant m_t. \end{array} \right. \end{align*} $$
Form
$F'$
from
$T_0$
by identifying, for top nodes
$t,s \in \operatorname {\mathrm {\mathsf {Top}}}(T)$
, the elements
${t^{*}(m_t)}$
and
${s^*(m_s)}$
whenever
$\mathsf {last}(t)=\mathsf {last}(s)$
. That is, let
, where
Note that we have a p-morphism
$f = \mathsf {last} \circ g \circ q_{\mathcal {W}} \colon F' \to F$
. Furthermore, F is clearly finite and rooted. As to gradedness, take
$x \in F'$
with the aim of showing that all maximal chains in
$\downarrow (x)$
are of the same length, utilising Lemma 6.26. If
$x \in \operatorname {\mathrm {\mathsf {Trunk}}}(F')$
, then
$\downarrow (x)^{F'}$
is a linear order. So assume that
$x \in \operatorname {\mathrm {\mathsf {Top}}}(F')$
. Then any maximal chain X in
$\downarrow (x)$
corresponds to a branch of
$T_0$
, and therefore has length
$n+1$
.
Let us now use Lemma 6.32 to verify that our construction preserves
$\alpha $
-connectedness for
$\alpha \in \Lambda $
and complete the proof. Let
$k \in \mathbb N^{>0}$
be minimal such that
$1^k \in \Lambda $
, or
$\infty $
if no such signature is present. For
$u \in \operatorname {\mathrm {\mathsf {Top}}}(F)$
let
$\widehat u$
be the equivalence class of those elements
${t^*(m_t)}$
such that
$\mathsf {last}(t) = u$
. Note that by construction, for
$x \in \operatorname {\mathrm {\mathsf {Trunk}}}(T)$
and
$u \in \operatorname {\mathrm {\mathsf {Top}}}(F)$
,
$$ \begin{align} x < \widehat u \quad\Leftrightarrow\quad \mathsf{last}(x) < u. \end{align} $$
We need to check the three conditions of Lemma 6.32.
-
(i) Note that
$\operatorname {\mathrm {\mathsf {height}}}(F') = \operatorname {\mathrm {\mathsf {height}}}(F)$
. -
(ii) For any
$x \in F'$
with
$\operatorname {\mathrm {\mathsf {depth}}}(x)=1$
, either
$x \in \operatorname {\mathrm {\mathsf {Trunk}}}(T)$
or
$x={t^{*}(n_t-1)}$
for some top node
$t \in T$
. In the former case, the fact that
$\mathopen |{\Uparrow} (x)\mathclose | \leqslant k$
follows from (⋆) and the fact that
$\mathopen | {\Uparrow} ({\mathsf {last}(x)})^F\mathclose | \leqslant k$
. In the latter case we have
${\Uparrow} (x) = \left \{\widehat {\mathsf {last}(t)}\right \}$
. -
(iii) Similarly, for any
$x \in F'$
with
$\operatorname {\mathrm {\mathsf {depth}}}(x)> 1$
, either
$x \in \operatorname {\mathrm {\mathsf {Trunk}}}(T)$
or
$x={t^*(r)}$
for some top node
$t \in T$
and
$r < n_t-1$
. In the latter case,
${\Uparrow} (x)$
is a chain, so connected. For the former case, it suffices to show that any two top elements
$\widehat u, \widehat v \in {\Uparrow} (x)$
are connected by a path in
${\Uparrow} (x)$
. Note that
$\operatorname {\mathrm {\mathsf {depth}}}(\mathsf {last}(x))^F> 1$
. Now, since
$F \vDash \chi ({\langle {2 \cdot 1} \rangle })$
, by Lemma 6.32 there is a path
$u \rightsquigarrow v$
in
${\Uparrow} ({\mathsf {last}(x)})^F$
. We may assume that this path is of form given in Figure 7(a), where
$w_0, \ldots , w_k$
are top nodes in F. Using (⋆), this path then translates into a path
$\widehat u \rightsquigarrow \widehat v$
as in Figure 7(b), where
$y_i \in \mathsf {last}^{-1}\{a_i\} \cap {\Uparrow} (x)$
for each i.
The form of the paths in
$ {\Uparrow} ({\mathsf {last}(x)})^F$
and
$ {\Uparrow} (x)^{F'}$
.
6.7 Gradification without Scott’s tree
Now that the situation
$2 \cdot 1 \in \Lambda $
has been dealt with, let us turn to the case
$2 \cdot 1 \notin \Lambda $
.
Theorem 6.33. Let
$\Lambda \subseteq \mathcal S$
be such that
$2 \cdot 1 \notin \Lambda $
. Let F be a finite, rooted poset such that
$F \vDash \mathbf {SFL}(\Lambda )$
. Then there is a finite, graded, rooted poset
$F'$
and a p-morphism
$f \colon F' \to F$
such that
$F' \vDash \mathbf {SFL}(\Lambda )$
.
Unfortunately, the proof of Theorem 6.29 crucially relied on the fact that the original frame F was
$(2 \cdot 1)$
-connected. Consider for instance the frame F given in Figure 8, which at x is not
$(2 \cdot 1)$
-connected. If we apply the construction to F, we end up with a frame
$F'$
in which x sits below two connected components of height
$1$
, that is,Footnote
4
$\mathrm {ConType}({\Uparrow} (x)^{F'}) = 2^2$
. Hence
$F'$
is not
$2^2$
-connected, while F is. Taking
$2\cdot 1$
away from
$\Lambda $
is a double-edged sword however, since it allows for more complex constructions in
$F'$
.
The technique in the proof of Theorem 6.29 does not work in general.
The following reusable lemma will come in handy a couple of times.
Lemma 6.34. Let
$f \colon F' \to F$
be a surjective p-morphism between finite posets, and take
$x \in F'$
. Assume that for any
$y,z \in \operatorname {{\mathrm {Succ}}}(x)$
there is a path
$y \rightsquigarrow z$
in
${\Uparrow} (x)$
whenever there is a path
$f(y) \rightsquigarrow f(z)$
in
${\Uparrow} (f(x))$
. Then
$$ \begin{align*} \mathrm{ConComps}({\Uparrow} (x)) = \{{f}^{-1}[C] \mid C \in \mathrm{ConComps}({\Uparrow} (f(x)))\}. \end{align*} $$
In particular, if
$\operatorname {\mathrm {\mathsf {height}}}({f}^{-1}[C]) = \operatorname {\mathrm {\mathsf {height}}}(C)$
for any
$C \in \mathrm {ConComps}({\Uparrow} (f(x)))$
then
$$ \begin{align*} \mathrm{ConType}({\Uparrow} (x)) = \mathrm{ConType}({\Uparrow} (f(x)). \end{align*} $$
Proof Note that, since f is a p-morphism and F and
$F'$
are finite,
$\{{f}^{-1}[C] \mid C \in \mathrm {ConComps}({\Uparrow} (f(x)))\}$
is a partition of
${\Uparrow} (x)$
into upwards- and downwards-closed sets. So it suffices to show that
${f}^{-1}[C]$
is connected for every
$C \in \mathrm {ConComps}({\Uparrow} (f(x)))$
. Take
$y_0, z_0 \in {f}^{-1} [C]$
. Since
${f}^{-1}[C]$
is downwards-closed in
${\Uparrow} (x)$
, there are
$y, z \in \operatorname {{\mathrm {Succ}}}(x) \cap {f}^{-1}[C]$
such that
$y \leqslant y_0$
and
$z \leqslant z_0$
. Then
$f(y), f(z) \in C$
, so by assumption there is a path
$f(y) \rightsquigarrow f(z)$
in
${\Uparrow} (f(x))$
. But then by assumption there is a path
$y \rightsquigarrow z$
in
${\Uparrow} (x)$
, which lies in
${f}^{-1}[C]$
since the latter is upwards- and downwards-closed. This yields a path
$y_0 \rightsquigarrow z_0$
.
Let us turn now to the proof of Theorem 6.33. The construction works in two steps as follows (see Figure 9 for an example).
-
• Again, we start by splitting F up into its tree unravelling
$\operatorname {{\mathrm {Tree}}}(F)$
. -
• Then, in order to connect the frame back up again while ensuring that it remains graded, we construct ‘zigzag roller-coasters’ connecting top nodes of different heights.
An example of gradification in the absence of Scott’s tree.
Proof of Theorem 6.33
As in the proof of Theorem 6.29, we may assume that
$\epsilon ,1, 2 \notin \Lambda $
.
Start with
$T= \operatorname {{\mathrm {Tree}}}(F)$
. For every two distinct
$p,q \in \operatorname {\mathrm {\mathsf {Top}}}(T)$
such that
$\mathsf {last}(p)=\mathsf {last}(q)=t$
, we will build a ‘roller-coaster’ structure
$Z(p,q)$
, which will furnish a bridge between p and q. Every such structure
$Z(p,q)$
is independent, so that they can all be added to T at the same time. First note that by Corollary 6.27, T is graded; let
$\rho \colon T \to \mathbb N$
be its rank function.
Now, take distinct
$p,q \in \operatorname {\mathrm {\mathsf {Top}}}(T)$
such that
$\mathsf {last}(p)=\mathsf {last}(q)=t$
. Let
. By swapping p and q, we may assume that
$l \geqslant 0$
. We need to join p to q with a path which ascends in grade. We do this using a zigzagging path, which consists of lower points
$a_0, \ldots , a_l$
, upper points
$b_0, \ldots , b_{l-1}$
and intermediate points
$c_0, \ldots , c_{l-1}$
. The relations between these points are as follows (see Figure 10):
$$ \begin{gather*} a_i < c_i < b_i, \qquad a_{i+1}<b_i. \end{gather*} $$
The relations between the zigzag points in case
$l=3$
.
Consider
$p \wedge q$
(i.e., the intersection of p and q, regarded as chains), and let
. Note that
$k \geqslant 0$
since p and q are incomparable. Moreover,
$k \geqslant 1$
as follows. Suppose for a contradiction that
$k = 0$
, so that p is an immediate successor of
$p \wedge q$
. Then
$\mathsf {last}(p)$
is an immediate successor of
$\mathsf {last}(p \wedge q)$
. But
$\mathsf {last}(q)=\mathsf {last}(p)$
, so we have, as chains,
$$ \begin{align*} p = (p \wedge q) \cup \{\mathsf{last}(p)\} = (p \wedge q) \cup \{\mathsf{last}(q)\} = q. \end{align*} $$
contradicting that p and q are distinct. #
To ensure that the new poset
$F'$
is still graded, we need to dangle some scaffolding down from the zigzag path to
$p \wedge q$
. Below each lower point
$a_i$
we will dangle a chain of
$k+i-1$
points
$d(i,1), \ldots , d(i,{k+i-1})$
. The relations are as follows:
$$ \begin{align*} d(i,1) < d(i,2) < \cdots < d(i,{k+i-1}) < a_i. \end{align*} $$
Finally, let
$\mathrm Z(p,q)$
denote the whole structure of the zigzag path plus the dangling scaffolding. Attach
$\mathrm Z(p,q)$
to T by adding the following relations and closing under transitivity (see Figure 11):
$$ \begin{align*} a_0 < p, \qquad a_l < q, \qquad \forall i \colon p \wedge q < d(i,1). \end{align*} $$
The zigzag path and the ladder structure in place.
Let
$F'$
be the result of adding
$\mathrm Z(p,q)$
to T for every pair
$p,q$
, and define the function
$f \colon F' \to F$
by
First, let us see that f is a p-morphism. The (Forth) condition follows from the fact that
$\mathsf {last}$
is monotonic, and that:
-
• if
$x \leqslant y$
with
$x \in T$
and
$y \in Z(p,q)$
, then by construction
$x \leqslant p \wedge q$
, meaning that
$f(x) = \mathsf {last}(x) \leqslant \mathsf {last}(p \wedge q) \leqslant \mathsf {last}(p) = f(y)$
, and -
• if
$x \leqslant y$
with
$x \in Z(p,q)$
and
$y \in T$
, then by construction
$y \in \{p,q\}$
, so that
$f(x) = \mathsf {last}(p) = f(y)$
.
The (Back) condition follows from the fact that
$\mathsf {last}$
is open, and that each
$Z(p,q)$
maps to a top node.
Second, for any pair
$p,q$
, we can extend the rank function
$\rho $
to the new structure
$\mathrm Z(p,q)$
as follows (as indicated by the heights of the nodes in Figure 11):
$$ \begin{gather*} \rho(a_i) = \rho(p) + i - 1, \\ \rho(b_i) = \rho(p) + i + 1, \\ \rho(c_i) = \rho(p) + i, \\ \rho(d(i,j)) = \rho(p \wedge q) + j. \end{gather*} $$
To see that, thus extended,
$\rho $
is still a rank function, it suffices to check that the newly ranked
$Z(p,q)$
fits into T as a ranked structure. That is, we need to check the following equations:
$$ \begin{gather*} \rho(p) = \rho(a_0) + 1, \\ \rho(q) = \rho(a_l) + 1, \\ \rho(d(i,1)) = \rho(p \wedge q) + 1. \end{gather*} $$
But these follow by definition. In this way we see that
$F'$
is graded.
Finally, it remains to be shown that
$F \vDash \mathbf {SFL}(\Lambda )$
. So take
$x \in F$
. First, whenever
$x \in Z(p,q)$
for some
$p,q$
, by construction
${\Uparrow} (x)$
is
$\alpha $
-connected for every signature other than
$\epsilon $
,
$1^2$
,
$2 \cdot 1$
, and k where
$k \geqslant \operatorname {\mathrm {\mathsf {height}}}(F)+1$
. Hence we may assume that
$x \in T$
. Let us use Lemma 6.34. Take
$y,z \in \operatorname {{\mathrm {Succ}}}(x)$
such that there is a path
$f(y) \rightsquigarrow f(z)$
in
${\Uparrow} ({\mathsf {last}(x)})$
, with the aim of finding a path
$y \rightsquigarrow z$
in
${\Uparrow} (x)$
.
First assume that
$y \in Z(p,q)$
for some
$p,q$
. Then since
$y \in \operatorname {{\mathrm {Succ}}}(x)$
and
$x \in T$
, by construction
$x = p \wedge q$
. All of
$Z(p,q)$
is connected in
${\Uparrow} (x)$
, and hence there is a path
$y \rightsquigarrow p$
. Let
$p' \in T$
be the immediate successor of x which lies below p (this exists since T is a tree). Then we have a path
$y \rightsquigarrow p'$
in
${\Uparrow} (x)$
. With this case thus dealt with, we may now assume that
$y \in T$
, and similarly that
$z \in T$
.
So, we have a path
$\mathsf {last}(y) \rightsquigarrow \mathsf {last}(z)$
. We now proceed in a similar fashion to the proof of Theorem 6.29. We may assume that the path
$\mathsf {last}(y) \rightsquigarrow \mathsf {last}(z)$
has the form in Figure 12(a), where
$t_0, \ldots , t_k$
are top nodes in F. Let
and
. For each
$i \in \{1, \ldots , k-1\}$
, choose
$u_i \in {\mathsf {last}}^{-1}\{a_i\}$
. For
$i \in \{0, \ldots , k-1\}$
, take
$p_i,q_i \in {\mathsf {last}}^{-1}\{t_i\}$
such that
$u_i \leqslant p_i$
and
$u_{i+1} \leqslant q_i$
. For each such i, since
$\mathsf {last}(p_i)=\mathsf {last}(q_i)$
, there is a path
$p_i \rightsquigarrow q_i$
which lies in
$Z(p_i,q_i)$
, and hence lies in
${\Uparrow} (x)$
. Compose all these paths as in Figure 12 to form a path
$y \rightsquigarrow z$
in
${\Uparrow} (x)$
as required.
The form of the paths in
$ {\Uparrow} ({\mathsf {last}(x)})$
and
$ {\Uparrow} (x)$
.
It now remains to show that if
$C \in \mathrm {ConComps}({\Uparrow} ({\mathsf {last}(x)}))$
, then
$\operatorname {\mathrm {\mathsf {height}}}({f}^{-1}[C]) = \operatorname {\mathrm {\mathsf {height}}}(C)$
. First, since f is a p-morphism,
$\operatorname {\mathrm {\mathsf {height}}}({f}^{-1}[C]) \geqslant \operatorname {\mathrm {\mathsf {height}}}(C)$
. Conversely, let
$X \subseteq {f}^{-1}[C]$
be a maximal chain. Assume X intersects with some
$Z(p,q)$
. Then we can replace the part
$X \cap (Z(p,q) \cup \{p,q\})$
with the unique maximal chain in
${\Uparrow} (p \wedge q)^T$
containing q (this exists since T is a tree). Then by construction this does not decrease the length of X nor does it move X outside of
${f}^{-1}[C]$
(since the latter is upwards- and downwards-closed). Therefore, we may assume that
$X \subseteq T$
, so X corresponds to a chain
$\mathsf {last}[X]$
of the same length in C.
Therefore, by Lemma 6.34 we get that
$\mathrm {ConType}({\Uparrow} (x)) = \mathrm {ConType}({\Uparrow} ({\mathsf {last}(x)})$
. Applying Lemma 6.7, we have that
${\Uparrow} (x)$
has an
$\alpha $
-partition if and only if
${\Uparrow} ({\mathsf {last}(x)})$
has an
$\alpha $
-partition.
6.8 Nervification
We now find ourselves, having suitably prepared F, in a position to make use of its additional graded structure. The general method of the final construction, in which we transform F into a frame which nerve-validates
$\mathbf {SFL}(\Lambda )$
, is the same as in Theorems 6.29 and 6.33. We begin with the tree unravelling
$\operatorname {{\mathrm {Tree}}}(F)$
, perform some alterations, then rejoin top nodes. A key difference here is that we won’t rejoin every top node to every other top node whose ‘
$\mathsf {last}$
’ value is the same. Instead, we line up all the top nodes mapping to the same element and link each top node to at most two other top nodes, which we think of as its neighbours. See Figure 13 for an example of the construction.
An example of nervification, using the graded structure of F.
Definition 6.35. Let T be a finite tree. Then for each
$x \in T$
, we have that
$\downarrow (x)$
is a chain. For
$k\leqslant \operatorname {\mathrm {\mathsf {height}}}(x)$
, let
$x^{(k)}$
be the element of this chain which has height k. Let
$x^{(-k)}$
be the element which has height
$\operatorname {\mathrm {\mathsf {height}}}(x)-k$
.
Definition 6.36. For
$n \in \mathbb N$
, let
.
Theorem 6.37. Take
$\Lambda \subseteq \mathcal S$
and let F be a finite, graded, rooted poset of height n such that
$F \vDash \mathbf {SFL}(\Lambda )$
. Then there is a poset
$F'$
and a p-morphism
$f \colon F' \to F$
such that
$F' \vDash \mathbf {SFL}(\Lambda )$
and such that
$F'$
is
$\alpha $
-diamond-connected for every
$\alpha \in \mathcal S_n$
.
Proof of Theorem 6.37
We may assume that
$\epsilon ,1 \notin \Lambda $
. Further, if
$2 \in \Lambda $
, then
$\operatorname {\mathrm {\mathsf {height}}}(F)=1$
, so F is already
$\alpha $
-diamond-connected for every
$\alpha \in \mathcal S_n$
. Hence we may assume that
$2 \notin \Lambda $
.
Once more, start with
$T = \operatorname {{\mathrm {Tree}}}(F)$
. Chop off the top nodes: let
. For each
$t \in \operatorname {\mathrm {\mathsf {Top}}}(F)$
, we will add a new structure
$W(t)$
, which lies only above elements of
$T'$
. Let
$\rho \colon F \to \mathbb N$
be the rank function on F. Note that
$\rho \circ \mathsf {last} \colon T \to \mathbb N$
is the rank function on T.
Take
$t \in \operatorname {\mathrm {\mathsf {Top}}}(F)$
. Enumerate
$\mathsf {last}^{-1}\{t\}= \{p_1, \ldots , p_m\}$
. For each
$i \leqslant m-1$
, define
Note that
$k_i \geqslant 1$
just as in the proof of Theorem 6.33. Since F is graded and T is a tree, we have that
$$ \begin{align*} \mathopen|{\Updownarrow} (r_i,p_i)^T\mathclose| = \mathopen|{\Updownarrow} (r_i,p_{i+1})^T\mathclose| = k_i. \end{align*} $$
In other words,
$p_i^{(l_i)} = p_{i+1}^{(l_i)} = r_i$
. We will construct a ‘chevron’ structure which joins
$p_i^{(-1)}$
to
$p_{i+1}^{(-1)}$
. For each
$i \leqslant m-1$
, take new elements
$a(i,1), \ldots , a(i,{k_i})$
, and add them to
$T'$
using the following relations:
$$ \begin{align*} a(i,1) < \cdots < a(i,{k_i}), \qquad \forall j \leqslant k_i \colon p_i^{(l+j)}, p_{i+1}^{(l+j)} < a(i,j). \end{align*} $$
Let
$W(t)$
be this new structure (i.e., the chain
$\{a(i,1) < \cdots < a(i,{k_i})\}$
in place). See Figures 14 and 15 for examples of this process of adding chevrons.
The chevron structure in a case with two branches.
The chevron structure in a more complex case involving three branches.
The process of adding
$W(t)$
is independent for each
$t \in \operatorname {\mathrm {\mathsf {Top}}}(F)$
. Let
$F'$
be the result of adding every
$W(t)$
to
$T'$
. Define
$f \colon F' \to F$
by
Since we have made sure that each
$W(t)$
contains, for each
$p_i \in \mathsf {last}^{-1}\{t\}$
, a node above
$p_i^{(-1)}$
which maps to t, and that all of the new structure maps to a top node, f is a p-morphism.
Let us see that
$F' \vDash \mathbf {SFL}(\Lambda )$
. Take
$x \in F'$
. If
$x \in W(t)$
for some t, then
${\Uparrow} (x)$
is either empty or a chain, hence
${\Uparrow} (x) \vDash \mathbf {SFL}(\Lambda )$
. So we assume that
$x \in T'$
. The verification is now very similar to that in Theorem 6.33, making use of Lemma 6.34. Take
$y,z \in \operatorname {{\mathrm {Succ}}}(x)$
such that there is a path
$f(y) \rightsquigarrow f(z)$
in
${\Uparrow} ({\mathsf {last}(x)})$
. As in the proof of Theorem 6.33, by construction of
$W(t)$
we may assume that
$y,z \in T'$
. Just as in that proof, we can construct a path
$y \rightsquigarrow z$
from the path
$f(y) \rightsquigarrow f(z)$
, using the fact that whenever
$t \in {\Uparrow} ({\mathsf {last}(x)}) \cap \operatorname {\mathrm {\mathsf {Top}}}(F)$
, any
$w,v \in {f}^{-1}\{t\}$
are connected by a path in
${\Uparrow} (x)^{F'}$
(this is how we constructed
$F'$
). It is straightforward then to check that if
$C \in \mathrm {ConComps}({\Uparrow} ({\mathsf {last}(x)}))$
we have
$\operatorname {\mathrm {\mathsf {height}}}({f}^{-1}[C]) = \operatorname {\mathrm {\mathsf {height}}}(C)$
, giving that
$$ \begin{align*} \mathrm{ConType}({\Uparrow} (x)) = \mathrm{ConType}({\Uparrow} ({\mathsf{last}(x)})). \end{align*} $$
To complete the proof, let us see that
$F'$
is
$\alpha $
-diamond-connected for every
$\alpha \in \mathcal S_n$
. Take
$x,y \in F'$
with
$x < y$
and consider
${\Updownarrow} (x,y)$
. There are several cases.
-
(a) Case
$y \in T'$
. We have that
${\Updownarrow} (x,y)^{F'} = {\Updownarrow} (x,y)^{T'}$
, which is linearly ordered since
$T'$
is a tree; hence it is connected and of height at most
$n-2$
.
Hence
$y = a(i,j)$
for
$a(i,j) \in W(t)$
a new element. Let
$p_i,p_{i+1}, r_i, l_i$
be as above.
-
(b) Case
$x \in W(t)$
. Note that by construction
${\Updownarrow} (x,y)$
is linearly ordered. -
(c) Case
$x=p_i^{(l+e)}$
for some e. If we have
$\operatorname {\mathrm {\mathsf {height}}}({\Updownarrow} (x,y))=1$
, then
$e=i-1$
and
${\Updownarrow} (x,y)$
is the antichain on two elements, which is
$\alpha $
-connected. Otherwise, by construction,
$a(i,{j-1}) \in {\Updownarrow} (x,y)$
which is connected to everything. -
(d) Case
$x=p_{i+1}^{(l+e)}$
for some e. This is symmetric. -
(e) Case
$x=r_i$
. Again, if
$\operatorname {\mathrm {\mathsf {height}}}({\Updownarrow} (x,y)))=1$
then
$j=1$
and
${\Updownarrow} (x,y)$
is the antichain on two elements, otherwise
$a(i,1) \in {\Updownarrow} (x,y)$
which is connected to everything. -
(f) Otherwise,
$x < r_i$
(since
$T'$
is a tree). Then
$r_i \in {\Updownarrow} (x,y)$
which is connected to everything.
6.9 End of Proof of Theorem 6.15
We can now prove our second main result:
Proof of Theorem 6.15
By Lemmas 6.19 and 6.20, we need to show that every finite, rooted frame of
$\mathbf {SFL}(\Lambda )$
is the up-reduction of one which nerve-validates
$\mathbf {SFL}(\Lambda )$
; in fact this up-reduction is just a p-morphism. So take such a frame F. We may assume that F is graded: when we have
$2 \cdot 1 \in \Lambda $
, apply Theorem 6.29, otherwise apply Theorem 6.33. Then by Theorem 6.37, there is a frame
$F'$
and a p-morphism
$f \colon F' \to F$
such that
$F'$
is
$\alpha $
-nerve-connected for every
$\alpha \in \Lambda $
(note that by Remark 6.12 we must have
$\Lambda \subseteq \mathcal S_n$
where
$n = \operatorname {\mathrm {\mathsf {height}}}(F)$
). Then, by Theorem 6.23,
$F'$
nerve-validates
$\mathbf {SFL}(\Lambda )$
, which completes the proof.
Acknowledgements
We are grateful to the referee for many helpful and detailed comments which improved the presentation of the paper.
Funding
The first author was supported by the Amsterdam Science Talent Scholarship during this research.
