Disjunction and Negation in Information Based Semantics

Abstract

We investigate an information based generalization of the incompatibility-frame treatment of logics with non-classical negation connectives. Our framework can be viewed as an alternative to the neighbourhood semantics for extensions of lattice logic by various negation connectives, investigated by Hartonas. We set out the basic semantic framework, along with some correspondence results for extensions. We describe three kinds of constructions of canonical models and show that double negation law is not canonical with respect to any of these constructions. We also compare our semantics to Hartonas’.

This paper is an outcome of the project Logical Structure of Information Channels, no. 21-23610M, supported by the Czech Science Foundation and realized at the Institute of Philosophy of the Czech Academy of Sciences.

1 Introduction

A characteristic feature of relational semantics is that it is based on a relation $\vDash$, which in any given model relates elements of the model and formulas of some language. For example, in the standard Kripke semantics for modal logics the elements of Kripke models represent possible worlds and $\vDash$, as a relation between possible worlds and formulas, is conceived of as the relation of truth. Motivated by this interpretation, the following semantic clauses for conjunction, disjunction, and negation are postulated:

• ($\wedge$) $s \vDash \alpha \wedge \beta$ iff $s \vDash \alpha$ and $s \vDash \beta$,

• ($\vee$) $s \vDash \alpha \vee \beta$ iff $s \vDash \alpha$ or $s \vDash \beta$,

• ($\lnot$) $s \vDash \lnot \alpha$ iff $s \nvDash \alpha$.

As a consequence, these connectives behave in accordance with classical logic in Kripke semantics. To avoid various features of classical logic, relational semantic frameworks for various non-classical logics, like, for example, intuitionistic logic and relevant logics, replace possible worlds with some more general entities, which we might neutrally call states. With respect to these states negation does not behave in this simple way, and the question of how to interpret these more general states has posed a perennial issue. One suggestion that has appeared repeatedly in the literature is that they should be viewed as bodies of information, i.e. as information states.¹ The relation $\vDash$ between such states and formulas should perhaps be called (informational) support rather than truth. But the crucial thing is that with respect to such interpretation the clause ($\lnot$) for negation seems implausible because a body of information may be incomplete and thus support neither a given sentence nor its negation, or it can be inconsistent and thus support both a sentence and its negation. Consequently, one has to introduce a different semantic clause for negation. When the clause ($\lnot$) for negation is abandoned the space for non-classical logics is opened.

It is quite common that even if possible worlds are replaced with abstract states and the semantics of negation is modified, the structure of the semantic clauses ($\wedge$) and ($\vee$) for conjunction and disjunction is preserved.² However, from the informational perspective there seems to be some asymmetry between conjunction and disjunction. The clause ($\wedge$) still makes a good sense even if we replace possible worlds with information states (a body of information supports a conjunction iff it supports both conjuncts). However, it has been pointed out many times that the clause ($\vee$) for disjunction is implausible in the informational interpretation, just like the clause ($\lnot$) for negation.³ A body of information may support a disjunction even if it does not support any of its disjuncts. If, for instance, we conceive of a body of information as that being available to an agent in the course of some reasoning task, then we know from experience that we may have information that a disjunction holds without any information about which of the disjuncts holds.

Several alternative treatments of disjunction have been proposed in the literature. For example, while Kripke semantics for intuitionistic logic [17] accepts the clause ($\vee$) for disjunction, the so called Beth semantics [2] for intuitionistic logic treats disjunction in a more complex way.

In the informational perspective one can characterize disjunction in this way, which shall be our approach: the disjunction of $\alpha$ and $\beta$ is what two states have in common if one of them supports $\alpha$ and the other one supports $\beta$. In other words, if an information state s supports $\alpha \vee \beta$ then it contains the common content of the information expressed by $\alpha$ and the information expressed by $\beta$. If this is taken as the characteristic property of disjunction, one can transform it into a semantic clause. Assume that $s \circ t$ represents the common (informational) content of the states s and t and $s \le u$ expresses that the information of s is contained in the information of u. Then we obtain the following:

• ($\vee$)’ $s \vDash \alpha \vee \beta$ iff there are states t, u such that $t \vDash \alpha$, $u \vDash \beta$, and $t \circ u \le s$.

For example, assume that information states are conceived as sets of possible worlds (as is common in epistemic logic [8]) and a formula is supported by an information state iff it is true (in the sense of classical logic) in every possible world of the state. Then the common content of two states coincides with union (a formula is true in all worlds of s  and all worlds of t iff it is true in all worlds of $s \cup t$) and informational inclusion $\le$ coincides with the superset relation. It indeed holds in this setting that a disjunction is supported by an information state iff the state is a subset of the union of two states, t and u, such that t supports the first disjunct and u supports the second disjunct. For instance, one can take t to be the set of all worlds in which the first disjunct is true and u the set of all worlds in which the second disjunct is true.

Dually, information states can be represented as theories (of some standard logical system like classical logic, intuitionistic logic, relevant logic or fuzzy logic) and a formula is supported by a state iff it belongs to the corresponding theory. In that case the common content coincides with intersection and informational inclusion coincides with the subset relation. Then it holds that a state s supports a disjunction iff there are two theories t and u (e.g. the theories generated by the two disjuncts) such that t supports the first disjunct, u supports the second disjunct, and $t \cap u \subseteq s$.

The clause ($\vee$)’ can be viewed as capturing the general structure of these cases. Our framework will be based on this clause. A similar semantic treatment of disjunction has been employed for example in [6, 9, 16, 19].⁴

As regards negation, we will adopt the semantic characterization in terms of a primitive incompatibility relation, following work by Goldblatt [11] on ortholattices, and Dunn [7] and Restall [22] on relevant and paraconsistent negations, among other researchers working in non-classical logic. The central idea is that an information state supports $\lnot \alpha$ iff the state is incompatible with any state that supports $\alpha$. As mentioned, negation interpreted in this manner has been studied in the context of non-classical logic before, but we’ll combine this treatment of negation with the treatment of disjunction mentioned above. The main aim of this paper is to investigate abstract features of negation characterized in this way in the context of information based semantics involving the mentioned treatment of disjunction, proving new completeness, frame correspondence, and canonicity results. Our framework is similar, in certain respects, to that developed by Hartonas [14], but ours has the advantage of being more concrete and, in some ways, simpler, allowing for an easier interpretation of the resulting class of models. In particular, we seek to interpret the points in the frame as state of information, and the various relations and operations thereon as dealing directly with their information, and for this purpose the more concrete approach here is a better fit than the more abstract approach taken in [14].

2 Semilattice Semantics

In this section we introduce a semilattice semantics for the language L which is built out of a set of atomic formulas At by conjunction $\wedge$ and disjunction $\vee$.⁵ A pair of L-formulas $\left\langle \alpha , \beta \right\rangle$ will be called a consequence L-pair. We will write $\alpha \vdash \beta$ instead of $\left\langle \alpha , \beta \right\rangle$. Our logical basis will be the so called lattice logic $\mathsf {LL}$ understood as a set of consequence L-pairs generated by the system consisting of the following axioms and rules:

The distributive lattice logic $\mathsf {DLL}$ is generated by the system for $\mathsf {LL}$ enriched with the following axiom:

For the semantic treatment of the logic we will use the following structures.

Definition 1

