Categories: How I Learned to Stop Worrying and Love Two Sorts

Abstract

RS-frames were introduced by Gehrke as relational semantics for substructural logics. They are two-sorted structures, based on RS-polarities with additional relations used to interpret modalities. We propose an intuitive, epistemic interpretation of RS-frames for modal logic, in terms of categorization systems and agents’ subjective interpretations of these systems. Categorization systems are a key to any decision-making process and are widely studied in the social and management sciences.

A set of objects together with a set of properties and an incidence relation connecting objects with their properties forms a polarity which can be ‘pruned’ into an RS-polarity. Potential categories emerge as the Galois-stable sets of this polarity, just like the concepts of Formal Concept Analysis. An agent’s beliefs about objects and their properties (which might be partial) is modelled by a relation which gives rise to a normal modal operator expressing the agent’s beliefs about category membership. Fixed-points of the iterations of the belief modalities of all agents are used to model categories constructed through social interaction.

1 Introduction

Relational semantic frameworks for logics algebraically captured by varieties of normal lattice expansions¹ have been intensely investigated for more than three decades [3, 15, 17, 19, 22, 25, 27, 30, 31, 33, 34, 39, 40]. However, none of these frameworks has gained the same pre-eminence and success as Kripke semantics. Indeed, the extant proposals are regarded as significantly less intuitive than Kripke structures, especially w.r.t. their possibility to support the various established interpretations of modal operators (e.g. epistemic, temporal, dynamic), and hence doubts have been raised as to the suitability of these logics for applications. Various directions have been explored to try and cope with these difficulties, such as: (a) attempts to provide a conceptual justification to some of the distinctive features of these semantics (for instance, in [25], a conceptual motivation has been given for the ‘two-sortedness’ of the relational semantics for substructural logics introduced in the same paper in terms of a duality between states and information quanta); (b) recapturing the usual definition of the interpretation clause of modal operators in a generalized context [27, 28]; (c) improving the modularity of mathematical theories such as correspondence theory, to facilitate the transfer of results across different semantic settings. The latter direction has been implemented specifically for lattice-based logics in [6, 9, 10], and pursued more in general in [4, 5, 7, 8, 11–14, 21, 26, 37, 38].

The contribution of the present paper pertains to direction (a): we propose categorization theory in management science as a concrete frame of reference for understanding the RS-semantics of lattice-based modal logic, and we argue that, when understood in this light, a natural epistemic interpretation can be given to the modal operators, which captures e.g. the factivity and positive introspection of knowledge.

Our starting point is the connection, mentioned also in [25], between RS-semantics and Formal Concept Analysis (FCA) [24]. Namely, RS-frames for normal lattice-based modal logics are based on polarities, that is, tuples $(A, X, \perp )$ such that A and X are sets, and $\perp \subseteq A\times X$. In FCA, polarities can be understood as formal contexts, consisting of objects (the elements of A) and properties (the elements of X) with the relation $\perp$ indicating which object satisfies which property. It is well known that any polarity induces a Galois connection between the powersets of A and X, the stable sets of which form a complete lattice, and in fact, any complete lattice is isomorphic to one arising from some polarity. This representation theory for general lattices, due to Birkhoff, provides the polarity-to-lattice direction of the duality developed in [25], and is also at the heart of FCA. Indeed, the Galois-stable sets arising from formal contexts can be interpreted as formal concepts. One of the most felicitous insights of FCA is that concepts are endowed by construction with a double interpretation: an extensional one, specified by the objects which are instances of the formal concept, and an intensional one, specified by the properties shared by any object belonging to the concept.

The second key step is the arguably natural idea that categories and classification systems, as studied in social sciences and management science, are a very concrete setting of application of the insights of FCA.

Indeed, in social science and management science, categories are understood as types of collective identities for broad classes e.g. of market products, organizations or individuals. Categorization theory recognizes categories as a key aspect of any decision-making process, in that they structure the space of options by defining the boundaries of meaningful comparisons between the available alternatives [29, 32, 42]. Also, categories function as cognitive sieves, filtering out those features which are redundant or less essential to the decision-making, thus contributing to minimize the agents’ cognitive efforts. Examples of categories are musical genres, which are widely applied as tools to compress and convey relevant information about a musical product to its potential audience. Structuring information and decision-making along the faultlines of genres is so established a practice in the creative industries that genres have become the main way to structure competition as well as to create consumer group identity.

An aspect of categories which is very much highlighted in the categorization theory literature is that they never occur in isolation; rather, they arise in the context of categorization systems (e.g. taxonomies), which are typically organized in hierarchies of super- (i.e. less specified) and sub- (i.e. more specified) categories. This observation agrees with the FCA treatment, according to which concepts arise embedded in their concept lattice.

One of the open challenges in the extant literature is how to reconcile the view on categories which defines them in terms of the objects (e.g. products) belonging to that category with another view which defines categories in terms of the features enjoyed by its members. The intensional and extensional perspectives on concepts brought about by FCA provide an elegant reconciliation of the two views on categories, which gives a second clue that the FCA perspective on categorization theory can be fruitful.

In recent years, a substantial research stream in social and management science explores the dynamic aspects of categorization [29, 35]. For instance, category emergence investigates how new categories are created, either ex nihilo or through the recombination of existing ones, and how the interaction of relevant groups of agents, such as the media or the reviewers, plays a role in this process. The aspect of social interaction is essential to understand how categories arise and are put to use: although they can be seen to arise from factual pieces of information about the world (e.g., the products available in a given market and their features), a critical component of their nature cannot be reduced to factual information. In other words, categories are social artifacts, and reasoning about them requires a peculiar combination of factual truth, individual perception and social interaction.

The main point of interest and the conceptual contribution of the present proposal concerns precisely the formalization of the subjective and social aspects of this emergence. Namely, we observe that the agents’ subjective perspective on products and features can be naturally modelled by associating each agent with a binary relation $R\subseteq A\times X$ on the database $(A, X, \perp )$, which represents the subjective filters superimposed by each agent on the information of the database. That is, for every product $a\in A$ and every feature $x\in X$, we read aRx as ‘product a has feature x according to the agent’. By general order-theoretic facts, these relations² induce normal modal operators on the categorization system associated with the database. These modal operators enrich the basic propositional logic of the categorization systems. In this enriched logical language, it is easy to distinguish between ‘objective’ information (stored in the database), encoded in the formulas of the modal-free fragment of the language, and the agents’ subjective interpretation of the ‘objective’ information, encoded in formulas in which modal operators occur. This language is expressive enough to encode agents’ beliefs/perceptions regarding other agents’ beliefs/perceptions, and so on. Again, this makes it possible to define fixed points of these regressions, similarly to the way in which common knowledge is defined in classical epistemic logic [20]. Intuitively, these fixed points represent the stabilization of a process of social interaction; for instance, the consensus reached by a group of agents regarding a given category. Clearly, market dynamics are bound to create further destabilization, necessitating a new round of interaction in order to establish a new equilibrium. Further directions will be to generalize the framework of dynamic epistemic logic [2] to the setting outlined in the present paper, and further develop the theory of lattice-based mu-calculus initiated in [6].