An information frame (IF) is a structure $\left\langle S, \circ , i \right\rangle$, where S is a non-empty set, $\circ$ is an associative, commutative, idempotent binary operation on S, and i is an element of S such that $s \circ i = s$.

The set S represents a space of information states. The operation $\circ$ assigns to any two states t, u the common (informational) content of t and u, i.e. a state $t \circ u$ consisting of information that the two states have in common. The element i represents the state of the absolute inconsistency (or triviality). As pointed out in the introduction, the operation $\circ$ can be conceived of either as union (of possible worlds), or as intersection (of theories). Both perspectives make good sense, so it is open to interpretation whether $\circ$ is understood as join or rather as meet. We will fix the latter perspective, so that we introduce the order of the structure in the following way: $s \le t$ iff $s \circ t = s$. In this perspective, i is the top element of the structure.

Definition 2

Let $I=\left\langle S, \circ , i \right\rangle$ be an IF. A filter in I is any subset F of S such that $i \in F$, and for any $t, u \in S$ it holds that $t \circ u \in F$ iff $t \in F$ and $u \in F$. A valuation in I is a function that assigns to each atomic formula from At a filter in I. Given a valuation V  in I, the pair $\left\langle I, V \right\rangle$ is called an information model (IM).

Equivalently, one can define filters as non-empty subsets of S that are upward closed (w.r.t. $\le$) and closed under $\circ$. Relative to a given IM, we can introduce the following semantic clauses for L-formulas:

• (a) $s \vDash p$ iff $s \in V(p)$, for any atomic formula p,

• (b) $s \vDash \alpha \wedge \beta$ iff $s \vDash \alpha$ and $s \vDash \beta$,

• (c) $s \vDash \alpha \vee \beta$ iff there are states t, u such that $t \vDash \alpha$, $u \vDash \beta$, and $t \circ u \le s$.

If $s \vDash \alpha$ we say that the state s supports the formula $\alpha$. Let M be an IM, and $\alpha$ an L-formula. Then $|| \alpha ||_M$ is the set of states in M that support $\alpha$ (the subscript will usually be omitted).

Proposition 1

$|| \alpha ||_M$ is a filter in M, for every L-formula $\alpha$.

We say that a consequence L-pair $\alpha \vdash \beta$ is valid in an IF I if $|| \alpha || \subseteq || \beta ||$, for any IM $M=\left\langle I, V \right\rangle$. The proof of the following proposition proceeds by a canonical model construction as in [19].

Proposition 2

A consequence L-pair $\alpha \vdash \beta$ is valid in all IFs if and only if it is derivable in the system $\mathsf {LL}$.

Definition 3

A distributive information frame (DIF) is an IF satisfying the following condition: if $t \circ u \le s$ then there are $t', u'$ such that $t \le t'$, $u \le u'$, and $t' \circ u'=s$.

In the distributive information frames the semantic clause for disjunction can be reformulated as in the following proposition.

Proposition 3

Let M be an IM based on a DIF, and $\alpha , \beta$ any L-formulas. Then it holds for any state s in M:

• $s \vDash \alpha \vee \beta$ iff there are states t, u such that $t \vDash \alpha$, $u \vDash \beta$, and $t \circ u = s$.

Proposition 4

A consequence L-pair $\alpha \vdash \beta$ is valid in all DIFs if and only if it is derivable in the system $\mathsf {DLL}$.

3 Incompatibility Relation in Information Frames

In this section we focus on general features of negation in the context of semilattice semantics. Our approach is based on the treatment of negation that has been extensively used in the literature on non-classical logics and that characterizes negation in terms of the following plausible semantic clause: $\lnot \alpha$ is supported by a state s if and only if any state supporting $\alpha$ is incompatible with s (see [7, 11, 22]). We extend L with negation ($\lnot$) and denote the resulting language as $L^{\lnot }$. Moreover, we enrich our models with a primitive incompatibility relation $\bot$.

Definition 4

An incompatibility proto-IF is a tuple $\left\langle S, \circ , i, \bot \right\rangle$, where $\left\langle S, \circ , i \right\rangle$ is an IF, and $\bot$ is a binary relation on S, satisfying the following monotonicity condition: if $t \bot u$ and $t \le s$ then $s \bot u$. For any $s \in S$, the set $\{t \in S~|~s\bot t \}$ will be denoted as $\bot _s$, and the set $\{t \in S~|~t\bot s \}$ as $\bot ^s$. An incompatibility proto-IM is an incompatibility proto-IF equipped with a valuation.

The semantic clause for negation is defined as follows:

• $s \vDash \lnot \alpha$ iff for any t, if $t \vDash \alpha$ then $t \bot s$.

Proposition 5

Let $I=\left\langle S, \circ , i, \bot \right\rangle$ be an incompatibility proto-IF. Then $|| \alpha ||$ is a filter in $\left\langle I, V \right\rangle$, for every valuation V and every $L^{\lnot }$-formula $\alpha$, if and only if $\bot _t$ is a filter, for every $t \in S$.

Definition 5

An incompatibility proto-IF where $\bot _t$ is a filter, for every $t \in S$, will be called simply an incompatibility IF (IIF, for short). A filter F in an IIF will be called an incompatibility filter if there is a state $t \in S$ such that $F=\bot _t$.

Proposition 6

For any IIM M and all $L^{\lnot }$-formulas $\alpha , \beta$, if $\alpha \vdash \beta$ is valid in M then $\lnot \beta \vdash \lnot \alpha$ is valid in M.

Definition 6

By a logic $\varLambda$, we will understand a set of consequence $L^{\lnot }$-pairs that (a) is closed under uniform substitution (b) contains all the axioms of the lattice logic, (c) is closed under the rules of the lattice logic, and under the following rule:

• (N) $\alpha \vdash \beta / \lnot \beta \vdash \lnot \alpha$.

Instead of $\alpha \vdash \beta \in \varLambda$, we will just write $\alpha \vdash _{\varLambda } \beta$. Given a logic $\varLambda$, a $\varLambda$-theory is defined as a non-empty set of $L^{\lnot }$-formulas $\varDelta$ satisfying the following conditions: (a) if $\alpha \in \varDelta$ and $\beta \in \varDelta$ then $\alpha \wedge \beta \in \varDelta$, (b) if $\alpha \in \varDelta$, and $\alpha \vdash _{\varLambda } \beta$ then $\beta \in \varLambda$.

Proposition 7

For any logic $\varLambda$ and all $L^{\lnot }$-formulas $\alpha , \beta$, $\lnot \alpha \vee \lnot \beta \vdash _{\varLambda } \lnot (\alpha \wedge \beta )$ and $\lnot (\alpha \vee \beta )\vdash _{\varLambda }\lnot \alpha \wedge \lnot \beta$.

Now, we will show that our framework is flexible especially in that it allows us to define for any logic various alternative canonical models. Fix an arbitrary logic $\varLambda$. We will construct three alternative canonical models for $\varLambda$. The first two constructions use $\varLambda$-theories. First, we define the following structure:

• $I^{\varLambda }_1=\left\langle S_1, \circ _1, i_1, \bot _1 \right\rangle$

where $S_1$ is the set of non-empty⁶ $\varLambda$-theories, $\varDelta \circ _1 \varGamma = \varDelta \cap \varGamma$, $i_1$ is the set of all $L^{\lnot }$-formulas, and $\bot _1$ is defined as follows:

• $\varDelta \bot _1 \varGamma$ iff there is an $\alpha \in \varDelta$ such that $\lnot \alpha \in \varGamma$.

We also define $M^{\varLambda }_1=\left\langle I^{\varLambda }_1, V_1 \right\rangle$, where $\varDelta \in V_1(p)$ iff $p \in \varDelta$.

Proposition 8

The structure $I^{\varLambda }_1$ is an IIF and $M^{\varLambda }_1$  is an IIM.

Proposition 9

For any $\varLambda$-theory $\varDelta$, and any $L^{\lnot }$-formula $\alpha$:

• $\varDelta \vDash \alpha$ in $M^{\varLambda }_1$ iff $\alpha \in \varDelta$.

As a consequence, for all $\alpha , \beta \in L^{\lnot }$, $\alpha \vdash _{\varLambda } \beta$ if and only if $|| \alpha || \subseteq || \beta ||$ in $M^{\varLambda }_1$.

Proposition 10

For any logic $\varLambda$ there is a class of IIMs  $\mathcal {C}$ such that $\varLambda$ coincides with all the consequence $L^{\lnot }$-pairs valid in $\mathcal {C}$.

Proposition 11

The set of all consequence pairs that are valid in all IIFs coincides with the minimal logic, i.e. the logic obtained by axioms and rules of the lattice logic plus the rule (N).

A negation connective obeying only (N) has been called a “subminimal negation”, following Hazen [15]. The previous construction of canonical models generalizes Goldblatt’s canonical models for orthologic [11]. Interestingly there is a quite different alternative way how to define the incompatibility relation among theories. This construction was employed by Hartonas in [14] and it works also for our setting (a more detailed discussion of the connection between our and Hartonas’ frameworks will be provided in the following section).

Definition 7

For any $\varLambda$-theory $\varDelta$ we define

• $\varDelta ^* = \{ \alpha \in L^{\lnot }~|~\text {there is }\beta \in L^{\lnot }\text { s.t. }\beta \vdash _{\varLambda } \delta \text {, for all }\delta \in \varDelta \text {, and }\lnot \beta \vdash \alpha \}$.

Note that $\varDelta ^*$ is again a (possibly empty) $\varLambda$-theory. Now, consider the following structure:

• $I^{\varLambda }_2=\left\langle S_2, \circ _2, i_2, \bot _2 \right\rangle$

where, $S_2$ is the set of all $\varLambda$-theories (including the empty one), $\varDelta \circ _2 \varGamma = \varDelta \cap \varGamma$, $i_2$ is (as before) the set of all $L^{\lnot }$-formulas, and $\varDelta \bot _2 \varGamma$ iff $\varDelta ^{*} \subseteq \varGamma$. Moreover, we define $M^{\varLambda }_2=\left\langle I^{\varLambda }_2, V_2 \right\rangle$, where $V_2=V_1$.

Proposition 12

The structure $I^{\varLambda }_2$ is an IIF and $M^{\varLambda }_2$ is an IIM.

Proposition 13

For any $\varLambda$-theory $\varDelta$, and any $L^{\lnot }$-formula $\alpha$:

• $\varDelta \vDash \alpha$ in $M^{\varLambda }_2$ iff $\alpha \in \varDelta$.

As a consequence, for all $\alpha , \beta \in L^{\lnot }$, $\alpha \vdash _{\varLambda } \beta$ if and only if $|| \alpha || \subseteq || \beta ||$ in $M^{\varLambda }_2$.

Our third construction of a canonical model is based on the structure of the Lindenbaum-Tarski algebra of $\varLambda$. Let $[\alpha ]$ denote the equivalence class determined by $\alpha$, i.e. $[\alpha ]$ is a set of $L^{\lnot }$-formulas $\beta$ such that $\alpha \vdash _{\varLambda } \beta$ and $\beta \vdash _{\varLambda } \alpha$. Let $Prop_{\varLambda } = \{[\alpha ]~|~\alpha \in L^{\lnot } \}$. We distinguish two cases. First assume that $\varLambda$ contains an explosive formula, i.e. some $L^{\lnot }$-formula $\xi$ such that $\xi \vdash \beta$ for all $\beta \in L^{\lnot }$. Then we define:

• $I^{\varLambda }_3=\left\langle S_3, \circ _3, i_3, \bot _3 \right\rangle$,

where $S_3=Prop_{\varLambda }$, $[\alpha ] \circ _3 [\beta ] = [\alpha \vee \beta ]$, $i_3=[\xi ]$, $[\alpha ] \bot _3 [\beta ]$ iff $\beta \vdash _{\varLambda } \lnot \alpha$. So, the structure consists of the Lindenbaum-Tarski algebra of $\varLambda$ turned upside down. We further define $M^{\varLambda }_3=\left\langle I^{\varLambda }_3, V_3 \right\rangle$, where $[\alpha ] \in V_3 (p)$ iff $\alpha \vdash _{\varLambda } p$.

If $\varLambda$ contains no explosive formula, the structure has to be enriched with a top element so that the definition of the structure $I^{\varLambda }_3=\left\langle S_3, \circ _3, i_3, \bot _3 \right\rangle$ is complicated in the following way:

• $S_3=Prop_{\varLambda } \cup \{ i_3 \}$, where $i_3$ is a new element, i.e. $i_3 \notin Prop_{\varLambda }$,

• for $[\alpha ], [\beta ] \in Prop_{\varLambda }$, $[\alpha ] \circ _3 [\beta ] = [\alpha \vee \beta ]$,

  and for all $s \in S_3$ we fix $s \circ _3 i_{3} = i_{3} \circ _3 s = s$,

• for $[\alpha ], [\beta ] \in Prop_{\varLambda }$, $[\alpha ] \bot _3 [\beta ]$ iff $\beta \vdash _{\varLambda } \lnot \alpha$,

  and for all $s \in S_3$, we state that $i_3 \bot _3 s$ and $s \bot _3 i_3$.

Moreover, $M^{\varLambda }_3=\left\langle I^{\varLambda }_3, V_3 \right\rangle$, where $s \in V_3 (p)$ iff $s= i_3$ or $s=[\alpha ]$ and $\alpha \vdash _{\varLambda } p$. The following two propositions hold for both these constructions.

Proposition 14

The structure $I^{\varLambda }_3$ is an IIF and $M^{\varLambda }_3$ is an IIM.

Proposition 15

For all $L^{\lnot }$-formulas $\alpha , \beta$:

• $[\alpha ] \vDash \beta$ in $M^{\varLambda }_3$ iff $\alpha \vdash _{\varLambda } \beta$.

As a consequence, for $\alpha , \beta \in L^{\lnot }$, $\alpha \vdash _{\varLambda } \beta$ if and only if $|| \alpha || \subseteq || \beta ||$ in $M^{\varLambda }_3$.

Definition 8

We say that a set of consequence $L^{\lnot }$-pairs K characterizes a class of IIFs $\mathcal {C}$ if it holds for any IIF I that $I \in \mathcal {C}$ iff all $L^{\lnot }$-pairs from K are valid in I. A consequence $L^{\lnot }$-pair $\alpha \vdash \beta$ characterizes a class $\mathcal {C}$ if $\{ \alpha \vdash \beta \}$ characterizes $\mathcal {C}$.

Proposition 16

The following facts hold:

• (a) $p \vdash \lnot \lnot p$ characterizes the class of IIFs with symmetric incompatibility relation⁷,

• (b) $\lnot \lnot p \vdash p$ characterizes the class of IIFs satisfying the following property: for every filter F and every state $s \notin F$ there is a state t such that $s \notin \bot _t$ and $F \subseteq \bot ^t$.

• (c) $\{ p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$  characterizes the class of IIFs where $\bot$ is symmetric and where every filter is the intersection of a set of incompatibility filters, i.e., for every filter F there is a set of states $X \subseteq S$ such that $F = \bigcap _{s \in X} \bot _s$.

• (d) $\lnot p \wedge \lnot q \vdash \lnot (p \vee q)$ characterizes the class of IIFs satisfying the following property: for any states s, t, u, if $u \bot s$ and $v \bot s$ then $u \circ v \bot s$.

• (e) $\lnot (p \wedge q) \vdash \lnot p \vee \lnot q$ characterizes the class of IIFs satisfying the following property: for any state s and any filters F, G, if $F \cap G \subseteq \bot ^s$ then there are states t, u such that $F \subseteq \bot ^t$, $G \subseteq \bot ^u$ and $t \circ u \le s$.

• (f) $p\wedge \lnot p\vdash q$ characterizes the class of IIFs satisfying the following property: for any state s, if $s\bot s$ then $s=i$.

• (g) $p\vdash q\vee \lnot q$ characterizes the class of IIFs satisfying the following property: for any filter F and any state s, there are states t, u s.t. $t\in F$, $u \bot v$ for all $v \in F$, and $t\circ u\le s$.

Definition 9

Let $n \in \{1, 2, 3 \}$ and let K be a set of consequence $L^{\lnot }$-pairs that characterizes a class of IFFs $\mathcal {C}$. We say that K is canonical$_n$ if for every logic $\varLambda$ such that $K \subseteq \varLambda$, the frame $I^{\varLambda }_n$ is in the class $\mathcal {C}$. A consequence $L^{\lnot }$-pair $\alpha \vdash \beta$ is canonical$_n$ if $\{ \alpha \vdash \beta \}$ is canonical$_n$.

Note that canonicity gives us completeness results in the following sense: if a consequence $L^{\lnot }$-pair $\alpha \vdash \beta$ is canonical$_n$ for at least one $n \in \{1, 2, 3 \}$ then the lattice logic enriched with $\alpha \vdash \beta$ is complete with respect to the class of IIFs that $\alpha \vdash \beta$ characterizes. More generally, if $\{ \alpha _j\vdash \beta _j~|~j \in J \}$ is a set of consequence $L^{\lnot }$-pairs such that for each $j \in J$, $\alpha _j\vdash \beta _j$ is canonical$_n$ (for at least one $n \in \{1, 2, 3 \}$) and characterizes a class of IIFs $\mathcal {C}_j$ then the lattice logic enriched with $\{ \alpha _j\vdash \beta _j~|~j \in J \}$ is complete with respect to the class $\bigcap _{j \in J} \mathcal {C}_j$. Here are some examples of canonicity.

Proposition 17

Each of the consequence $L^{\lnot }$-pairs $p \vdash \lnot \lnot p$, $\lnot p \wedge \lnot q \vdash \lnot (p \vee q)$, $p\wedge \lnot p\vdash q$ is canonical$_1$ and canonical$_3$.

The previous proposition cannot be stated for canonicity$_2$. See for instance the proof of Proposition 18 in the appendix that shows that $I^{\varLambda }_2$ for a logic $\varLambda$ containing $p \vdash \lnot \lnot p$ does not have a symmetric incompatibility relation. As regards the cases with ‘non-first order conditions’, i.e. (b), (c), (e), and (g) of Proposition 16, we will focus only on the double negation law (c) and leave the remaining cases for future research. We also leave for future research whether it can be actually proved that these consequence $L^{\lnot }$-pairs cannot be characterized by first-order conditions (for a related result, see [12]). However, we will show that double negation is not canonical for each of our canonical model constructions. Especially the case of non-canonicity$_1$ is interesting.

Proposition 18

For each $n \in \{1, 2, 3 \}$, $\{p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$ is not canonical$_n$.

In the next section, we provide a comparison with Hartonas’ semantics. To facilitate the comparison we need another definition. This definition can be motivated by non-canonicity of double negation law, or by the fact that the algebra of propositions in an IIF, i.e. the algebra of possible values of formulas in the IIF, is always a complete lattice with an additional negation operation (to be more specific, it is always an algebraic lattice with a negation operation). To allow also for lattices that are not complete, we can restrict the space of possible valuations in the style of the so-called general frames known from modal logic (see [3, §1.4]). Given an IIF, let us define the following two operations on filters corresponding to the algebraic counterparts of disjunction and negation:

• $F \sqcup G = \{ s \in S~|~\text {there are }t \in F\text { and }u \in G\text { such that }t \circ u \le s \}$,

• $- F = \{ s \in S~|~\text {for all }t \in F\text {, }t \bot s \}$.

Definition 10

A general IIF (GIIF, for short) is a pair $J=\left\langle I, P \right\rangle$ where I is an IIF, and P is a set of filters in I closed under the operations $\cap , \sqcup , -$. A valuation V in J is a valuation in I that assigns to every atomic formula an element of P. A GIIF equipped with a valuation is called a general IIM (GIIM).

Note that every logic $\varLambda$ is sound and complete for instance with respect to the GIIF obtained from $I^{\varLambda }_3$ by restricting the space of valuations to principal filters, or with respect to the GIIFs obtained from $I^{\varLambda }_1$ or $I^{\varLambda }_2$ by restricting the valuations to principal filters that are generated by a theory that is in turn generated by a single formula.

Before moving on, let’s pause to note some points of difference between our semantics and the incompatibility semantics discussed by Dunn [7], and others. Restricted to language $L^{\lnot }$, the difference comes down to two sequents which are immediate consequences of Dunn’s approach, but which are not generally valid in our framework. These are distribution $\alpha \wedge (\beta \vee \gamma )\vdash (\alpha \wedge \beta )\vee \gamma$ and $\lnot \alpha \wedge \lnot \beta \vdash \lnot (\alpha \vee \beta )$. Both of these are consequences of working only with ‘prime’ states, for which the usual disjunction truth condition ($\vee$) obtains. By moving to our semantic setting, we can reject these sequents, and perhaps there are compelling philosophical reasons to want to do so. For instance, there are well-rehearsed reasons to reject distribution coming out of the literature on quantum logic (see [21] for a classic philosophical discussion), and logics without distribution have also been defended in connection with understanding logical consequence in terms of meaning containment (see [4]).

4 Comparison with Hartonas’ Approach

In this section we compare our semantics with the one presented in Hartonas’ [14], which is based on his duality theory for lattices developed in [13]. We first reconstruct Hartonas’ approach based on his neighborhood frames. Let $X \ne \emptyset$, and $\nu : X \rightarrow \mathcal {P}(X)$. The function $\nu$ determines the following two maps on $\mathcal {P}(X)$ defined as follows:

• $\lambda U = \{ x \in X~|~\text {for all }u \in U: x \in \nu (u) \}$,

• $\rho U = \{ x \in X~|~\text {for all }u \in U: u \in \nu (x) \}$.

These maps form a Galois connection and their composition determines a closure operator $\varGamma _{\nu } = \lambda \rho$. The sets satisfying $U=\varGamma _{\nu } (U)$ are called $\nu$-stable sets. Now we can introduce Hartonas neighborhood frames (models).

Definition 11

A Hartonas neighborhood frame (HNF) is any structure $N=\langle X, Y, \iota , \nu , \bot \rangle$, where X is a non-empty set, $Y \subseteq X$, $\iota \in X$, $\nu : X \rightarrow \mathcal {P}(X)$, and $\bot \subseteq X \times X$ such that the following conditions are satisfied:

• (a) $\nu (x) = \varGamma _{\nu } (\{x \})$, for any $x \in X$,

• (b) for any $\nu$-stable $U \subseteq X$ there is $x \in X$ such that $U=\nu (x)$,

• (c) the $\nu$-stable sets generated by the points of Y form a bounded sublattice of the complete lattice of $\nu$-stable sets where the top element is X and the bottom element is the singleton set $\{ \iota \}$; the elements of the sublattice are called regular subsets of X,

• (d) the neighborhood function imposes a partial order on the carrier set of a frame by letting $x \le _{\nu } y$ iff $\nu (y) \subseteq \nu (x)$,

• (e) if U is regular, then $\{ x \in X~|~\text {for all }u \in U: u \bot x \}$ is also regular.

A valuation in N is a function that assigns to each atomic formula from At a regular subsets of X. Given a valuation V in N, the pair $\left\langle N, V \right\rangle$ is called a Hartonas neighborhood model (HNM).

Proposition 19

In any HNF, the $\nu$-stable sets are exactly the principal upsets with respect to the ordering $\le _{\nu }$ and $\nu$ is a bijection between X and the lattice of $\nu$-stable sets such that $\nu (x)=\{ y \in X~|~x \le _{\nu } y \}$, for every $x \in X$. Moreover, $\nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y)))$ is the greatest lower bound of x and y, and $\iota$ the top element w.r.t. $\le _{\nu }$.

Relative to a given HNM, a relation of support $\Vdash$ between the elements of X and $L^{\lnot }$-formulas is defined in Hartonas’ semantics as follows:

• (a) $x \Vdash p$ iff $x \in V(p)$, for any atomic formula p,

• (b) $x \Vdash \alpha \wedge \beta$ iff $x \Vdash \alpha$ and $x \Vdash \beta$,

• (c) $x \Vdash \alpha \vee \beta$ iff $x \in \nu (y)$ for each y s.t. for any z if $z \Vdash \alpha$ or $z \Vdash \beta$ then $z \in \nu (y)$,

• (d) $x \Vdash \lnot \alpha$ iff for any y, if $y \Vdash \alpha$ then $y \bot x$.

Hartonas’ condition for disjunction, which is somewhat unintuitive and complicated, on first blush, is designed to lead to the following equivalence:

• $x \Vdash \alpha \vee \beta$ iff $x \in \varGamma _{\nu }(\{y \in X~|~y \Vdash \alpha \text { or } y \Vdash \beta \} )$.

The following proposition is a simple consequence of the definitions.

Proposition 20

Let M be a HNM. Then $\{ x \in X~|~x \Vdash \alpha \text { in }M \}$ is regular, for every $L^{\lnot }$-formula $\alpha$.

Definition 12

A HNF (HNM) is called normal (NHNF, NHNM) if it satisfies the following two conditions:

• (a) for every $x \in X$, the set $\{y \in X~|~x \bot y \}$ is $\nu$-stable,

• (b) for every $x,y,z \in X$, if $z \in \nu (x)$ and $x \bot u$ then $z \bot u$.

In the light of Proposition 19 we define $x \circ ^{\nu } y=\nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y)))$. Now we can formulate the claim that NHNFs and NHNMs can be viewed, respectively, as special cases of GIIFs and GIIMs.

Proposition 21

Let $N=\langle X, Y, \nu , \iota , \bot \rangle$ be a NHNF. Then the structure $I=\langle X, \circ ^{\nu }, \iota , \bot \rangle$ is an IIF and $N'=\langle I, \nu (Y) \rangle$ is a GIIF. The valuations in N in the sense of the Definition 11 are exactly the valuations in $N'$ in the sense of Definition 10. Moreover, for any such valuation V, any $x \in X$ and $\alpha \in L^{\lnot }$ it holds that $x \Vdash \alpha$ in $\langle N, V \rangle$ iff $x \vDash \alpha$ in $\langle N', V \rangle$.

We have shown that normal HNMs correspond exactly to particular cases of our GIIMs. One can observe that the restriction to normal HNMs is not a serious limitation. Hartonas’ completeness proof [14, Theorem 3.12] proceeds by the canonical model method. The canonical model that Hartonas uses for a logic $\varLambda$ is the structure $N^{\varLambda }=\langle X^{\varLambda }, Y^{\varLambda }, \iota ^{\varLambda }, \nu ^{\varLambda }, \bot ^{\varLambda } \rangle$ where $X^{\varLambda }$ is the set of all $\varLambda$-theories, $Y^{\varLambda }$ is the set of those $\varLambda$-theories that are generated by a single formula, $\iota ^{\varLambda }$ is the set of all formulas, $\varGamma \in \nu ^{\varLambda }(\varDelta )$ iff $\varDelta \subseteq \varGamma$, and $\bot ^{\varLambda }$ is defined in the same way as our $\bot _2$. In general the model $N^{\varLambda }$ corresponds structurally with our $M^{\varLambda }_2$. Note that for any $\varLambda$, $N^{\varLambda }$ is normal in the sense of Definition 12.

Hartonas also formulates an interesting modification of the framework presented above. In this modified semantics negation is captured in an operational way using an operation that we might call Hartonas star to contrast it with the so-called Routley star that is often used especially in relevant logics instead of the incompatibility relation (see [7]). As Hartonas points out, the Routley star is motivated by the fact that one can define a corresponding operation on prime theories in the canonical model. In order to work properly the Routley star requires ‘primeness’ and thus it is not suitable for the approaches based on theories rather than prime theories. To be more specific, there is no operation corresponding directly to Routley star that could be defined in canonical models based on all theories. Hartonas shows that his star operation is a feasible alternative for Routley star suitable for theory-based approaches. We have used this operation when we defined the incompatibility relation $\bot _2$ in the canonical model $M^{\varLambda }_2$.

The construction of the canonical model $M^{\varLambda }_2$ within our framework actually shows that the Hartonas star can be adapted to our setting. Let us finish this section with a brief discussion of how this can be done.

Definition 13

An information frame with a Hartonas star (IFHS) is a tuple $\left\langle S, \circ , i, * \right\rangle$, where $\left\langle S, \circ , i \right\rangle$ is an IF, and $*$ is an arbitrary unary operation on S. An information model with a Hartonas star (IMHS) is an IFHS equipped with a valuation.

Relative to a IMHS, the semantic clauses for conjunction and disjunction are as before and the semantic clause for negation is as follows:

• $s \vDash \lnot \alpha$ iff for any t, if $t \vDash \alpha$ then $t^* \le s$.

This clause is less intuitive than the clause using incompatibility relation. This is however similar to the case of Routley star which is also difficult to justify on the intuitive basis (though see [22] for an attempt). Nevertheless, this treatment of negation has some technical merits.