Structure of the Paper. In Sect. 2, we collect the necessary definitions and basic facts about RS-semantics. In Sect. 3, we discuss how the mathematical environment introduced in the previous section can be understood using categories and categorization systems as the framework of reference. In particular, we show how normal modal operators on lattices can support an epistemic interpretation. In Sect. 4, we build on the epistemic interpretation of the modal operators, and introduce a common knowledge-type construction to account for a view of categories as the outcome of social interaction. In Sect. 5 we collect our conclusions. More technical background is relegated to Appendix A, while the proofs of some technical lemmas can be found in Appendix B.

2 Preliminaries

In this section we recall some preliminaries on perfect lattices, RS-polarities, generalized Kripke frames and formal concept analysis. We will assume familiarity with the basics of lattice theory (see e.g. [16]).

2.1 Perfect Lattices

A bounded lattice $\mathbb {L} = (L, \wedge , \vee , 0, 1)$ is complete if all subsets $S\subseteq L$ have both a supremum $\bigvee S$ and an infimum $\bigwedge S$. An element a in $\mathbb {L}$ is completely join-irreducible if, for any $S\subseteq \mathbb {L}$, $a = \bigvee S$ implies $a \in S$. Complete meet-irreducibility is defined order-dually. The sets of completely join- and meet-irreducible elements of $\mathbb {L}$ are denoted by $J^{\infty }(\mathbb {L})$ and $M^{\infty }(\mathbb {L})$, respectively.

A complete lattice $\mathbb {L}$ is called perfect if it is join-generated by its completely join-irreducibles, and meet-generated by its completely meet-irreducibles. That is, $\mathbb {L}$ is perfect if for any $u\in \mathbb {L}$, we have $\bigvee \{j\in J^{\infty }(\mathbb {L})\mid j\le u\}=u= \bigwedge \{m\in M^{\infty }(\mathbb {L})\mid u\le m\}$.

2.2 Polarities and Birkhoff’s Representation Theorem

Definition 1

A polarity is a triple $\mathbb {P} = (A,X,\perp )$ where A and X are sets, and $\perp \ \subseteq \ A \times X$ is a relation. For every polarity $\mathbb {P}$, we define the functions $(\cdot )^{\uparrow }$ (upper) and $(\cdot )^{\downarrow }$ (lower)³ between the posets $(\mathcal {P}(A), \subseteq )$ and $(\mathcal {P}(X), \subseteq )$, as follows:

The maps $(\cdot )^{\uparrow }$ and $(\cdot )^{\downarrow }$ form a Galois connection between $(\mathcal {P}(A), \subseteq )$ and $(\mathcal {P}(X) , \subseteq )$, i.e. $V\subseteq U^{\uparrow }$ iff $U \subseteq V^{\downarrow }$ for all $U \in \mathcal {P}(A)$ and $V \in \mathcal {P}(X)$. Well-known consequences of this fact are: the composition maps $(\cdot )^{\uparrow \downarrow }: = (\cdot )^{\downarrow }\circ (\cdot )^{\uparrow }$ and $(\cdot )^{\downarrow \uparrow }: = (\cdot )^{\uparrow }\circ (\cdot )^{\downarrow }$ are closure operators on $(\mathcal {P}(A), \subseteq )$ and $(\mathcal {P}(X), \subseteq )$, respectively;⁴ The set of all Galois-stable subsets of A (i.e. those $U \in \mathcal {P}(A)$ such that $U^{\uparrow \downarrow } = U$) forms a complete sub-semilattice of $(\mathcal {P}(A), \bigcap )$, which we denote by $\mathbb {P}^+$;⁵ since it is complete, the semilattice $\mathbb {P}^+$ is in fact a lattice, where meet is set-theoretic intersection and join is the closure of the set-theoretic union. If fact, Birkhoff showed that every complete lattice is isomorphic to $\mathbb {P}^+$ for some polarity $\mathbb {P}$. This lattice can be identified with the lattice of concepts arising from $\mathbb {P}$ (this terminology comes from Formal Concept Analysis), i.e. tuples (C, D) s.t. $C\subseteq A$, $D\subseteq X$ and $D^{\downarrow } = C$ and $C^{\uparrow } = D$.⁶ Concepts (resp. Galois stable subsets of X and of A) can be characterized as (members of) tuples $(U^{\uparrow \downarrow }, U^{\uparrow })$ and $(V^{\downarrow }, V^{\downarrow \uparrow })$ for any $U\subseteq A$ and $V\subseteq X$.

Let us conclude the present subsection by introducing some notation and showing some useful facts. Polarities $(A, X, \perp )$ induce ‘specialization pre-orders’ on A and X defined as follows: $x\le y$ iff $\forall a (a\perp x\rightarrow a\perp y)$ for all $x, y\in X$, and $a\le b$ iff $\forall x (b\perp x\rightarrow a\perp x)$ for all $a, b\in A$. Clearly, $\le \circ \perp \circ \le \subseteq \perp$. For every $b\in A$ and $z\in X$, let $z{\uparrow }: = \{x\mid z\le x\}$, and $b{\downarrow }: = \{a\mid a\le b\}$. The proofs of the following lemma and corollary can be found in Appendix B.

Lemma 1

$z{\uparrow }$ and $b{\downarrow }$ are Galois-stable for all $b\in A$ and $z\in X$.

Corollary 1

$z^{\downarrow \uparrow } = z{\uparrow }$ and $b^{\uparrow \downarrow } = b{\downarrow }$ for all $b\in A$ and $z\in X$.

Summing up, the concepts generated by each $a\in A$ and $x\in X$ are $(a{\downarrow }, a^{\uparrow })$ and $(x^{\downarrow }, x{\uparrow })$ respectively.

2.3 RS-polarities and Dual Correspondence for Perfect Lattices

As mentioned early on, every complete lattice is isomorphic to $\mathbb {P}^+$ for some polarity $\mathbb {P}$. When specializing to distributive lattices and Boolean algebras, the well-known dualities obtain between set-theoretic structures and perfect algebras. In particular, perfect distributive lattices are dual to posets, and perfect (i.e. complete and atomic) Boolean algebras are dual to sets. The question then arises: which polarities are dual to perfect lattices? The answer was given by Gehrke in [25], where the so-called reduced and separated polarities, or RS-polarities, have been characterized as duals to perfect lattices, by rephrasing in a model-theoretic way the duality for perfect lattices given in [18]. In what follows, we will recall what it means for a polarity to be reduced and separated, and briefly explain how these two properties guarantee the perfection of the dual lattice. First, the route from perfect lattices to polarities is given by the following definition:

Definition 2

For every perfect lattice $\mathbb {L}$, the polarity associated with $\mathbb {L}$ is the triple $\mathbb {L}_+ := (J^\infty (\mathbb {L}),M^\infty (\mathbb {L}),\perp _+)$ where $\perp _{+}$ is the lattice order $\le _{\mathbb {L}}$ restricted to $J^\infty (\mathbb {L}) \times M^\infty (\mathbb {L})$.

Definition 3

(cf. [25, Definitions 2.3 and 2.12]). A polarity $\mathbb {P} = (A, X, \perp )$ is:

• 1. separating if the following conditions are satisfied:

  • (s1) for all $a, b\in A$, if $a\ne b$ then $a^{\uparrow }\ne b^{\uparrow }$, and

  • (s2) for all $x, y\in Y$, if $x\ne y$ then $x^{\downarrow }\ne y^{\downarrow }$.

• 2. reduced if the following conditions are satisfied:

  • (r1) for every $a\in A$, some $x\in X$ exists s.t. a is $\le$-minimal in $\{b\in A\mid b \not \perp x \}$.

  • (r2) for every $x\in X$, some $a\in A$ exists s.t. x is $\le$-maximal in $\{y\in X\mid x\not \perp a\}$.

• 3. an RS-polarity ⁷ if it is separating and reduced.

If $\mathbb {P}$ is separating, then, denoting $S: = \{b\mid b\in A$ and $b<a\} = a{\downarrow }{\setminus }\{ a \}$ for each $a\in A$, notice that $a{\downarrow }$ is completely join-irreducible in $\mathbb {P}^+$ iff $\bigvee _{b\in S}b{\downarrow }\varsubsetneq a{\downarrow }$ iff $a^{\uparrow }\varsubsetneq \bigcap _{b\in S}b^{\uparrow }$, i.e. some $x\in X$ exists such that $b\perp x$ for all $b\in S$ and $a\not \perp x$, which is condition (r1). Similarly, (r2) dually characterizes the condition that, for every $x\in X$, the subset $x{\uparrow }$ is completely meet-irreducible in $\mathbb {P}^+$, represented as a sub meet-semilattice of $\mathcal {P}(X)$.

Proposition 1

(cf. [25, Remark 2.13] and [18, Proposition 4.7, Corollary 4.9]). For every perfect lattice $\mathbb {L}$ and RS-polarity $\mathbb {P}$,

• 1. $\mathbb {L}_+$ is an RS-polarity and $(\mathbb {L}_+)^{+} \cong \mathbb {L}$.

• 2. $\mathbb {P}^+$ is a perfect lattice and $(\mathbb {P}^+)_{+} \cong \mathbb {P}$.

2.4 RS-frames and Models

In the present section, we report on the definition of a relational semantics, based on RS-polarities, for an expansion $\mathcal {L}$ of the basic lattice language with a unary normal box-type connective. We also give semantics for a further expansion of $\mathcal {L}$ with a unary normal diamond-type connective , and with two special sorts of variables $\mathbf {i},\mathbf {j}$ called nominals, and $\mathbf {m}, \mathbf {n}$ called co-nominals. This semantics is the outcome of a dual characterization which is discussed in detail and in full generality in [9, Sect. 2], and is reported on in the appendix for the part directly relevant to this paper. The most peculiar feature of this semantics is that formulas are satisfied at $a\in A$ and co-satisfied (refuted) at $x\in X$.

Definition 4

An RS-frame for $\mathcal {L}$ is a structure $\mathbb {F} = (\mathbb {P},R)$ where $\mathbb {P} = (A,X,\perp )$ is an RS-polarity, and $R\subseteq A\times X$ such that the images and pre-images of singletons under R are Galois-closed, i.e. for every $x\in X$ and $a\in A$,

$$\begin{aligned} R^{-1}[x]^{\uparrow \downarrow }\subseteq R^{-1}[x]~ and ~ R[a]^{\downarrow \uparrow }\subseteq R[a]. \end{aligned}$$

Relations R which satisfy this condition are called RS-compatible.

The additional conditions on R are compatibility conditions guaranteeing that the following assignments respectively define the operations $\Box$ and associated with R on the lattice $\mathbb {P}^+$: for every $U\in \mathbb {P}^+$,

Definition 5

For every RS-frame $\mathbb {F} = (\mathbb {P},R)$, its complex algebra is the lattice expansion $\mathbb {F}^+: = (\mathbb {P}^+, \Box )$ where $\Box$ is defined as above.

Lemma 2

$\le \circ \ R\ \circ \le \ \subseteq R$ for every RS-frame $\mathbb {F} = (\mathbb {P},R)$.

An RS-model for $\mathcal {L}$ on $\mathbb {F}$ is a structure $\mathbb {M} = (\mathbb {F}, v)$ such that $\mathbb {F}$ is an RS-frame for $\mathcal {L}$ and v is a variable assignment mapping each $p\in \mathsf {PROP}$ to a pair $(V_1(p), V_2(p))$ of Galois-stable sets in $\mathcal {P}(A)$ and $\mathcal {P}(X)$ respectively. In a model for the expanded language with , nominals and conominals, variable assignments also map nominals $\mathbf {j}$ to $(j^{\uparrow \downarrow }, j^{\uparrow })$ for some j in A and co-nominals $\mathbf {m}$ to $(m^{\downarrow }, m^{\downarrow \uparrow })$ for some m in X.

The following table reports the recursive definition of the satisfaction and co-satisfaction relations on $\mathbb {M}$:

The following lemma is proven easily by simultaneous induction on $\phi$ and $\psi$ using the truth definitions above. The base cases for 0 and 1 use conditions (r1) and (r2) and those for proposition letters, nominals and co-nominals follow from the way valuations are defined.

Lemma 3

For all formulas $\phi$ and $\psi$ it holds that

• 1. $\mathbb {M}, a \Vdash \phi$ iff for all $x \in X$, if $\mathbb {M}, x \succ \phi$ then $a \perp x$, and