In Hartonas’ framework, the star operation is regulated by several constraints. In our framework no restrictions are needed and any operation is admissible which is supported by the following two propositions.

Proposition 22

For any IMHS M and any $\alpha \in L^{\lnot }$, $||\alpha ||_M$ is a filter in M.

Proposition 23

For any IMHS M and all $\alpha , \beta \in L^{\lnot }$, if $\alpha \vdash \beta$ is valid in M then $\lnot \beta \vdash \lnot \alpha$ is valid in M.

The previous proposition together with the fact that for any logic $\varLambda$ the canonical model $M^{\varLambda }_2$ can be viewed as an IMHS give us the following result.

Proposition 24

For any logic $\varLambda$ there is a class of IMHSs $\mathcal {C}$ such that $\varLambda$ coincides with all the consequence $L^{\lnot }$-pairs valid in $\mathcal {C}$. Moreover, the set of all consequence pairs that are valid in all IFHSs coincides with the minimal logic, i.e. the logic obtained by axioms and rules of the lattice logic plus the rule (N).

This comparison between our proposed semantics and Hartonas’ is illustrative in showcasing some nice properties of our approach. In addition to this, however, we think that the comparison also speaks in favour of our framework at an intuitive and conceptual level. In particular, we think the use of $\circ$ to interpret disjunction makes intuitive sense, and fits nicely into an approach to relational semantics which takes information states to be the basic entities. That we can obtain a similar kind of generality to Hartonas’ framework, employing neighbourhood semantic machinery, suggests that our approach retains some of the generality of his framework, while, perhaps, employing intuitively clearer structures.

A Appendix

Proof

(Proposition 5). First, assume that $\bot _t$ is a filter, for every $t \in S$. We show the inductive step for negation, that is, we will assume that $|| \alpha ||$ is a filter, and show that then $|| \lnot \alpha ||$ is a filter as well. It holds that $i \vDash \lnot \alpha$, since for any $t \in ||\alpha ||$, $i \in \bot _t$. Next, assume that $s \vDash \lnot \alpha$ and $s \le t$. Then if $u \vDash \alpha$ then $s \in \bot _u$, and thus $t \in \bot _u$. So, $t \vDash \lnot \alpha$. Assume that $s \vDash \lnot \alpha$ and $t \vDash \lnot \alpha$. Then for any $u \in || \alpha ||$, $s \in \bot _u$ and $t \in \bot _u$, and so $s \circ t \in \bot _u$. Thus $s \circ t \vDash \lnot \alpha$.

Second, assume that for some $t \in S$, $\bot _t$ is not a filter. We will show that there is a valuation V in I, and a formula $\alpha$ such that $|| \alpha ||$ is not a filter in $\left\langle I, V \right\rangle$. We consider three cases: (a) $i \notin \bot _t$; (b) there are $s, u \in S$ such that $s \le u$, $s \in \bot _t$, and $u \notin \bot _t$; (c) there are $s, u \in \bot _t$ such that $s \circ u \notin \bot _t$.

Consider a valuation V such that $V(p)=\{ v \in S~|~t \le v \}$. In the case (a), $t \vDash p$ but $i \notin \bot _t$. So, $i \notin || \lnot p ||$. In the case (b), if $v \vDash p$ then $t \le v$, and thus $s \in \bot _v$. So, $s \vDash \lnot p$. But $u \nvDash \lnot p$, for $t \vDash p$ and $u \notin \bot _t$. Hence, $|| \lnot p ||$ is not a filter. In the case (c) $s \vDash \lnot p$ and $u \vDash \lnot p$ but $s \circ u \nvDash \lnot p$. Hence, again, $|| \lnot p ||$ is not a filter.   $\square$

Proof

(Proposition 9). The proof is by induction on the complexity of $\alpha$, and the only case we will consider is that where $\alpha =\lnot \beta$. The right-to-left direction is immediate, so suppose that $\lnot \beta \notin \varDelta$. Fix $\varGamma =\{\gamma \mid \beta \vdash _{\varLambda }\gamma \}$, and note that $\varGamma \in S_1$ and $\varGamma \vDash \beta$. Suppose that $\varGamma \bot _1 \varDelta$ holds, so that for some $\gamma \in \varGamma$, $\lnot \gamma \in \varDelta$; in that case, $\beta \vdash \gamma$, and so $\lnot \gamma \vdash \lnot \beta$, and thus $\lnot \beta \in \varDelta$, contrary to the assumption. Thus $\varDelta \nvDash \lnot \beta$, as desired.    $\square$

Proof

(Proposition 13). Again the proof is by induction on the complexity of $\alpha$. The inductive step for negation amounts to Lemma 3.13 in [14]. Since our notation is quite different, let us reconstruct this step. For the left-to-right direction assume that $\varDelta \vDash \lnot \beta$. Then for any $\varGamma \in S_2$, if $\varGamma \vDash \beta$, i.e. $\beta \in \varGamma$, then $\varGamma ^* \subseteq \varDelta$. Let us fix $\varGamma =\{\gamma \mid \beta \vdash _{\varLambda }\gamma \}$. Then $\gamma \in \varGamma ^*$ iff for some $\delta$, $\delta \vdash _{\varLambda } \beta$ and $\lnot \delta \vdash _{\varLambda } \gamma$, which is equivalent to $\lnot \beta \vdash _{\varLambda } \gamma$. Hence, $\varGamma ^*= \{\gamma \mid \lnot \beta \vdash _{\varLambda }\gamma \}$ and thus $\lnot \beta \in \varDelta$. For the right-to-left direction assume that $\lnot \beta \in \varDelta$. Take any $\varGamma$  such that $\varGamma \vDash \beta$  and thus $\beta \in \varGamma$. Let $\gamma \in \varGamma ^*$. Then there is $\delta$ such that $\delta \vdash _{\varLambda }\beta$ and $\lnot \delta \vdash _{\varLambda } \gamma$. Hence, $\lnot \beta \vdash _{\varLambda } \gamma$ and $\gamma \in \varDelta$. We have shown that $\varGamma ^* \subseteq \varDelta$, i.e. $\varGamma \bot _2 \varDelta$. It follows that $\varDelta \vDash \lnot \beta$.    $\square$

Proof

(Proposition 15). The inductive step for negation can be proved as follows: $[\alpha ] \vDash \lnot \beta$ iff for all $\gamma$, if $[\gamma ] \vDash \beta$ then $[\gamma ] \bot _3 [\alpha ]$ iff for all $\gamma$, if $\gamma \vdash _{\varLambda } \beta$ then $\alpha \vdash _{\varLambda } \lnot \gamma$ iff $\alpha \vdash _{\varLambda } \lnot \beta$.    $\square$

Proof

(Proposition 16). (b) First, take any IIF I in which the condition is satisfied, i.e. for every filter F and every state $s \notin F$ there is a state t such that $s \notin \bot _t$ and $F \subseteq \bot ^t$. Assume $s \nvDash p$, i.e. $s \notin V(p)$. Thus, there is t such that $s \notin \bot _t$ and $V(p) \subseteq \bot ^t$. Then $t \vDash \lnot p$ (any state supporting p is incompatible with t) but since it is not the case that $t \bot s$ we obtain $s \nvDash \lnot \lnot p$. We have shown that $\lnot \lnot p \vdash p$ is valid in I. Second, take an IIF I in which the condition is not satisfied, i.e. there is a filter F and a state $s \notin F$ such that for every state t, if $F \subseteq \bot ^t$ then $s \in \bot _t$. Consider a valuation V such that $V(p)=F$. Then $s \nvDash p$. Moreover, if $t \vDash \lnot p$, then $V(p) \subseteq \bot ^t$, and, consequently $t \bot s$. It follows that $s \vDash \lnot \lnot p$. We have shown that $\lnot \lnot p \vdash p$ is not valid in I.