• 2. $\mathbb {M}, x \succ \psi$ iff for all $a \in A$, if $\mathbb {M}, a \Vdash \psi$ then $a \perp x$.

An inequality $\phi \le \psi$ is true in $\mathbb {M}$, denoted $\mathbb {M} \Vdash \phi \le \psi$, if for all $a \in A$ and all $x \in X$, if $\mathbb {M}, a \Vdash \phi$ and $\mathbb {M}, x \succ \psi$ then $a \perp x$.

Remark 1

It follows from Lemma 3 that $\mathbb {M} \Vdash \phi \le \psi$ iff for all $a \in A$, if $\mathbb {M}, a \Vdash \phi$ then $\mathbb {M}, a \Vdash \psi$. It also follows that $\mathbb {M} \Vdash \phi \le \psi$ iff for all $x \in X$, if $\mathbb {M}, x \succ \psi$ then $\mathbb {M}, x \succ \phi$. We will find these equivalent characterizations of truth in a model useful when treating examples.

2.5 Standard Translation on RS-frames

As in the Boolean case, each RS-model $\mathbb {M}$ for $\mathcal {L}$ can be seen as a first-order structure, albeit two-sorted. Accordingly, we define correspondence languages as follows.

Let $L_1$ be the two-sorted first-order language with equality built over the denumerable and disjoint sets of individual variables $\mathsf {A}$ and $\mathsf {X}$, with binary relation symbol $\perp$, R, and two unary predicate symbols $P_1, P_2$ for each $p \in \mathsf {PROP}$.⁸

We will further assume that $L_1$ contains denumerably many individual variables $i, j, \ldots$ corresponding to the nominals $\mathbf {i}, \mathbf {j}, \ldots \in \mathsf {NOM}$ and $n, m, \ldots$ corresponding to the co-nominals $\mathbf {n}, \mathbf {m}\in \mathsf {CO\text {-}NOM}$. Let $L_0$ be the sub-language which does not contain the unary predicate symbols corresponding to the propositional variables. Let us now define the standard translation of $\mathcal {L}^+$ into $L_1$ recursively:⁹

The following is a variant of [9, Lemma 2.5].

Lemma 4

For any $\mathcal {L}$-model $\mathbb {M}$ and any $\mathcal {L}^+$-inequality $\phi \le \psi$, it holds that $\mathbb {M} \Vdash \phi \le \psi$    iff    $\mathbb {M} \,\models \, \forall a \forall x [\mathrm {ST}_a(\phi ) \wedge \mathrm {ST}_x(\psi ) \rightarrow a \perp x]$    iff    $\mathbb {M} \,\models \, \forall a [\mathrm {ST}_a(\phi ) \rightarrow \mathrm {ST}_a(\psi )]$    iff    $\mathbb {M}\, \models \,\forall x [\mathrm {ST}_x(\psi ) \rightarrow \mathrm {ST}_x(\phi )]$.

2.6 Examples

So far we have seen that the environment of RS-frames provides a mathematically motivated generalization of the correspondence theory which was key to the success of classical normal modal logic as a formal framework in multiple settings. The focus of this paper is to try and understand whether and how this generalized environment can retain some of the intuition which made Kripke semantics and modal logic so appealing. Let us start with the inequality $\Box 0\le 0$, which corresponds on Kripke frames to the condition that every state has a successor.

To justify the last equivalence, notice that by definition, in RS-polarities no object a verifies $\forall x (a \perp x)$. Hence the condition in the penultimate line is true precisely when the premise of the implication is false. This condition says that every state is not R-related to some co-state; the condition on Kripke frames is recognizable modulo suitable insertion of negations. Next, let us consider the inequality $\Box p\le p$, which corresponds on Kripke frames to the condition that R is reflexive.

since by definition, $\mathrm {ST}_{a}(\mathbf {m}) = a \perp m$, and $\mathrm {ST}_{a}(\Box \mathbf {m})= \forall y(m\le y \rightarrow a R y)$ can be rewritten as $m{\uparrow }\subseteq R[a]$, which is equivalent to aR m, since $R\ \circ \le \ \subseteq R$ (cf. Lemma 2). To recognize the connection with the usual reflexivity condition, observe that $\forall a \forall m(a R m \rightarrow a \perp m)$ is equivalent to $R\subseteq \perp$, and the reflexivity of a relation $R\subseteq A\times A$ can be written as $\text {Id}\subseteq R$, which is equivalent to $R^c\subseteq {\text {Id}}^c$.

Clearly, $\Box p \le p$ implies $\Box \Box p \le \Box p$. Let us consider the converse inequality, which in the classical setting corresponds to transitivity:

where

While, again, with a bit of work it is possible to retrieve the transitivity condition in this new interpretation, already with a relatively simple inequality such as $\Box p \le \Box \Box p$ this game is not really useful for the purpose of gaining a better intuitive understanding of this semantics, since it requires jumping through too many hoops (the accessibility relation on states is here encoded into a ‘non unaccessibility’ relation between states and co-states), and quickly becomes awkward and unintuitive. In the next section, we will argue that better results can be achieved by taking it as primitive, rather than as the generalization of some other semantics.

3 Conceptualizing RS-semantics via Categorization Theory

In the present section, we propose a conceptualization of the notions introduced in the previous section based on ideas from categorization theory in management science. The starting point of this conceptualization is the very well known idea, core to Formal Concept Analysis, that polarities $(A, X, \perp )$ are abstract representations of databases, in which A and X are sets of objects and properties respectively, and $\perp$ encodes information about whether a given object satisfies a given property. More specifically, we propose to think of a given polarity $\mathbb {P} = (A, X, \perp )$ as a database such that A is the set of all products in a given market at a certain moment (e.g. all models of cars, or models of togas on sale in the Netherlands in a given year), and X all the relevant observable features of these products. The specialization pre-order $a\le b$ on objects (a has at least all the features that b has) can then be read as ‘product a is at least as specified (i.e. rich in features) as product b’ and the one on features $x\le y$ (any product having x has also y) as ‘feature y is more generic than feature x’. The RS-conditions on the database can then be understood as follows:

• (s1): Any two distinct products can be told apart by some feature;

• (s2): For any two distinct features there is a product having one but not the other;

• (r1): For any product a, if there are strictly more specified products than a in the market, then they all share some feature x which a does not have;

• (r2): For any feature x, if there are strictly more generic features than x, then some product a exists which has all of them but not x.