(c) First, note that if $\bot$ is symmetric, $\bot _t = \bot ^t$ for any state t. Hence, it follows from (a) and (b) that $\{ p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$ characterizes the class of IIFs where (i) the compatibility relation is symmetric and (ii) for any filter F and any state $s \notin F$ there is an incompatibility filter G such that $F \subseteq G$ and $s \notin G$. Now it suffices to show that (ii) is equivalent to the condition stating that every filter is the intersection of a set of incompatibility filters. Let $UpF=\{G~|~G\text { is an incompatibility filter such that }F \subseteq G \}$. It is obvious that $F \subseteq \bigcap UpF$. It holds that there is F that is not the intersection of any set of incompatibility filters iff there is F that is a proper subset of $\bigcap UpF$ iff there is F and $s \notin F$ such that $s \in \bigcap UpF$ iff (ii) does not hold.    $\square$

Proof

(Prop. 17). We will just consider the case of $\lnot p\wedge \lnot q\vdash \lnot (p\vee q)$ – the others are similar, and this is the axiom that distinguishes our basic setting from that employing a standard treatment of disjunction (and all ‘prime’ states). For canonicity$_1$, suppose that $\varGamma ,\varSigma ,\varDelta \in S_1$, $\varGamma \bot _1\varDelta$, and $\varSigma \bot _1\varDelta$. It follows that there are $\alpha \in \varGamma$ and $\beta \in \varSigma$ such that $\lnot \alpha ,\lnot \beta \in \varDelta$. Thus $\lnot \alpha \wedge \lnot \beta \in \varDelta$, and thus $\lnot (\alpha \vee \beta )\in \varDelta$. It is immediate that $\alpha \vee \beta \in \varGamma \circ _1\varSigma =\varGamma \cap \varSigma$, and thus $\varGamma \circ _1\varSigma \bot _1\varDelta$, as desired. For canonicity$_3$, we’ll work in the more complex setting, not assuming that there is an explosive formula. To that end, suppose that $s,t,u\in S_3$, $s\bot _3 u$, and $t\bot _3 u$. If any of s, t, u is $i_3$ then we’re done, as $i_3\bot _3 v$, $v\bot _3i_3$, and $v\circ _3i_3=i_3\circ _3v=i_3$ all hold for every v, so suppose that none is: i.e., that there are $\alpha ,\beta ,\gamma \in Prop_\varLambda$ such that $s=[\alpha ]$, $t=[\beta ]$, and $u=[\gamma ]$. By the supposition, then, $\gamma \vdash \lnot \alpha$ and $\gamma \vdash \lnot \beta$, and thus $\gamma \vdash \lnot \alpha \wedge \lnot \beta$. It follows that $\gamma \vdash \lnot (\alpha \vee \beta )$, and thus, since $s\circ _3t=[\alpha \vee \beta ]$, $s\circ _3\bot _3u$, as desired.    $\square$

Proof

(Proposition 18). First, we will show that $\{ p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$ is not canonical$_1$. Let $\varLambda$ be the distributive lattice logic enriched with (N) and both $\lnot \lnot p \vdash p$ and $p \vdash \lnot \lnot p$. We will show the following: There is a filter of non-empty $\varLambda$-theories F (i.e. a set of non-empty $\varLambda$-theories that is closed under intersection and stronger $\varLambda$-theories) and there is a non-empty $\varLambda$-theory $\varDelta \notin F$ such that $\varDelta \bot _1 \varOmega$ for all $\varOmega$ such that $\varGamma \bot _1 \varOmega$  for each $\varGamma \in F$. This will imply that F  cannot be expressed as an intersection of incompatibility filters. Let us construct F and $\varDelta$ satisfying the desired property. Take for each $i \in \mathbb {N}$ an infinite set of atomic formulas $X_i=\{p^i_1, p^i_2, \ldots \}$, assuming that if $i \ne j$  then $X_i$  and $X_j$ are disjoint. Let $\varGamma _i$ be the $\varLambda$-theory generated by $X_i$. Let F be the filter generated by the set of $\varLambda$-theories $\{\varGamma _1, \varGamma _2, \ldots \}$. Now we can construct $\varDelta$. Let Y be the set of all disjunctions of atomic formulas from $\bigcup _{i \in \mathbb {N}} X_i$ satisfying the following:

• $p^{i_1}_{j_1} \vee \ldots \vee p^{i_n}_{j_n} \in Y$ iff all $i_1, \ldots , i_n$ are distinct and it is not the case that there is k such that $j_1 = \ldots = j_n = k$ and $i_1, \ldots , i_n \le k$.

This definition can be illustrated with the following table. Y contains all disjunctions of atomic formulas from different columns except those that are connected by a path built from the horizontal lines.

Let $\varDelta$  be the $\varLambda$-theory generated by Y. Let $\varGamma \in F$. Then there are $\varGamma _{i_1}, \ldots , \varGamma _{i_n}$ such that $\varGamma _{i_1} \cap \ldots \cap \varGamma _{i_n} \subseteq \varGamma$. Take $k=max\{i_1, \ldots , i_n\}$. Then $p^1_k \vee \ldots \vee p^k_k \in \varGamma$ but $p^1_k \vee \ldots \vee p^k_k \notin \varDelta$, and thus $\varDelta \ne \varGamma$. We have shown that $\varDelta \notin F$.

Now assume $\varGamma \bot _1 \varOmega$ for each $\varGamma \in F$. Then $p^1_{j_1} \wedge \ldots \wedge p^1_{j_n} \vdash _{\varLambda } \alpha$ for some $p^1_{j_1}, \ldots , p^1_{j_n} \in X_1$ and some $\alpha$ such that $\lnot \alpha \in \varOmega$. Then $\lnot (p^1_{j_1} \wedge \ldots \wedge p^1_{j_n}) \in \varOmega$. Take $k=max\{j_1, \ldots , j_n \}+1$. There must be some $p^k_{i_1}, \ldots , p^k_{i_m} \in X_k$ such that $\lnot (p^k_{i_1} \wedge \ldots \wedge p^k_{i_m}) \in \varOmega$. Hence $\lnot ((p^1_{j_1} \wedge \ldots \wedge p^1_{j_n}) \vee (p^k_{i_1} \wedge \ldots \wedge p^k_{i_m})) \in \varOmega$. Moreover, k was selected in such a way that it also holds that $p^1_j \vee p^k_i \in \varDelta$, for each $j \in \{j_1, \ldots , j_n \}$  and $i \in \{i_1, \ldots , i_m \}$. Then $(p^1_{j_1} \wedge \ldots \wedge p^1_{j_n}) \vee (p^k_{i_1} \wedge \ldots \wedge p^k_{i_m}) \in \varDelta$, by distributivity, and thus $\varDelta \bot _1 \varOmega$  as desired.

Second, we will show that $\{ p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$ is not canonical$_2$. Let $\varLambda$ be the lattice logic enriched with (N) and both $\lnot \lnot p \vdash p$ and $p \vdash \lnot \lnot p$. We will show that $\bot _2$ is not symmetric. Let $\varGamma$ be the $\varLambda$-theory generated by $\{ p \}$ and $\varDelta$ the $\varLambda$-theory generated by an infinite set of atomic formulas $X=\{ q_1, q_2 \ldots \}$ assuming that $p \notin X$. Then $\varGamma ^*$ is the $\varLambda$-theory generated by $\{ \lnot p \}$ and $\varDelta ^*=\emptyset$ (for there is no $\beta$ such that $\beta \vdash _{\varLambda } \delta$  for each $\delta \in \varDelta$). Hence, $\varDelta \bot _2 \varGamma$  but not $\varGamma \bot _2 \varDelta$.

Finally, we will show that $\{ p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$ is not canonical$_3$. Let $\varLambda$ be again the lattice logic enriched with (N) and with $\lnot \lnot p \vdash p$ and $p \vdash \lnot \lnot p$. Let $X=\{q_1, q_2, q_3, \ldots \}$ be an infinite set of atomic formulas such that $p \notin X$. Let F be the filter in $I^{\varLambda }_3$ generated by $\{[q_1], [q_2], [q_3], \ldots \}$. Recall that $I^{\varLambda }_3$ is given by the Lindenbaum-Tarski algebra turned upside down and enriched with a new top element $i_3$. It holds that $[\alpha ] \in F$ iff there are $q_{i_1}, \ldots , q_{i_n}$ such that $\alpha \vdash _{\varLambda } q_{i_1} \vee \ldots \vee q_{i_n}$. It follows that $[p] \notin F$. In order to show that $\{ p \vdash \lnot \lnot p, \lnot \lnot p \vdash p \}$ is not canonical$_3$ it is sufficient to observe that for any $t \in S_3$, if $F \subseteq \bot ^{t}_3$ then $[p] \bot _3 t$. Note that there is no $\beta$ such that $\beta \vdash _{\varLambda } \lnot \alpha$ for all $\alpha \in F$. This follows for example from the fact that $\varLambda$ has the variable sharing property and so for any $\beta$ we can take any $q_i$ not occurring in $\beta$ and then $\beta \nvdash _{\varLambda } \lnot q_i$. It follows that $F \subseteq \bot ^{t}_3$ only if $t=i_3$. But it holds $[p] \bot i_3$ which finishes the proof.    $\square$

Proof

(Proposition 19). First, we show that $\nu (x)=\{ y \in X~|~x \le _{\nu } y \}$. By the definition of $\varGamma _{\nu }$ as $\lambda \rho$ it generally holds that if $y \in \varGamma _{\nu } (\{x \})$ then $\varGamma _{\nu }(\{y\}) \subseteq \varGamma _{\nu } (\{x \})$. By (a) and (d) of Definition 11 we obtain: if $y \in \nu (x)$ then $x \le _{\nu } y$, i.e. $\nu (x) \subseteq \{ y \in X~|~x \le _{\nu } y \}$. On the other side, if $x \le _{\nu } y$ then $\nu (y) \subseteq \nu (x)$, and since $y \in \nu (y)$ (because in general $y \in \lambda \rho (\{y\})$), it follows that $y \in \nu (x)$, and thus $\{ y \in X~|~x \le _{\nu } y \} \subseteq \nu (x)$. Since any $\nu$-stable set is of the form $\nu (x)$, for some $x \in X$, $\nu$-stable sets are exactly the principle upsets w.r.t. $\le _{\nu }$. Since $\le _{\nu }$ is a partial order, $\nu$ is a bijection between X and the lattice of $\nu$-stable sets.

By (c) of Definition 11 we obtain $\{ \iota \} \subseteq \nu (x)$, for every $x \in X$, which means (by (d)) that $\iota$ the top element w.r.t. $\le _{\nu }$. It remains to be shown that $\nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y)))$ is the greatest lower bound of x and y w.r.t. $\le _{\nu }$. It holds that $\nu (x) \subseteq \varGamma _{\nu } (\nu (x) \cup \nu (y))$ and thus $\nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y))) \le _{\nu } x$. By the same reasoning $\nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y))) \le _{\nu } y$, so $\nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y)))$ is a lower bound of $\{x , y \}$. Assume that $z \le _{\nu } x$ and $z \le _{\nu } y$. Then $\nu (x) \subseteq \nu (z)$ and $\nu (y) \subseteq \nu (z)$. So, $\nu (x) \cup \nu (y) \subseteq \nu (z)$ and since $\nu (z)$ is $\nu$-stable we obtain $\varGamma _{\nu } (\nu (x) \cup \nu (y)) \subseteq \nu (z)$. It follows that $z \le _{\nu } \nu ^{-1}(\varGamma _{\nu } (\nu (x) \cup \nu (y)))$ which is what we needed to show.    $\square$