The separation conditions (s1) and (s2) seem rather intuitive and do not require much explanation; (r1) can be enforced by suitably adding ‘artificial’ features to the database, and (r2) can be enforced by removing features from the database which are the exact intersection of two or more generic features.¹⁰ Clearly, removing such features can always be done without loss of descriptive power. We can always enforce the separation and reduction conditions, since the finite polarities we consider are a subclass of the so-called doubly founded polarities, for which this is always possible, see [23].

Arguably, the reformulation of the RS-conditions in terms of products and features makes them easier to grasp.

Further, we propose to understand the lattice $\mathbb {P}^+$ as the collection of ‘candidate categories’. That is, each element of $\mathbb {P}^+$ is a set of products which is completely identified by the set of features common to its elements. That is, any product with all these features is a member of the ‘candidate category’. We refer to these categories as ‘candidate’ since they are purely implicit in the database, and not necessarily the target of any social construction. In particular, only a restricted subset of candidate categories will support the interpretation of socially meaningful categories (which have labels such as western, opera, bossa-nova, SUV, smart phone etc.). Labels of socially meaningful categories can be assigned to ‘candidate categories’ in the usual way, namely, by means of an assignment v which associates each atomic category label $p\in \mathsf {PROP}$ to a category viewed both extensionally as $V_1(p)\subseteq X$ and intensionally as $V_2(p)\subseteq A$.¹¹ Notice the perfect match between the encoding of the meaning of atomic propositions on Kripke models and of atomic category labels on RS-models: the meaning of atomic proposition p is given as the set of states at which p holds true; the meaning of atomic category label p is given as the set of products which are the members of p, and the set of features which describe p. In what follows, we will refer to the intension of a category (cf. Footnote 6) as its description, and we say that a feature describes a category if it belongs to its description.

Given such an assignment,¹² the database is endowed with a structure of an $\mathcal {L}$-model $\mathbb {M}$, in such a way that, for every formula (category label) $\phi \in \mathcal {L}$, any $a\in A$ and $x\in X$, the symbols $\mathbb {M}, a \Vdash \phi$ and $\mathbb {M}, x \succ \phi$ can be understood as ‘object a is a member of category $\phi$’, and ‘feature x describes category $\phi$’. One immediately apparent advantage of this conceptualization is that it provides an intuitive way to understand $\succ$ from first principles rather than as the negative counterpart of $\Vdash$.

The other advantage concerns the understanding of the connectives $\wedge$ and $\vee$ in the general lattice environment. The issue is that their standard interpretation as conjunction and disjunction does not seem completely right, since distributivity seems hardwired in the way we understand ‘and’ and ‘or’ in natural language. The satisfaction clauses for $\wedge$ and $\vee$ formulas read:

These clauses say that the category $\phi \wedge \psi$ is the one whose members are members of both categories $\phi$ and $\psi$; hence, these products will satisfy at least both the description of $\phi$ and of $\psi$, and hence the description of $\phi \wedge \psi$ contains at least the union of these descriptions. The category $\phi \vee \psi$ is described by the intersection of the descriptions of $\phi$ and of $\psi$. Hence, membership in $\phi \vee \psi$ only requires products to satisfy this smaller set of features, and typically includes much more than the union of the members of the two categories. So for instance, $\mathsf {bird}\vee \mathsf {cat}$ would exclude reptiles, insects and fish, but include vertebrate homeothermic species such as the platypus. This interpretation of $\wedge$ and $\vee$ makes it possible to understand intuitively why distributivity fails. Indeed, a member of $(\mathsf {phone}\vee \mathsf {smartphone}) \wedge (\mathsf {kettle}\vee \mathsf {smartphone})$ is guaranteed to have all the features in the description of $\mathsf {phone}$ (and in fact, $\mathsf {kettle}\vee \mathsf {smartphone}$ is so general that can be assumed to not add any feature that $\mathsf {phone}$ does not have already). However, this might be not enough for it to be a member of $(\mathsf {phone}\wedge \mathsf {kettle})\vee \mathsf {smartphone}$, given that the category $\mathsf {phone}\wedge \mathsf {kettle}$ has no members (hence its description consists of all features), and so the members of $(\mathsf {phone}\wedge \mathsf {kettle})\vee \mathsf {smartphone}$ must have at least all the features in the description of $\mathsf {smartphone}$.

Now that we have a working understanding of $\Vdash$ and $\succ$, we can recognize the normal box-type operator on $\mathbb {P}^+$ as the perspective of a single agent on categories. Accordingly, $\mathbb {M}, a \Vdash \Box \phi$ and $\mathbb {M}, x \succ \Box \phi$ can be understood as ‘object a is a member of category $\phi$ according to the agent’, and ‘feature x describes category $\phi$ according to the agent’. The normality conditions $\Box \top = \top$ and $\Box (\phi \wedge \psi ) = \Box \phi \wedge \Box \psi$ can be understood as rationality requirements: that is, the agent correctly recognizes the ‘uninformative’ category $\top$ as such, and her understanding/perception of the greatest common subcategory of any two categories $\phi$ and $\psi$ is the greatest common subcategory of the categories she understands as $\phi$ and $\psi$.

On the side of the database, the agent is modelled as a relation $R\subseteq A\times X$. Hence, aRx intuitively reads ‘object a has feature x according to the agent’. Unsurprisingly, the additional properties of R (cf. Lemma 2) can be also understood as rationality requirements: if aRx then aRy for every $y\ge x$ says that if the agent attributes feature x to product a, then the agent will attribute to a also all the features which are ‘implied’ by x. Likewise, if aRx then bRx for every $b\le a$ says that if the agent attributes feature x to product a, then the agent will attribute x also to all the products which are ‘more specified’ than a.

Like in the classical case, two modal operators, $\Box$ and , are associated with the same relation R. However, these operations are not dual to each other, in the sense of e.g. $\Diamond : = \lnot \Box \lnot$, but are rather adjoints to each other, that is, for all $u, v\in \mathbb {P}^+$,

In fact, rather than encoding the dual perspective on the subjectivity of the agent that $\Box$ encodes, the operation encodes the same perspective that $\Box$ encodes, only geared towards objects while $\Box$ is geared towards features. Indeed, for every object j and every feature m, denoting by $\mathbf {j}$ and $\mathbf {m}$ the categories respectively generated by j and m,

Thus, the information jRm (‘the agent attributes feature m to object j’) is encoded on the side of the categories both by saying that m describes the category (the one the agent understands as the category generated by j), and by saying that j is a member of the category $\Box \mathbf {m}$ (the one the agent understands as the category generated by m). As to the defining clauses of the recursive definition of $\Vdash$ and $\succ$, by definition, $\mathbb {M}, a\Vdash \Box \phi$ is the case iff for all features x, if $\mathbb {M}, x \succ \phi$, then aR x. That is, product a is recognized by the agent as member of category $\phi$ iff the agent attributes to a all the features that belong to the description of $\phi$.

Moreover, by definition, $\mathbb {M}, x \succ \Box \phi$ iff for all $a\in A$, if $\mathbb {M}, a \Vdash \Box \phi$, then $a \perp x$. That is, feature x pertains to the description of category $\phi$ according to the agent iff x is verified by each object a that the agent recognizes as a member of $\phi$.

Two modal axioms commonly considered in epistemic logic are ‘reflexivity’ $\Box p\le p$ and ‘transitivity’ ($\Box p \le \Box \Box p$). The axiom $\Box p\le p$ is interpreted epistemically as the factivity of knowledge (‘if the agent knows that p then p is true’). The first-order correspondent of the factivity axiom on RS-frames is $\forall a \forall x(aRx\rightarrow a\perp x)$, which indeed expresses a form of factivity, in that it requires that whenever the agent attributes any feature x to any product a, then it is indeed the case that x is a feature of a. The axiom $\Box p\le \Box \Box p$ is interpreted epistemically as the positive introspection of knowledge (‘if the agent knows that p, then the agent knows that she knows that p’). The first-order correspondent of the positive introspection axiom on RS-frames is $\forall a \forall m(a Rm \rightarrow R^{-1}[m]^{\uparrow }\subseteq R[a])$, expressing the condition that if an agent attributes feature m to product a, then she will attribute to a all the features which are shared by the products to which she attributes m. To understand the link between this condition and positive introspection, consider the category $\Box \mathbf {m}$, i.e. the category which the agent understands as the one generated by a given feature m.¹³ This category can be identified with the tuple $(R^{-1}[m], R^{-1}[m]^{\uparrow })$. That is, the members of $\Box \mathbf {m}$ are the products to which the agent attributes m (recall that $R^{-1}[m]$ is a Galois-stable set by Definition 4) and the description of $\Box \mathbf {m}$ is the set of the features which the products in $R^{-1}[m]$ have in common. By definition, $b\perp z$ for every $b\in R^{-1}[m]$ and $z\in R^{-1}[m]^{\uparrow }$. The first-order correspondent of $\Box p \le \Box \Box p$ requires that bRz for such b and z. So, while factivity corresponds to $R\subseteq \perp$, positive introspection gives the reverse inclusion restricted to products and features pertaining to ‘boxed categories’. That is, the agent must be aware of the features of the products of the categories that she knows.

4 Categories as Social Constructs

In the present section, we introduce a formal account of the emergence of categories as the outcome of a process of social interaction. We consider for the sake of simplicity a setting of two agents. Accordingly, we consider the bi-modal logic $\mathcal {L}$ which is the axiomatic extension of the basic normal LE-logic for two unary normal box-type modal operators, 1 and 2, with the axioms $ip\le p$ and $ip\le iip$ for $1\le i\le 2$. Models for this logic are structures $(\mathbb {P}, R_1, R_2, v)$ such that $\mathbb {P} = (X, A, \perp )$ is an RS-polarity, $R_i\subseteq A\times X$ for $1\le i\le 2$, such that the following conditions hold:

• 1. $\forall x(R_i^{-1}[x]^{\uparrow \downarrow }\subseteq R_i^{-1}[x])$;

• 2. $\forall a(R_i[a]^{\downarrow \uparrow }\subseteq R_i[a])$;

• 3. $R_i\subseteq \perp$;

• 4. $\forall a \forall x(a R_i x \rightarrow R_i^{-1}[x]^{\uparrow }\subseteq R_i[a])$,

and v is an assignment which associates each $p\in \mathsf {PROP}$ to an element of $\mathbb {P}^+$ viewed both extensionally as $V_1(p)\subseteq A$ and intensionally as $V_2(p)\subseteq X$ in such a way that $V_1(p) = V_2(p)^{\downarrow }$ and $V_2(p) = V_1(p)^{\uparrow }$.

In this setting, a common knowledge-type construction can be performed which yields an expansion, denoted $\mathcal {L}_C$, of the bi-modal LE-logic above with a normal box-type operator C, the interpretation of which on $\mathbb {P}^+$, given the additional axioms, is given as follows: for any $u\in \mathbb {P}^+$,

$$\begin{aligned} C(u): = \mathop {\bigwedge }\nolimits _{{s\in S}}su, \end{aligned}$$

where S is the set of all compound modalities of the forms $(ij)^n$ and $i(ji)^n$, for $1\le i\ne j\le 2$ and for some $n\in \mathbb {N}$.

Lemma 5

$C(u)\le u$ and $C(u)\le C(C(u))$ for any $u\in \mathbb {P}^+$.

Let $R_C, R_s\subseteq A\times X$ for any $s\in S$ be defined as follows: $aR_s x$ iff $a\le s x$ and $aR_C x$ iff $a\le C(x)$. Clearly, $R_C = \bigcap _{s\in S} R_s$. In the standard setting of epistemic logic, the accessibility relations associated with agents do not directly encode the agents’ knowledge but rather their uncertainty. Hence, on the relational side, the relation associated with the common knowledge operator is defined as the reflexive transitive closure of the union of the relations associated with individual agents, which is typically much bigger than those associated with individual agents. In the present setting, relations associated with agents directly encode what agents positively know rather than their uncertainty. Consequently, the common knowledge relation $R_C$ is the intersection of the relations $R_s$ encoding the finite iterations, which is typically much smaller.

As both C and every $s\in S$ are compositions of normal box-operators, they are themselves normal box-operators. Hence the relations $R_C$ and $R_s$ they give rise to are RS-compatible (cf. Definition 4). Thus, the correspondence reductions discussed in Sect. 2.6 apply to C and $R_C$, yielding:

Lemma 6

The relation $R_C$ defined above verifies the following conditions:

• 1. $R_C\subseteq \perp$;

• 2. $\forall a \forall x(a R_C x \rightarrow R_C^{-1}[x]^{\uparrow }\subseteq R_C[a])$.

For any given category label $\phi$, the category $C(\phi ) = \bigwedge \{C(\mathbf {m})\mid \phi ^{\mathbb {P}^+}\le \mathbf {m}\}$. For this reason, in what follows we restrict our attention to categories $C(\mathbf {m})$ for some feature $m\in X$. The members of $C(\mathbf {m})$ are the products in the set $R^{-1}_C[m] = (\bigcap _{s\in S}R_s)^{-1}[m]$, and the description of $C(\mathbf {m})$ is $R^{-1}_C[m]^{\uparrow } = ((\bigcap _{s\in S}R_s)^{-1}[m])^{\uparrow }$. These can be understood as the socially constructed categories, the membership and description of which are socially agreed upon. Clearly, there are many less of them than candidate categories, which agrees with our intuition.