Proof

(Proposition 21). Let $N=\langle X, Y, \nu , \iota , \bot \rangle$ be a NHNF. Proposition 19 shows that $\langle X, \circ ^{\nu }, \iota \rangle$ is an IF. Moreover, the conditions (a) and (b) from Definition 12 guarantee that $I=\langle X, \circ ^{\nu }, \iota , \bot \rangle$ is an IIF. Since $\nu (x)$ is always a (principal) filter, the valuations in N are always the valuations in I. Let V be a valuation in N (in the sense of Definition 11). We will show by induction that for any $\alpha \in L^{\lnot }$ it holds that $x \Vdash \alpha$ in $\langle N, V \rangle$ iff $x \vDash \alpha$ in $\langle I, V \rangle$. The case of atomic formulas and the inductive stapes for conjunction and negation are immediate. Let us show the inductive step for disjunction. Assume that the claim holds for some $L^{\lnot }$-formulas $\alpha , \beta$. It follows from Propositions 19 and 20 that there are states $z_{\alpha }, z_{\beta }$ such that $\nu (z_{\alpha }) = \{ x \in X~|~x \Vdash \alpha \}$ and $\nu (z_{\beta }) = \{ x \in X~|~x \Vdash \beta \}$. Now we can observe that the following claims are equivalent:

• $x \vDash \alpha \vee \beta$,

• there are $u, v \in X$ such that $u \vDash \alpha$, $v \vDash \beta$ and $u \circ ^{\nu } v \le _{\nu } x$,

• there are $u, v \in X$ such that $u \Vdash \alpha$, $v \Vdash \beta$ and $\nu ^{-1}(\varGamma _{\nu } (\nu (u) \cup \nu (v))) \le _{\nu } x$,

• there are $u, v \in X$ such that $u \Vdash \alpha$, $v \Vdash \beta$ and $\nu (x) \subseteq \varGamma _{\nu } (\nu (u) \cup \nu (v))$,

• $\nu (x) \subseteq \varGamma _{\nu } (\nu (z_{\alpha }) \cup \nu (z_{\beta }))$,

• $x \in \varGamma _{\nu } (\nu (z_{\alpha }) \cup \nu (z_{\beta }))$,

• $x \Vdash \alpha \vee \beta$.

It follows that $\nu (Y)$ is closed under the required operation and thus $N'=\langle I, \nu (Y) \rangle$ is a GIIF such that the valuations in N coincide with the valuations in $N'$, which finishes the proof.    $\square$