5 Conclusion and Further Research

In this paper we have proposed an interpretation of RS-semantics in terms of agents’ reasoning about objects, their properties and the categories induced by the accompanying relation. We have argued that this semantics is particularly well adapted to this interpretation and, conversely, that through this interpretation one could gain an intuitive understanding of the semantics.

Our proposal has a distinctly epistemic character, but one which differs from standard epistemic logic in at least two respects: firstly, the relations used to interpret the epistemic operators are intended to capture positive knowledge, rather than uncertainty; secondly, these relations relate objects to features rather than possible worlds to one another. We considered two classical principles of epistemic logic, namely factivity and positive introspection. By applying the correspondence theory of [9] we computed the relational properties corresponding to these principles, i.e. necessary and sufficient conditions on an agent’s incidence relation between objects and properties for her knowledge of categories to verify these epistemic principles. Various questions for further investigation remain open here: what is the meaning of other classical epistemic principles, like e.g. negative introspection, in this setting? Are there other principles that should be included in a minimal logic of categorization? Of course, all of this depends on the reasoning abilities and level of access to reality we wish to attribute to agents. Moreover, most standard logical questions remain open: axiomatizations, proof systems, decidability, complexity, etc.

This paper is a first assay in using RS-semantics for reasoning about categorization and, as such, remains quite general in its assumptions. To be of more immediate practical relevance, the considerations here should be specialized to particular fields of enquiry where categorization plays or could play a prominent role. Below we briefly consider three such fields.

Natural Language Semantics. We have seen that the assignments of RS-models support a notion of meaning that is different from the one in classical modal logic, but is recognizably what the meaning of category labels should be: namely, a semantic category specified as the set of its members and the set of features describing it. In natural language semantics, linguistic utterances are assigned a meaning in the same spirit, which generalizes the truth-based semantics of sentences. More generally, categories or concepts are fundamental to the construction of meaning in natural language, since each noun is naturally associated with a category. Exploring systematic connections between categories and natural language semantics is a promising direction for further research.

Knowledge Representation and Formal Ontologies. Categories are central to any form of knowledge representation. Description logics [1] are one of the dominant paradigms for logical reasoning in this context. Our formalism represents a different and possibly complementary perspective on the formal ontologies, classification systems, and taxonomies studied there. In particular, the non-distributive nature of category formation and the two-level separation between objects and features are foreign to the description logics paradigm. It is natural to ask to what degree the various expressive features of description logic (like uniqueness quantification, qualified cardinality restrictions etc.) could be accommodated in our framework, and future extensions will study this question.

Categorization Theory in Management Science. As already indicated, this was one of our main sources of inspiration for the proposals of the present paper. Our formalism is a first step in the direction of a formal logical account of the real world phenomena studied by categorization theorists. There are various considerations that make it an attractive framework in which to study categorization and in which to formulate empirically testable hypotheses. We mention two of these reasons: Firstly, it allows one to study the effects of adding or removing objects with new properties and/or properties already associated with other categories, thus allowing for a fine grained analysis of the likely changes in a classification system resulting from innovations of different kinds.

Secondly, our approach gives us all potential categories “automatically", while only some of them are real, socially agreed upon categories for economic decision-makers. It can therefore serve as a powerful instrument to better study and understand the causes and consequences of the selection of real categories from the broader set of potential ones. To start with, different real world domains could be compared with respect to the ratios of real to potential categories present in them. One reasonable conjecture seems to be that these ratios will depend a lot on competitive dynamics and the matureness of categories, while also having an effect on them. One could the go on to study changes over time in these ratios as well as the differences in ratios—and their changes—among different audiences espousing different classifications.

Extensions and Variations. In closing, we mention two of the many possible extensions of the present framework: category membership does not need to be absolute, as products can simultaneously have different grades of membership in different categories. This calls for quantitative, possibly many-valued versions of our semantics. Also, the categories in a given market do not need to be static, but can evolve and change over time as new products with new features or new combinations of existing features enter the market [41, 42]. Dynamic versions of our formalism would be suitable to deal with such continuously evolving categorization systems.

Appendices

A Relational Semantics via Dual Characterization

The dual correspondence between perfect lattices and RS-polarities serves as a base to generalize the Kripkean semantics of modal logic to logics with possibly non-distributive propositional base. Analogous to the dual correspondence between Kripke frames and complete and atomic Boolean algebras with operators, one would want a dual correspondence between perfect normal lattice expansions and RS-polarities endowed with additional relations. In [9, Sect. 2], a method for computing the definition of the relations dually corresponding to normal modal operators was discussed and illustrated for a certain modal signature consisting of unary and binary modal operators.

In this subsection we will report on this method, for an expansion $\mathcal {L}$ of the basic lattice language with a unary box-modality, canonically interpreted on lattices endowed with a completely meet-preserving operation. Moreover, we will derive, by means of a dual characterization argument, its interpretation on expanded RS-polarities.

We take the connection between the satisfaction relation $\Vdash$ in Kripke frames and the interpretation of modal formulas in BAOs as our guideline: let $\mathbb {F} = (W, R)$ be a Kripke frame. From the satisfaction relation $\Vdash \subseteq W\times \mathcal {L}$ between states of $\mathbb {F}$ and formulas, an interpretation $\overline{v}: \mathcal {L}\rightarrow \mathbb {F}^+$ into the complex algebra of $\mathbb {F}$ can be defined, which is an $\mathcal {L}$-homomorphism, and is obtained as the unique homomorphic extension of the equivalent functional representation of the relation $\Vdash$ as a map $v: \mathsf {PROP}\rightarrow \mathbb {F}^+$, defined as $v(p) = {\Vdash }^{-1}[p]$ ¹⁴. In this way, interpretations can be derived from satisfaction relations, so that for any $a\in J^{\infty }(\mathbb {F}^+)$ and any formula $\phi$,

$$\begin{aligned} a\Vdash \phi \quad \text{ iff } \quad a\le \overline{v}(\phi ), \end{aligned}$$

(1)

where, on the left-hand side, $a\in J^{\infty }(\mathbb {F}^+)$ is identified with a state of $\mathbb {F}$ via the isomorphism $\mathbb {F}\cong (\mathbb {F}^+)_+$. Conversely, consider a perfect lattice with completely meet-preserving operation $\mathbb {C} = (\mathbb {L}, \Box )$, and a homomorphic assignment $\overline{v}: \mathcal {L}\rightarrow \mathbb {C}$, and recall that the complete lattice $\mathbb {L}$ can be identified with the lattice $\mathbb {P}^+$ arising from some RS-polarity $\mathbb {P} = (A, X, \perp )$. We want to define a suitable relation $R = R_{\Box }$ and satisfaction relation $\Vdash _{\overline{v}}$ satisfying the condition (1). The method we are going to illustrate hinges on the dual characterization of $\overline{v}$ as a pair of relations $(\Vdash _{\overline{v}}, \succ _{\overline{v}})$ such that $\Vdash _{\overline{v}}\ \subseteq \ J^{\infty }(\mathbb {L})\times \mathcal {L}\cong A\times \mathcal {L}$ and $\succ _{\overline{v}}\ \subseteq \ M^{\infty }(\mathbb {L})\times \mathcal {L}\cong X\times \mathcal {L}$. This dual characterization is established by induction on formulas.

The base of the induction is clear: for every $a\in J^{\infty }(\mathbb {P}^+)$ and every $p\in \mathsf {PROP} \cup \{0, 1 \}$, we define

$$\begin{aligned} a\Vdash _{\overline{v}} p\quad \text{ iff } \quad a\le \overline{v}(p). \end{aligned}$$

(2)

Now let us turn to the inductive step for the box. Since $\overline{v}: \mathcal {L}\rightarrow \mathbb {P}^+$ is a homomorphism, $\overline{v}(\Box \phi ) = \Box ^{\mathbb {P}^+}\overline{v}(\phi )$. Suppose that (1) holds for $\phi$.

Since $\mathbb {P}^+$ is perfect, $\overline{v}(\phi ) = \bigwedge \{x \in M^{\infty }(\mathbb {L}) \mid \overline{v}(\phi ) \le x\}$. Thus,

Notice that, at the end of this chain of equivalence, we have equivalently reduced the whole information on $\Box$ to the information whether $a \le \Box ^{\mathbb {P}^+} x$ for each a and x. So this can be taken as the definition of the relation $R\subseteq A\times X$: we let aRx iff $a \le \Box ^{\mathbb {P}^+} y$.

To turn the last clause above into a satisfaction clause for $\Box$, we firstly replace $M^{\infty }(\mathbb {L})$ with X, which we identify via the isomorphism $\mathbb {P}\cong (\mathbb {P}^+)_+$. Secondly, we need to recall the second relation $\succ _{\overline{v}}$ between elements of X and formulas, obeying the following condition, which is to be defined by induction on the structure of the formulas in such a way that the following condition holds, analogously to (1):

$$\begin{aligned} x \succ \phi \quad \text{ iff } \quad \overline{v}(\phi ) \le x. \end{aligned}$$

(3)

These considerations produce the following satisfaction clause for $\Box$:

The co-satisfaction relation $\succ$ deserves some further comment: in the Boolean and distributive settings, $\succ$ is completely determined by $\Vdash$, and is hence not mentioned explicitly there. Here, in the non-distributive setting, the relation needs to be defined along with $\Vdash$. Equation (3) determines the base case:

$$\begin{aligned} y\succ \overline{v}(p)\quad \text{ iff } \quad \overline{v}(p)\le y. \end{aligned}$$

(4)

Specializing the clause above to powerset algebras $\mathcal {P}(W)$, we would have $y \succ _{V} p$ iff $V(p) \le y$ iff $V(p) \subseteq W/\{ x \}$ for some $x \in W$ iff $\{ x\} \not \subseteq V(p)$ iff $x \notin V(p)$ iff $x \not \Vdash p$, which shows that the relation $\succ$ can be regarded as an upside-down description of the satisfaction relation $\Vdash$, namely a co-satisfaction, or refutation.

The inductive step for the derivation of the co-satisfaction clause for $\Box$ goes as follows:

The last line follows from Eq. (1) for $\Box \phi$, and the identification, via the isomorphism $\mathbb {P}\cong (\mathbb {P}^+)_+$, of $J^{\infty }(\mathbb {L})$ with A, and of the lattice order $\le$ (restricted to $J^{\infty }(\mathbb {L}) \times M^{\infty }(\mathbb {L})$) with the incidence relation $\perp$ of the polarity.

B Proofs of Technical Lemmas

Proof

(Lemma 1). We only prove the part concerning z. Let $x\in z{\uparrow }^{\downarrow \uparrow }$, and let us show that $z\le x$. That is, let us fix a such that $a\perp z$, and show that $a\perp x$. Since $\perp \circ \le \subseteq \perp$, from $a\perp z$ it follows that $\forall y (z\le y\rightarrow a\perp y)$, which means that $a\in z{\uparrow }^{\downarrow }$. Since by assumption $x\in z{\uparrow }^{\downarrow \uparrow }$, this implies that $a\perp x$, as required.

Proof

(Corollary 1). Since $z{\uparrow }$ is Galois-stable and contains z and, by definition, $z^{\downarrow \uparrow }$ is the smallest such set, $z^{\downarrow \uparrow }\subseteq z{\uparrow }$. For the converse inclusion, let $z\le y$ and $a\perp z$. As $\perp \circ \le \subseteq \ \perp$, this implies $a\perp y$, which shows that $y\in z^{\downarrow \uparrow }$, as required.

Proof

(Lemma 2). Assume that aRz and $z\le y$. To show that $y\in R[a]$, by the second compatibility condition, it is enough to show that $y\in R[a]^{\downarrow \uparrow }$. That is, let us fix $b\in R[a]^{\downarrow }$ and show that $b\perp y$. From $b\in R[a]^{\downarrow }$ and aRz it follows that $b\perp z$. This and $z\le y$ imply that $b\perp y$, given that $\perp \ \circ \ \le \,\subseteq \ \perp$. The remaining part is proven similarly.

Proof

(Lemma 5). Clearly, $C(u)\le 1u\le u$, which proves the first inequality.

$$\begin{aligned} C(C(u)) = \mathop {\bigwedge }\nolimits _{{s\in S}}sC(u) = \mathop {\bigwedge }\nolimits _{s\in S}s(\mathop {\bigwedge }\nolimits _{t\in S}tu) = \mathop {\bigwedge }\nolimits _{s\in S}\mathop {\bigwedge }\nolimits _{t\in S}stu \ge \mathop {\bigwedge }\nolimits _{s'\in S}s'u = C(u). \end{aligned}$$