Towards a Fuzzy Context Logic

Abstract

A key step towards trustworthy, reliable and explainable, AI is bridging the gap between the quantitative domain of sensor-actuator systems and the qualitative domain of intelligent systems reasoning. Fuzzy logic is a well-known formalism suitable for aiming at this gap, featuring a quantitative mechanism that at the same time adheres to logical principles. Context logic is a two-layered logical language originally aimed at pervasive computing systems for reasoning about and within context, i.e., changing logical environments. Both logical languages are linguistically motivated. This chapter uncovers the close connection between the two logical languages presenting two new results. First, a proof is presented that context logic with a lattice semantics can be understood as an extension of fuzzy logic. Second, a fuzzification for context logic is proposed. The resulting language, which can be understood as a two-layered fuzzy logic or as a fuzzified context logic, expands both fields in a novel manner.

1. Introduction

Fuzzy logic has been employed successfully in intelligent systems, sensor-actuator systems, expert systems, and machine learning techniques for more than 50 years [1]. Being a tool for inference at both the logical and the sensor-actuator systems level its use for reliable and explainable autonomous systems has become a focus of recent research [2, 3, 4, 5]. One key building block for this has been a growing understanding of fuzzy logic semantics over the past 20 years [6] and the position this family of logics assumes within the field of logics in general. In particular, the connection to residuated lattices plays an important role for novel perspectives [7, 8]. One such new perspective is the connection to context logic, which is developed in this chapter.

Context logic was introduced in [9, 10, 11] as a logic for representing context-dependency and context phenomena in pervasive computing systems. Recent developments in context logic focus on a logical actuator control mechanism [12, 13, 14]. This chapter presents the logic with a fuzzy logic lattice semantics highlighting the close relation between the two formalisms and the close relation between context logic and the sensory and machine learning components of intelligent sensor actuator systems (ISAS), such as robotics and autonomous vehicles. We show that context logic can be understood as a fuzzy logic since it can be given an algebraic semantics like that of fuzzy logic as based upon lattice structures.

2. Fuzzy logic and context logic

We briefly review the basics of how fuzzy logic handles quantitative information and contrast this with the approach chosen in context logic. Here, it may appear we go into basic aspects at a greater depth than what may seem necessary. However, to bring the two logics together, establishing the common ground conceptually is a critical first step.

Fuzzy logic [15] was developed as a linguistically motivated logic that was to be more akin to how human beings reason with uncertain information and how experts analyze alternatives and act upon them [16]. Its main cognitive motivation was that human beings are able to relay, for instance, control information without the use of numerical values. In fact, human language outside scientific and technical contexts rarely employs quantities to express relations regarding a scale, amounts, or probabilities. We prefer to say, e.g., rarely rather than giving an estimate about a concrete percentage, or give a color term, such as yellow, instead of providing RGB values and we reason with such information. We “compute with words” [17]. One reason for this is the inherent uncertainty of perceptual or sensory information and the presence of intersubjective differences. Rules we receive or provide verbally benefit from this vagueness, as they have a wide applicability, allow a concise formulation, and allow for intersubjective differences: two people may disagree whether a certain fruit is yellow or rather a light orange, but they will agree that to at least some degree, something that has a light orange color is yellow. A rule given by an expert to a novice, such as “if a fruit is yellow, then it is ripe,” is easy to understand for a human being, and accordingly fuzzy expert systems, fuzzy sensor-actuator systems, and the output of some fuzzy learning systems, can be understood and verified by human beings better than purely numerical systems that operate with numerical equations.

In natural language, human beings convey information about continuous sensory domains, such as color or height, by use of adjectives. The phenomena of vagueness, uncertainty, and context-dependency are the main challenges for formalization from a linguistic point of view [18]. Adjectives can be used in several different ways. The main categories are:

Positive: Anne is tall (for her age).

Comparative: Anne is taller than Betty.

Equative: Ann is as tall as Betty.

Superlative: Ann is the tallest (girl on the team).

While the comparative and equative use are most easily mapped to a corresponding ordering and equivalence relation for the dimension in question (here: height), the positive and superlative can change their applicability depending on context. If we talk about children, 1.50 m (5 ft) may be tall. If we talk about the average European female adult, this is comparatively small. Likewise, the superlative changes with the context: Ann may be the smallest person in the room and still be called the tallest while the current topic is her team. Context logic is interesting from a cognitive science perspective as it enables the modeling of such influence of the context.

From a cognitive science point of view, fuzzy logic is an interesting formalism as it addresses issues of vagueness and uncertainty that appear especially in the semantics of adjectives. But it is also one of only few approaches bridging logical reasoning and machine learning [19].

Fuzzy logic goes beyond multi-valued logics [20] by proposing semantics for approximate reasoning. In particular, [15, p.424] proposes to “[view] the process of inference […] as the solution of a system of relational assignment equations.” This emphasizes the connection to both sensor-actuator systems and classical methods of system modeling and evaluation with recent advances reaching from explainable machine learning [5] to advanced uncertainty mechanisms for ontology design [21]. Combining the two languages promises to make the full expressiveness of natural language adjectives available for modeling, reasoning, and explanation in ISAS design.

3. Fuzzy logic as a logical language

While the linguistic background facilitates usability of fuzzy logic, it is easier to see logical connections with respect to a more restrictive and conventional logic syntax. We therefore use a simple propositional logical language as a classical background language in this chapter. We adopt the following syntax for the set of all formulae ${\mathcal{L}}_F$ based on a set of variables ${\mathcal{V}}_F$ and a set of predicate symbols ${\mathcal{P}}_F$.

$$\begin{array}{l}\text{For} \mathrm{P}\in {\mathcal{P}}_{\mathrm{F}} \text{and} \mathrm{x}\in {\mathcal{V}}_{\mathrm{F}},\mathrm{P}\left(\mathrm{x}\right) \text{is\hspace{0.17em}an} \left(\text{atomic}\right) \text{formula}.\\ \text{For} \mathrm{any} \text{formula} \varphi \in {\mathcal{L}}_{\mathrm{F}},\neg \varphi \text{is} \mathrm{a} \text{formula}.\\ \text{For} \mathrm{any} \text{formulae} \varphi ,\psi \in {\mathcal{L}}_{\mathrm{F}},\varphi \wedge \psi ,\varphi \vee \psi ,\text{and} \varphi \to \psi \mathrm{are} \text{formula}.\end{array}$$

Using this syntax, we can formalize a proposition similar to the above example as:

$$\text{Yellow}\left(\text{color}\right)\to \text{Ripe}\left(\text{ripeness}\right).$$

We can use the usual semantics for predicate logics to interpret this sentence based on a structure $\left(U,I,i_V,i_P\right)$. Here $U$ is the universe of discourse, which needs to contain in this example: the referents for the constants, i.e., concrete colors, e.g., as RGB values, and degrees of ripeness, e.g., as sets of tuples containing percentage of sugar and other substances indicative of degrees of ripeness. The term interpretation function $i_V:{\mathcal{V}}_F\to U$ maps the variable symbols ripeness and color to elements from $U$, distinct measurement values in a measurement value space. Predicate symbols are interpreted by the function $i_P:{\mathcal{V}}_P\to 2^U$ mapping out regions in $U$. The classical formula interpretation function $I:{\mathcal{L}}_F\to \left\{0,1\right\}$ maps formulae to values in $\left\{0,1\right\}$.

3.1 Interpretation of predicates based on fuzzy sets

A fundamental point where fuzzy logic differs from classical predicate logic is in the interpretation of the predicates and predication: classical logic considers $I\left(\text{Yellow}\left(\text{color}\right)\right)$ as true iff $i_V\left(\text{color}\right)\in i_P\left(\text{Yellow}\right)$, realizing predication by set membership ($\in$). Fuzzy logic, in contrast, interprets predicate symbols such as $\text{Yellow}$ with fuzzy sets ${\mu }_P:U\to \left[0,1\right]$, e.g., ${\mu }_{\text{Yellow}}:U\to \left[0,1\right]$, i.e., as functions into $\left[0,1\right]$. It then can replace the classical membership function $\in$ (of type $U\times 2^U\to \left\{0,1\right\}$), with a fuzzy set membership function $\mu :U\times \left(U\to \left[0,1\right]\right)\to \left[0,1\right]$ that simply applies the fuzzy set membership function: $\mu \left(u,{\mu }_{\mathrm{P}}\right)\mapsto {\mu }_{\mathrm{P}}\left(u\right)$. Being based on fuzzy sets ${\mu }_{\mathrm{P}}$, formulae ${\mathcal{L}}_F$ in fuzzy logic can then be interpreted with a fuzzy semantics using a suitable function $I:{\mathcal{L}}_F\to \left[0,1\right]$ for complex formulae.

3.2 Interpretation of connectives based on $t$-norms

To evaluate complex formulae, fuzzy logic requires extended semantics for the propositional connectives that can handle arbitrary values in $\left[0,1\right]$, while remaining true to the classical interpretation in the cases $\left\{0,1\right\}$. A general strategy in fuzzy logic is to allow different semantics to take the place of the classical semantics for propositional connectives ($\neg ,\wedge ,\vee ,\to$), in particular, as t-norms (functions $t:\left[0,1\right]\times \left[0,1\right]\to \left[0,1\right]$) with corresponding t-conorms (functions $s:\left[0,1\right]\times \left[0,1\right]\to \left[0,1\right]$), and their residuals ($r:\left[0,1\right]\times \left[0,1\right]\to \left[0,1\right]$), respectively [6]. These functions are described and discussed in more detail below. A t-norm based semantics interprets the logical language we defined above in the following way:

$$\begin{array}{ll}\text{For} \mathrm{Q}\in {\mathcal{P}}_{\mathrm{F}} \text{and} \mathrm{x}\in {\mathcal{V}}_{\mathrm{F}}:I\left(Q\left(x\right)\right)=\mu \left(i_V\left(x\right),i_P\left(Q\right)\right)& ={\mu }_Q\left(i_V\left(x\right)\right)\\ \text{For} \mathrm{any} \text{formula} \varphi \in {\mathcal{L}}_{\mathrm{F}}:I\left(\neg \varphi \right)& =1-I\left(\varphi \right)\\ \text{For} \mathrm{any} \text{formulae} \varphi ,\psi \in {\mathcal{L}}_{\mathrm{F}}:I\left(\varphi \wedge \psi \right)& =t\left(I\left(\varphi \right),I\left(\psi \right)\right)\\ I\left(\varphi \vee \psi \right)& =s\left(I\left(\varphi \right),I\left(\psi \right)\right)\\ I\left(\varphi \to \psi \right)& =r\left(I\left(\varphi \right),I\left(\psi \right)\right)\end{array}$$

3.3 Properties of $t$-norms

If the semantics for ∧ are based on a t-norm, this guarantees that important semantic properties of the classical conjunction are retained. A t-norm ${\left[0,1\right]}^2\to \left[0,1\right]$ is a commutative (1), associative (2), and monotone function (3), with a neutral element $1$ (4).

$$t\left(x,y\right)=t\left(y,x\right)$$E1

$$t\left(t\left(x,y\right),z\right)=t\left(x,t\left(y,z\right)\right)$$E2

$$\text{If} x⪯y \text{then} t\left(x,z\right)⪯t\left(y,z\right)$$E3

$$t\left(1,x\right)=x$$E4

Examples are the minimum t-norm (5), used in Gödel logics, and the product t-norm (6), used in probability theory:

$$t_{\min }\left(a,b\right)=min\left(a,b\right)$$E5

$$t_{\text{prod}}\left(a,b\right)=a\ast b$$E6

The corresponding t-conorms, denoted by the symbol $s$ and accordingly also called s-norms, can be obtained by applying De Morgan’s laws assuming the semantics of negation of a value $t$ to be $1-t$. Their neutral element is $0$.

$$s\left(a,b\right)=1-t\left(1-a,1-b\right)$$E7

The corresponding s-norms for the above example t-norms are then $s_{\min }$, the minimum s-norm (8), and the product s-norm $s_{\text{prod}}$ (9):

$$s_{\min }\left(a,b\right)=max\left(a,b\right)$$E8

$$s_{\text{prod}}\left(a,b\right)=a+b-a\ast b$$E9

There are several ways to interpret the implication and different approaches are suitable for different purposes (cf. [22], for a detailed overlook and comparison). As with other operators, fuzzy implication should be conservative for values in $\left\{0,1\right\}$. A widely used notion is the left-residual [23]:

$$r\left(a,b\right)=sup\left\{z\in \left[0,1\right]|t\left(a,z\right)\le b\right\}$$E10

The relation between the residual and the t-norm/s-norm are covered by two additional axioms, continuity (11) and pre-linearity (12):

$$t\left(x,y\right)⪯z \mathrm{iff} x⪯r\left(y,z\right)$$E11

$$s\left(r\left(x,y\right),r\left(y,s\right)\right)=1$$E12

For the above two t-norms $t_{\min },t_{\text{prod}}$ the following are corresponding residuals:

$$r_{\min }\left(a,b\right)=\left\{\begin{array}{l}1 \mathrm{iff} a\le b\\ b \text{otherwise}.\end{array}\right.$$E13

$$r_{\text{prod}}\left(a,b\right)=\left\{\begin{array}{l}1 \mathrm{iff} a\le b\\ b/a \text{otherwise}.\end{array}\right.$$E14

3.4 Generalized $t$-norms: the set-theoretic lattice

The most widely used examples of functions ${\mu }_P$ map elements of $U$ to values in $\left[0,1\right]$, with, e.g., the minimum or product t-norm. However, fuzzy logic can be given a generalized t-norm semantics based on residuated lattices, i.e., other lattice structures $\left(L,⪯\right)$ instead of $\left(\left[0,1\right],\le \right)$. A particularly interesting residuated lattice for the purposes of comparison with context logic is $L=\left(2^B,\subseteq \right)$, where $B$ is a given base set and $U=B$. Given this structure, we can define interpretation functions $i_V:{\mathcal{V}}_F\to B$ for variable symbols as before. But we can now interpret predicates not with classical $\left[0,1\right]$-fuzzy sets but with generalized $L$-fuzzy sets ${\mu }_P:B\to 2^B$, so that $I:{\mathcal{L}}_F\to 2^B$ for formulae:

$$I\left(P\left(x\right)\right)={\mu }_P\left(i_V\left(x\right)\right),\text{with} {\mu }_P:U\to 2^B$$E15

$$I\left(\neg \varphi \right)=2^B-I\left(\varphi \right)$$E16

$$I\left(\varphi \wedge \psi \right)=I\left(\varphi \right)\cap I\left(\psi \right)$$E17

$$I\left(\varphi \vee \psi \right)=I\left(\varphi \right)\cup I\left(\psi \right)$$E18

$$I\left(\varphi \to \psi \right)=I\left(\psi \right)\cup \left(2^B-I\left(\varphi \right)\right)$$E19

The intuition behind this is to map elements $x\in U$ to, e.g., sets of points, i.e., spatial regions or temporal or sensory values intervals. Instead of saying $x$ is $P$ to a degree of 0.5, for instance, we could thus distinguish $x$ as in a specific area of space, time, or sensor value space. E.g., we can assign a function ${\mu }_{\text{Yellow}}$ to map measured RGB colors $x$ to sets that form a filter around the color #FFFF00. Measuring an orange $x$ and a lime $y$ we could determine they are yellow to the same degree as ${\mu }_{\text{Yellow}}\left(x\right)$ and ${\mu }_{\text{Yellow}}\left(y\right)$ yielding the same large region around the core value #FFFF00. We could say $x$ is as yellow as $y$ is yellow, since with $I\left(\text{Yellow}\left(x\right)\right)=I\left(\text{Yellow}\left(y\right)\right)$ holds $I\left(\text{Yellow}\left(x\right)\leftrightarrow \text{Yellow}\left(y\right)\right)=2^B$. This would be the same result as with classical fuzzy sets, but we would be able to additionally avoid comparing incompatible contexts, e.g.: while a red apple $z$ may be as aubergine as an orange is yellow with classical fuzzy sets, the set theoretic interpretation yields $I\left(\text{Yellow}\left(x\right)\leftrightarrow \text{Aubergine}\left(z\right)\right)\subseteq I\left(\text{Yellow}\left(x\right)\leftrightarrow \text{Yellow}\left(y\right)\right)$, as the regions for $I\left(\text{Yellow}\left(x\right)\right)$ and $I\left(\text{Aubergine}\left(z\right)\right)$ overlap but are distinct. In contrast to the strictly ordered $\left[0,1\right]$, the partially ordered $2^B$ thus allows higher expressiveness.

Partial orders and corresponding lattice structures are at the heart of the semantics for context logic, and the two languages can on this basis be combined in a natural manner.

4. An overview of context logic

We now specify the context logic language and describe a semantics similarly in terms of a predicate logical language, which in turn can be related to lattice structures and thus fuzzy logical semantics.

4.1 Contextualization in context logic

Context logic has only one type of basic entity, context variables, and a single partial order relation $⊑$ (part of or sub-context): the city of London, for instance, is a sub-context of England, and March 2017 is a sub-context of the year 2017:

$$\text{London}⊑\text{England}$$

$$\text{March}2017⊑\text{Year}2017$$

The language provides three term operators $\sqcap$ (intersection), $\bigsqcup$ (sum), and $\sim$ (complement).

Since any pre-order can be expressed as a sub-relation of a partial order relation, and be extended to a partial order relation over its equivalence classes, the single sub-context relation together with the $\sqcap$ operators allows the specification of arbitrarily many different partial order relations [24]. More accurately we may, for instance, want to say that the city of London is a spatial sub-context or a sub-region of England, and that March 2017 is a temporal sub-context or a sub-interval of the year 2017.

$$\text{London}\sqcap \text{Space}⊑\text{England}$$

$$\text{March}2017\sqcap \text{Time}⊑\text{Year}2017$$

This and the following examples feature one simple spatial sub-context and one temporal sub-context relation. We can in the same manner however express, for instance, directional relations [25], temporal ordering relations (bi-directionally branching), and class hierarchies [9]. Ordering relations between thematic values, such as expressed by the comparative use of adjectives (Section 2) can also be added in the same way. The main purpose of the language is to facilitate expressing the common partial order core of all these theories, including the tractable fragments of these theories in a unified syntax.

A syntactic shorthand reflects – linguistically speaking – a topicalized adverbial position:

$$c:\left[a⊑b\right]\stackrel{\mathit{def}}{\iff }c\sqcap a⊑b$$

$$\text{Space}:\left[\text{London}⊑\text{England}\right]$$

$$\text{Time}:\left[\text{March}2017⊑\text{Year}2017\right]$$

Spatially, London is a sub-context of England. Temporally, March 2017 is a sub-context of the year 2017. For entities such as cities or months, this may seem redundant. But contexts, such as a birthday party, which have both temporal and spatial extent can thus be located temporally within one context and spatially within another:

$$\text{Space}:\left[\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}⊑\text{London}\right]$$

$$\text{Time}:\left[\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}⊑\text{March}2017\right]$$

We can also reflect that speakers may choose to topicalize the other way around [26], as the last two sentences are logically equivalent to the following:

$$\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}:\left[\text{Space}⊑\text{London}\right]$$

$$\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}:\left[\text{Time}⊑\text{March}2017\right]$$

or, leveraging the propositional second layer,

$$\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}:\left(\left[\text{Space}⊑\text{London}\right]\wedge \left[\text{Time}⊑\text{March}2017\right]\right)$$

where, for any propositional junctor $\circ \in \left\{\wedge ,\vee ,\to \right\}$:

$$c:\left({\varphi }_1\circ {\varphi }_2\right)\stackrel{\mathit{def}}{\iff }c:{\varphi }_1\circ c:{\varphi }_2\text{and}c:\neg \varphi \stackrel{\mathit{def}}{\iff }\neg c:\varphi$$

Regarding John’s birthday party: the location is in London, the time is in March 2017. Moreover, we can allow contexts to be stacked or combined, in order to express more complex contextualization:

$$\text{MarySays}:\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}:\left[\text{Time}⊑\text{March}2017\right]$$

$$\text{TomSays}:\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}:\left[\text{Time}⊑\text{August}2017\right]$$

Similarly to how we would express conflicting opinions in natural language, we can equivalently state:

$$\mathrm{Joh}{\mathrm{n}}^{\prime }\text{sBirthday}\sqcap \text{Time}:\left(\left[\text{MarySays}⊑\text{March}2017\right]\wedge \left[\text{TomSays}⊑\text{August}2017\right]\right)$$

$$d:c:\left[a⊑b\right]\equiv d:\left[c\sqcap a⊑b\right]\equiv d\sqcap c\sqcap a⊑b$$

Regarding John’s birthday party and the time, Mary says in March 2017 and Tom says in August 2017. Context logic thus allows to reflect colloquial contextualizations well, but also to represent conflicting information.

4.2 Context logic as a logical language

Context logic thus employs two syntactic layers: the term layer with the term operators $\sqcap ,\bigsqcup ,\sim$ and the propositional layer with the logic connectives ($\wedge ,\vee ,\neg ,\to$). Context terms ${\mathcal{T}}_C$ are defined over a set of variables ${\mathcal{V}}_C$:¹

$$\begin{array}{l}\mathrm{Any} \text{context\hspace{0.17em}variable} v\in {\mathcal{V}}_C \text{and\hspace{0.17em}the\hspace{0.17em}special\hspace{0.17em}symbols} \top \text{and} \perp \\ \mathrm{are} \text{atomic\hspace{0.17em}context\hspace{0.17em}terms}.\end{array}$$

$$\text{If} c \text{is} \mathrm{a} \text{context\hspace{0.17em}term},\text{then}\sim c \text{is} \mathrm{a} \text{context\hspace{0.17em}term}.$$

$$\text{If} c \text{and} d \mathrm{are} \text{context\hspace{0.17em}terms\hspace{0.17em}then} c\sqcap d \text{and} c\bigsqcup d \mathrm{are} \text{context\hspace{0.17em}terms}.$$

Context formulae ${\mathcal{L}}_C$ are defined as follows:

$$\text{If} c \text{and} d \mathrm{are} \text{context\hspace{0.17em}terms\hspace{0.17em}then} c⊑d \text{is\hspace{0.17em}an\hspace{0.17em}atomic\hspace{0.17em}context\hspace{0.17em}formula}.$$

$$\text{If} \varphi \text{is} \mathrm{a} \text{context\hspace{0.17em}formula},\text{then}\neg \varphi \text{is} \mathrm{a} \text{context\hspace{0.17em}formula}.$$

$$\begin{array}{l}\text{If} \varphi \text{and} \psi \mathrm{are} \text{context\hspace{0.17em}formulae\hspace{0.17em}then} \varphi \wedge \psi ,\varphi \vee \psi \text{and} \varphi \to \psi \mathrm{are}\\ \text{context\hspace{0.17em}formulae}.\end{array}$$

We further define:

$$c=d\stackrel{\mathit{def}}{\iff }\left[c⊑d\right]\wedge \left[d⊑c\right]$$E20

$$c⊏d\stackrel{\mathit{def}}{\iff }\left[c⊑d\right]\wedge \neg \left[d⊑c\right]$$E21

Different variant semantics have been proposed [10, 11, 26]. The different approaches slightly differ in the resulting semantics, but all three employ a lattice structure for specifying the meanings of context terms, assigning a partial order to give a semantics to $⊑$. Here, we give a semantics by mapping the language to a predicate logic with a single binary predicate $P$, describing a pre-order relation, to give the fundamental $⊑$ its semantics. We use a function ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}:{\mathcal{L}}_C\times {\mathcal{V}}_P\to {\mathcal{L}}_P$, where ${\mathcal{L}}_C$ is the set of context logic formulae, ${\mathcal{V}}_P$ is a vocabulary of predicate logic variables, and ${\mathcal{L}}_P$ is the set of predicate logic formulae. We also employ ${\mathcal{V}}_C$, the set of variables, as the set of constants for ${\mathcal{L}}_P$, and require ${\mathcal{V}}_P\cap {\mathcal{V}}_C=\varnothing$:

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑\top ,m\right)=\top$$E22

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑\perp ,m\right)=\perp$$E23

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑v,m\right)=P\left(m,v\right),\text{for} v\in {\mathcal{V}}_C$$E24

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑\sim c,m\right)={\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(c⊑\perp ,m\right) \text{for} c\in {\mathcal{T}}_C$$E25

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c\sqcap d,m\right)={\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m\right)\wedge {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑d,m\right)$$E26

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c\bigsqcup d,m\right)=\\ \forall m^{\prime },P\left(m^{\prime },m\right):\exists m″,P\left(m^{\prime },m\right):{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m″\right)\vee {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑d,m″\right)\\ \text{where} m^{\prime } \text{and} m″ \mathrm{are} \mathrm{new} \text{variables}.\end{array}$$E27

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(c⊑d,m\right)=\forall m^{\prime },P\left(m^{\prime },m\right):{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m^{\prime }\right)\to {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑d,m^{\prime }\right)\\ \text{where} m^{\prime } \text{is} \mathrm{a} \mathrm{new} \text{variable}.\end{array}$$E28

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\neg \varphi ,m\right)=\neg {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)$$E29

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi \wedge \psi ,m\right)={\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)\wedge {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\psi ,m\right)$$E30

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi \vee \psi ,m\right)={\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)\vee {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\psi ,m\right)$$E31

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi \to \psi ,m\right)={\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)\to {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\psi ,m\right)$$E32

We note that although we introduce new variables $m^{\prime },m″$ in (27) and (28), each new variable is only used together with the variable last introduced – $m^{\prime }$ with $m$, $m″$ with $m^{\prime }$ but not with $m$ –, not with any other variables introduced before. This means, we can alternate between two variables and reuse $m$ after $m^{\prime }$, i.e., that ${\mathcal{V}}_P=\left\{m,m^{\prime }\right\}$. We also note, that the context variables $v\in {\mathcal{V}}_C$ are constants with respect to the predicate logic and that they only appear in the second position of $P$ in (24). This property allows us to reformulate any binary expression $P\left(m,v\right)$ for $v\in {\mathcal{V}}_C$ using a different monadic predicate $P_v$ for each $v\in {\mathcal{V}}_C$, and write $P_v\left(m\right)$ instead of $P\left(m,v\right)$.

Consequently, the fragment of predicate logic required in application of ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}$ alone is in the two-variable fragment known to be decidable. Moreover, the variables, such as $m$ and $m^{\prime }$, only occur together in the atomic guard, as $P\left(m^{\prime },m\right)$, suggesting that the language as defined so far is in the so-called guarded fragment GF [27] defined as [cited after 28, p.1664f]:

$$\text{Every\hspace{0.17em}atomic\hspace{0.17em}formula\hspace{0.17em}belongs\hspace{0.17em}to} \mathrm{GF}.$$

$$\mathrm{GF} \text{is\hspace{0.17em}closed\hspace{0.17em}under}\neg ,\wedge ,\vee ,\to ,\leftrightarrow .$$

If x, y are tuples of variables, α(x, y) is an atomic formula, ψ(x,y) is in GF, and free (ψ ⊆ free (α) = {x,y}, where free (ϕ) is the set of the free variables of ϕ, then the formulae

$$\begin{array}{l}\exists y:\alpha \left(x,y\right)\wedge \psi \left(x,y\right)\\ \forall y:\alpha \left(x,y\right)\to \psi \left(x,y\right)\end{array}$$

$$\text{belong\hspace{0.17em}to} \mathrm{GF}.$$

In order to obtain the reasoning capabilities, however, we would need to add pre-order axioms for $P$, so as to be able to specify $⊑$ as a partial order relation:

$$\forall x,y,z:P\left(x,y\right)\wedge P\left(y,z\right)\to P\left(x,z\right)$$E33

$$\forall x:P\left(x,x\right)$$E34

and we see that transitivity (13) cannot be axiomatized in the two-variable fragment, as it requires three variables. Fortunately, [28, 29] have shown that for GF² + PG – the guarded fragment limited to two variables and a single binary pre-order that can only appear in the guard – is in 2-EXPTIME. Moreover, this result is a loose upper bound, since the language under inspection here can be expressed using the transitive binary relation $P$ in only one direction – namely from wholes to parts –, using otherwise only the monadic predicates $P_v,v\in {\mathcal{V}}_C$, placing the translation of context logic with the axioms for $⊑$ into the class ${\mathrm{MGF}}^2+\overleftarrow{\mathit{TG}}$, the two-variable monadic guarded fragment with one-way transitive guards, which is decidable and whose satisfiability problem is in EXPSPACE [28].

In addition to the pre-order axioms, we can also add a localized guarded variant of the so-called weak supplementation principle [30, Ch. 3] for $⊑$ ensuring a minimal homogeneity constraint over $v_1,v_2\in {\mathcal{V}}_C$:²

$$\begin{array}{l}\forall x:\left(\forall x^{\prime },P\left(x^{\prime },x\right):P\left(x^{\prime },v_1\right)\to P\left(x^{\prime },v_2\right)\right)\\ \wedge \left(\exists x^{\prime },P\left(x^{\prime },x\right):P\left(x^{\prime },v_2\right)\wedge \neg P\left(x^{\prime },v_1\right)\right)\\ \to \left(\exists x^{\prime },P\left(x^{\prime },x\right):P\left(x^{\prime },v_2\right)\wedge \neg \exists {x^{\prime }}^{\prime },P\left({x^{\prime }}^{\prime },x^{\prime }\right):P\left({x^{\prime }}^{\prime },v_1\right)\right).\end{array}$$E35

The principle says that, if for any $x$ all its parts $x^{\prime }$ that are in $v_1$ are also in $v_2$, but there is a part $x^{\prime }$ that is in $v_2$ but not in $v_1$ (paraphrasing: $v_1$ is a proper part of $v_2$), then there is a part $x^{\prime }$ of $v_2$ that has no parts in $v_1$ (i.e.: $x^{\prime }$ does not overlap $v_1$), i.e., is completely outside of $v_1$. Axiom 35 ensures that the entities described by $v_1,v_2\in {\mathcal{V}}_C$ do not have, e.g., singular points that are not entities themselves in the domain under inspection. This axiom is required for proving several of the lattice laws. Note that we thus characterize a weak supplementation principle only for $⊑$, that we, however, cannot formulate a weak supplementation principle for $P$ without leaving the guarded fragment.

In order to do this, however, we have to employ $v_1,v_2\in {\mathcal{V}}_C$ as schema variables, i.e., we have to formally see this actually not as one axiom but $\mid {\mathcal{V}}_C^2\mid$ axioms. This means that for infinite ${\mathcal{V}}_C$, the axiomatization becomes infinite. For practical, finite knowledge bases, ${\mathcal{V}}_C$ will be finite. If an infinite vocabulary ${\mathcal{V}}_C$ is employed, a practical realization would be to use a unification mechanism suitable for the particular language ${\mathcal{V}}_C$ employed.

Intuitively, the meaning of $a⊑b$ is that all parts of $a$ are part of $b$. The reading thus corresponds to a universal quantification, and the properties expressed by contexts in this statement describe homogenous properties inherited from wholes to their parts. Correspondingly, $\neg \left[a⊑b\right]$ expresses an existential quantification, stating that not all parts of $a$ are parts of $b$, which means that there is a part of $a$ that is not part of $b$, or that does not have property $b$. We can thus express heterogeneity.

The complement $\sim c$, is interpreted with respect to the pseudo-$0$-element $\perp$: the atomic formula $\top ⊑\sim a$ is interpreted as equivalent to $a⊑\perp$, meaning that no part is in $a$, implying universal quantification. There are thus two types of negation $\neg$ on the logical level and $\sim$ on the context level. $\perp$ is a pseudo-element, it disappears in the translation when applying (28). We do not need to assume that an empty element exists:

$$\begin{array}{ll}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(c⊑\perp ,m\right)& \equiv \forall m^{\prime },P\left(m^{\prime },m\right):{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m^{\prime }\right)\to {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑\perp ,m^{\prime }\right)\\ & \equiv \forall m^{\prime },P\left(m^{\prime },m\right):{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m^{\prime }\right)\to \perp \\ & \equiv \forall m^{\prime },P\left(m^{\prime },m\right):\neg {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m^{\prime }\right)\\ & \equiv \neg \exists m^{\prime },P\left(m^{\prime },m\right):{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m^{\prime }\right)\end{array}$$E36

A crucial consequence of adopting weak supplementation (35) is (2). It says that if all parts $m″$ of a part $m^{\prime }$ have a part $m‴$ that is part of $a$, this is equivalent to $m^{\prime }$ being part of $a$:

$$\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\equiv P\left(m^{\prime },a\right)$$E37

Proof (⫤): this holds immediately with the reflexivity (34) and transitivity (33) of $P$: if $P\left(m^{\prime },a\right)$ then all parts $m″$ of $m^{\prime }$ fulfill $P\left(m″,a\right)$ by transitivity, and therefore there is a part $m‴$ of $m″$, namely $m″$ itself, by reflexivity, so that $P\left(m‴,a\right)$.

Proof ($\models$): we prove the reverse direction by contradiction, applying (35). Assume $\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)$ and not $P\left(m^{\prime },a\right)$, i.e., that there is an $m_1^{″}$ that has $m‴,P\left(m‴,a\right)$ but not $P\left(m_1^{″},a\right)$. Then by (35) there has to be a part $m_2^{″}$ of $m^{\prime }$ that does not have a part $m‴$ where $P\left(m‴,a\right)$. But this is prevented by the premise $\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)$.

It can be shown (Section 4.4) that the definition of ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}$ together with the two pre-order axioms and the local guarded variant of the weak supplementation principle is sufficient to characterize context terms as spanning a bounded lattice. We note that with a different axiomatization other types of lattice structures could be realized for different application domains.

4.3 A fuzzy logic perspective on context logic

This section shows context logic as specified above is a two-layered language with a generalized $t$-norm-based fuzzy logic at the term level and a classical $\left\{0,1\right\}$-based semantics at the formula level. From there it is a small step to also add a $\left[0,1\right]$-based multivalued semantics to the formula level, so as to obtain a full two-layered fuzzy logic in Section 5.

To see that the context terms ${\mathcal{T}}_C$ can be viewed as a generalized t-norm, we set the intersection $\sqcap$, the meet operation of the lattice, as the monoid operation and the term $\top$ as the identity element of the monoid. The monoid properties associativity and identity element are fulfilled by any lattice (see Section 4.4, (44) and (46)). For the generalized fuzzy logic semantics, the lattice meet-operation $\sqcap$ will be shown to fulfill the properties of a $t$-norm, the join-operation $\bigsqcup$, those of the corresponding $s$-norm. Both are required to be commutative (1), associative (2), and support an identity element (4) and monotonicity (3) (for the full proofs see Section 4.4). We prove monotonicity for $\sqcap$ (38) and $\bigsqcup$ (39):

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\left[a⊑c\right]\wedge \left[b⊑d\right]\to \left[a\sqcap b⊑c\sqcap d\right],m\right)\equiv \\ \left(\forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\to P\left(m^{\prime },c\right)\right)\\ \wedge \left(\forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },b\right)\to P\left(m^{\prime },d\right)\right)\\ \to \left(\forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\wedge P\left(m^{\prime },b\right)\to P\left(m^{\prime },c\right)\wedge P\left(m^{\prime },d\right)\right)\end{array}$$E38

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\left[a⊑c\right]\wedge \left[b⊑d\right]\to \left[a\bigsqcup b⊑c\bigsqcup d\right],m\right)\equiv \\ \left(\forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\to P\left(m^{\prime },c\right)\right)\\ \wedge \left(\forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },b\right)\to P\left(m^{\prime },d\right)\right)\\ \to \forall m^{\prime },P\left(m^{\prime },m\right):\\ \left(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee P\left(m‴,b\right)\right)\\ \to \left(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,c\right)\vee P\left(m‴,d\right)\right)\end{array}$$E39

Proof (3): if every $m^{\prime }$ that is part of $a$ is in $c$ and every $m^{\prime }$ that is part of $b$ is in $d$, then every $m^{\prime }$ that is part of $a$ and $b$ is also in both $c$ and $d$. Proof (4): we see that it follows from this condition also that any $m‴$ that exists as part of any $m″$ in $a$ or $b$ must also be part of $c$ or $d$ in $m″$.

The generalized De Morgan law connects t-norms with s-norms (7). It follows for the translations of $\sqcap$ and $\bigsqcup$ directly from the De Morgan laws in predicate logic.

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\bigsqcup b=\sim \left(\sim a\sqcap \sim b\right),m\right)\equiv \\ \forall m^{\prime },P\left(m^{\prime },m\right):(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ P\left(m‴,a\right)\vee P\left(m‴,b\right))\\ \leftrightarrow \neg \exists m″,P\left(m″,m^{\prime }\right):\left(\neg \exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\\ \wedge \left(\neg \exists m‴,P\left(m‴,m″\right):P\left(m‴,b\right)\right)\end{array}$$E40

The residual can then be derived from its characterization:

$$r\left(a,b\right)=sup\left\{z|t\left(a,z\right)\preccurlyeq b\right\}.$$

The operation $\Rightarrow$ with the definition

$$a\Rightarrow b\stackrel{\mathit{def}}{\iff }\sim a\bigsqcup b$$E41

has the required property $t\left(a,z\right)\preccurlyeq b$ (with $\sqcap$ the $t$-norm and $⊑$, the lattice partial order $\preccurlyeq$).³

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\sqcap \left(\sim a\bigsqcup b\right)⊑b,m\right)\equiv \\ \forall m^{\prime },P\left(m^{\prime },m\right):(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ \left(\neg \exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},a\right)\right)\\ \vee P\left(m‴,b\right))\wedge P\left(m^{\prime },a\right)\to P\left(m^{\prime },b\right)\end{array}$$E42

We prove that for any $m^{\prime },P\left(m^{\prime },m\right):$

$$\begin{array}{l}\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ \left(\neg \exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},a\right)\vee P\left(m‴,b\right)\right)\wedge P\left(m^{\prime },a\right)\\ \models P\left(m^{\prime },b\right)\end{array}$$

and the term $\sim a\bigsqcup b$ expresses the maximal element local to $m$ with this property.

Proof: assume the antecedent is true, then because of transitivity of $P$ (33) and the conjunct $P\left(m^{\prime },a\right)$, there can be no $m‴$ part of $m^{\prime }$ for which all parts $m^{\mathit{iv}}$, including $m‴$ itself fulfill $\neg P\left(m^{\mathit{iv}},a\right)$. Therefore the second disjunct $P\left(m‴,b\right)$ must be true. But if we know that for all $m″$ with $P\left(m″,m^{\prime }\right)$ exists $m‴$, so that $P\left(m‴,b\right)$, we know by (2), a consequence of the localized guarded variant of the weak supplementation principle (35), that $P\left(m^{\prime },b\right)$. To see that it is maximal, assume there is $m_1^{\prime }$ outside of $\sim a\bigsqcup b$ and $P\left(m_1^{\prime },a\right)$ and $P\left(m_1^{\prime },b\right)$. To be outside of $\sim a\bigsqcup b$, there would have to be an $m″,P\left(m″,m_1^{\prime }\right)$ so that for all $m‴,P\left(m‴,m″\right)$ there is $m^{\mathit{iv}}$, so that $P\left(m^{\mathit{iv}},m‴\right)$ and $P\left(m^{\mathit{iv}},a\right)$ and $\neg P\left(m‴,b\right)$, but this cannot be, because $P\left(m‴,m_1^{\prime }\right)$ and by the assumption $P\left(m_1^{\prime },b\right)$, thus by transitivity (33) $P\left(m‴,b\right)$.

This result indicates that, at least with respect to the supplementation property expressed through (35), $\sim a\bigsqcup b$ fulfills the characterization of a residual. We can also show continuity (54) and pre-linearity (55) (Section 4.4).

We are thus justified to say that context logic terms have a generalized $t$-norm semantics and we can give a $t$-norm-based semantics to context logic.

We obtain: a t-norm-based classical semantics for context logic is a structure $\left(I,i,a,L_T,\preccurlyeq ,1_T,t,s\right)$, where the terms are interpreted by $i:{\mathcal{T}}_C\to L_T$ together with the function $a:{\mathcal{V}}_C\to L_T$ assigning context terms and variables, respectively, to elements of a lattice $L_T$, and the formulae, by the classical interpretation function $I:{\mathcal{L}}_C\to \left\{0,1\right\}$:

$$i\left(v\right)=a\left(v\right),\text{for} v\in V_C$$

$$i\left(\sim c\right)=1_T-i\left(c\right),$$

With $1_T-i\left(c\right)$the pseudo-complement of the lattice

$$i\left(c\sqcap d\right)=t\left(i\left(c\right),i\left(d\right)\right)$$

$$i\left(c\bigsqcup d\right)=s\left(i\left(c\right),i\left(d\right)\right)$$

$$I\left(c⊑d\right)=1 \mathrm{iff} i\left(c\right)\preccurlyeq i\left(d\right)$$

$$I\left(\neg \varphi \right)=1-I\left(\varphi \right)$$

$$I\left(\varphi \wedge \psi \right)=min\left(I\left(\varphi \right),I\left(\psi \right)\right)$$

$$I\left(\varphi \vee \psi \right)=max\left(I\left(\varphi \right),I\left(\psi \right)\right)$$

It only remains to show that the context term operators indeed support the lattice requirements.

4.4 Proof: context logic with local, guarded weak supplementation characterizes a bounded lattice

For the purpose of completeness, the proofs are listed here in detail. However, the results are part of basic, fundamental lattice theory and no novelty is claimed.

We prove that $\sqcap$ and $\bigsqcup$ fulfill the laws for a bounded lattice. We start by showing that $\sqcap$ fulfills the laws of a semilattice: $\sqcap$ is idempotent (7), associative (8), commutative (9), and has $\top$ as its neutral element (46).

$$a\sqcap a=a$$E43

$$a\sqcap \left(b\sqcap c\right)=\left(a\sqcap b\right)\sqcap c$$E44

$$a\sqcap b=b\sqcap a$$E45

$$a\sqcap \top =a$$E46

These properties hold, since $\sqcap$ directly translates into $\wedge$:

$${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c\sqcap d,m\right)={\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑c,m\right)\wedge {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑d,m\right)$$

We show the translations:

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\sqcap a=a,m\right)\equiv \forall P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\wedge P\left(m^{\prime },a\right)\leftrightarrow P\left(m^{\prime },a\right)\\ {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\sqcap \left(b\sqcap c\right)=\left(a\sqcap b\right)\sqcap c,m\right)\equiv \forall P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\wedge \left(P\left(m^{\prime },b\right)\wedge P\left(m^{\prime },c\right)\right)\\ \leftrightarrow \left(P\left(m^{\prime },a\right)\wedge P\left(m^{\prime },b\right)\right)\wedge P\left(m^{\prime },c\right)\\ {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\sqcap b=b\sqcap a,m\right)\equiv \forall P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\wedge P\left(m^{\prime },b\right)\\ \leftrightarrow P\left(m^{\prime },b\right)\wedge P\left(m^{\prime },a\right)\\ {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\sqcap \top =a,m\right)\equiv \forall P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\wedge \top \leftrightarrow P\left(m^{\prime },a\right)\end{array}$$

We can see that all translations of properties are tautologies and follow directly from the properties of $\wedge$. The semantics of $\bigsqcup$ requires a closer look. We first note that a basic requirement of extensionality holds:

$$\begin{array}{ll}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑a,m\right)& \equiv P\left(m,a\right)\equiv \forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },a\right)\\ & \equiv \forall P\left(m^{\prime },m\right):{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑a,m^{\prime }\right)\end{array}$$E47

The property (47) holds because $P\left(m,a\right)$ entails $P\left(m^{\prime },a\right)$ for all $P\left(m^{\prime },m\right)$ because of transitivity of $P$. Also, for all $m^{\prime },P\left(m^{\prime },m\right)$: $P\left(m^{\prime },a\right)$ entails $P\left(m,a\right)$, since $P$ is reflexive.

We can now prove the semilattice laws for $\bigsqcup$.

$$a\bigsqcup a=a$$E48

$$a\bigsqcup \left(b\bigsqcup c\right)=\left(a\bigsqcup b\right)\bigsqcup c$$E49

$$a\bigsqcup b=b\bigsqcup a$$E50

$$a\bigsqcup \perp =a$$E51

When we translate idempotency (48):

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\bigsqcup a=a,m\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ P\left(m‴,a\right)\vee P\left(m‴,a\right))\leftrightarrow P\left(m^{\prime },a\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ P\left(m‴,a\right))\leftrightarrow P\left(m^{\prime },a\right)\end{array}$$

we see that the translation of $\bigsqcup$ provides one direction of the proof. With (2), a consequence of weak supplementation, we obtain the other direction.

The other laws follow in a similar manner. We show associativity (49):

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\bigsqcup \left(b\bigsqcup c\right)=\left(a\bigsqcup b\right)\bigsqcup c,m\right)\equiv \forall m^{\prime },P\left(m^{\prime },m\right):\\ \forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee \forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,b\right)\vee P\left(m^v,c\right)\\ \leftrightarrow \forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):(\forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right)\\ \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,a\right)\vee P\left(m^v,b\right)\vee P\left(m‴,c\right)\end{array}$$

By proving the following for any $m^{\prime }$ from which the above then follows directly via the associativity and commutativity of $\vee$:

$$\begin{array}{l}\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee \forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,b\right)\vee P\left(m^v,c\right)\\ \equiv \forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee P\left(m‴,b\right)\vee P\left(m‴,c\right)\end{array}$$

We prove in two steps.

Proof ($\models$): assume we choose an arbitrary $m″,P\left(m″,m^{\prime }\right)$. The antecedent says that if there is an $m‴,P\left(m‴,m″\right)$ so that $P\left(m‴,a\right)$ or there is $P\left(m‴,m″\right)$ so that for all its parts $m^{\mathit{iv}}$, we can find $m^v$, so that $P\left(m^v,b\right)$ or $P\left(m^v,c\right)$. If there is an $m‴,P\left(m‴,a\right)$, the consequent holds. If there is no such $m‴,P\left(m‴,a\right)$, there must be an $m‴$, so that all its parts $m^{\mathit{iv}}$ have a part $m^v$ in $b$ or $c$. Since each such $m^v$ is also a part of $m″$, we can conclude that for all $m″,P\left(m″,m^{\prime }\right)$ there is an $m‴$ – namely, the $m^v$ we identified –, so that $P\left(m‴,b\right)\vee P\left(m‴,c\right)$.

Proof (⫤): assume we have for each $m″,P\left(m″,m^{\prime }\right)$: $\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee P\left(m‴,b\right)\vee P\left(m‴,c\right)$ and the consequent is false. In this case, there must be an $m_1^{″}$, so that $P\left(m‴,a\right)$ must be false for all $m‴,P\left(m‴,m_1^{″}\right)$ and that there is a part of any such $m‴$ so that all its subparts are neither in $b$ nor in $c$. By the premise however, we know that $m_1^{″}$ must have a part ${m″}_1^{\prime }$ so that $P\left({m″}_1^{\prime },b\right)\vee P\left({m″}_1^{\prime },c\right)$. But since $P$ is transitive we know that for all parts $m_1^{\mathit{iv}}$ of ${m″}_1^{\prime }$ holds either $P\left(m_1^{\mathit{iv}},b\right)$ or $P\left(m_1^{\mathit{iv}},c\right)$. By reflexivity we moreover know that each $m_1^{\mathit{iv}}$ has a part, namely itself, for which $P\left(m_1^{\mathit{iv}},b\right)$ or $P\left(m_1^{\mathit{iv}},c\right)$ hold.

Applying this result twice via the associativity and commutativity of $\vee$, we can conclude (49) must hold:

$$\begin{array}{l}\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee \forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,b\right)\vee P\left(m^v,c\right)\\ \equiv \forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee P\left(m‴,b\right)\vee P\left(m‴,c\right)\\ \equiv \forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):(\forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right)\\ \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P(m^{v}a\vee P\left(m^{v}b\right)\vee P\left(m‴,c\right)\end{array}$$

Theorem 14 holds immediately given the definition of the translation for $\bigsqcup$ and the commutativity of $\vee$:

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\bigsqcup b=b\bigsqcup a\right)\equiv \\ (\forall m^{\prime },P\left(m^{\prime },m\right):\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ P\left(m‴,a\right)\vee P\left(m‴,b\right))\\ \leftrightarrow (\forall m^{\prime },P\left(m^{\prime },m\right):\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ P\left(m‴,b\right)\vee P\left(m‴,a\right))\end{array}$$

Proving the neutral element property (51) requires (35).

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\bigsqcup \perp =a,m\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑a,m‴\right)\vee {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑\perp ,m‴\right))\\ \leftrightarrow {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\top ⊑a,m^{\prime }\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):\left(\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\vee \perp \right)\\ \leftrightarrow P\left(m^{\prime },a\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):\left(\forall m‴,P\left(m″,m\right):\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\\ \leftrightarrow P\left(m^{\prime },a\right)\end{array}$$

The proof follows immediately by (2).

In summary, we needed (35) for proving idempotency (48) and the neutral element (51). Associativity (49) and commutativity (50) were proven without using (35).

We have thus shown that $\sqcap$ and $\bigsqcup$ each create a semilattice structure over the $x\in {\mathcal{V}}_C$. When we prove the absorption laws, we see that the absorption law (52) can be proven without requiring (35), while the proof for the absorption law (53) uses it:

$$a\sqcap \left(a\bigsqcup b\right)=a$$E52

$$a\bigsqcup \left(a\sqcap b\right)=a$$E53

For (52):

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\sqcap \left(a\bigsqcup b\right)=a,m\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):(P\left(m^{\prime },a\right)\wedge \forall m″,P\left(m″,m^{\prime }\right):\\ \left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\vee \left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,b\right)\right))\\ \leftrightarrow P\left(m^{\prime },a\right)\end{array}$$

we show that for any $m^{\prime }$:

$$\begin{array}{l}P\left(m^{\prime },a\right)\wedge \forall m″,P\left(m″,m^{\prime }\right):\left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\\ \vee \left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,b\right)\right)\\ \equiv P\left(m^{\prime },a\right)\end{array}$$

Proof (⫤): this holds because of transitivity (33) and reflexivity (34) of $P$. If $P\left(m^{\prime },a\right)$, is true, we know $\forall m″,P\left(m″,m^{\prime }\right):\left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)$ is also true and thus also the disjunct. Therefore, the whole consequent must be true.

Proof ($\models$): here we already know $P\left(m^{\prime },a\right)$ in the antecedent, so the consequent cannot be false.

We prove (53):

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(a\bigsqcup \left(a\sqcap b\right)=a,m\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },m\right):(\forall m″,P\left(m″,m^{\prime }\right):\left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\\ \vee \left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\wedge P\left(m‴,b\right)\right))\\ \leftrightarrow P\left(m^{\prime },a\right)\end{array}$$

by showing for any $m^{\prime }$:

$$\begin{array}{l}\forall m″,P\left(m″,m^{\prime }\right):\left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\\ \vee \left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\wedge P\left(m‴,b\right)\right)\equiv P\left(m^{\prime },a\right)\end{array}$$

Proof ($\models$): $\forall m″,P\left(m″,m^{\prime }\right):\left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)\vee \left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\wedge P\left(m‴,b\right)\right)$ is true iff $\forall m″,P\left(m″,m^{\prime }\right):\left(\exists m‴,P\left(m‴,m″\right):P\left(m‴,a\right)\right)$ is true, and this entails $P\left(m^{\prime },a\right)$ by (2). Proof (⫤): this holds by transitivity and reflexivity.

The relation between the residual and the t-norm were covered by two additional axioms above: continuity (11) and pre-linearity (12):

$$x\sqcap y⊑z \mathrm{iff} x⊑\left(y\Rightarrow z\right)$$E54

$$\left(x\Rightarrow y\right)\bigsqcup \left(y\Rightarrow x\right)=\top$$E55

We prove continuity (54) by translation using ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}$.

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(x\sqcap y⊑z,m\right)\equiv {\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(x⊑\left(y\Rightarrow z\right),m\right) \text{translates\hspace{0.17em}into}:\\ \forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },x\right)\wedge P\left(m^{\prime },y\right)\to P\left(m^{\prime },z\right)\\ \equiv \forall m^{\prime },P\left(m^{\prime },x\right)\to \forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\\ \left(\neg \exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},y\right)\right)\vee P\left(m‴,z\right)\end{array}$$

Proof ($\models$): assume the antecedent holds, and $P\left(m^{\prime },x\right)$ for some $m^{\prime }$. Then, for $\forall m″,P\left(m‴,m″\right):\dots P\left(m‴,z\right)$ to be false, there must be an $m_1^{″},P\left(m_1^{″},m^{\prime }\right)$, so that $\forall m‴,P\left(m‴,m_1^{″}\right):\left(\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},y\right)\right)$ and $\forall m‴,P\left(m‴,m_1^{″}\right):\neg P\left(m‴,z\right)$. However, if $\forall m‴,P\left(m‴,m_1^{″}\right):\left(\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},y\right)\right)$ holds then by (2), $P\left(m_1^{″},y\right)$ and by transitivity also $P\left(m_1^{″},x\right)$ and by the assumption thus $P\left(m_1^{″},z\right)$, which cannot hold since all parts $m‴$ of $m_1^{″}$ including by reflexivity $m_1^{″}$ itself fulfill $\neg P\left(m‴,z\right)$.

Proof (⫤): assume the antecedent $\forall m^{\prime },P\left(m^{\prime },x\right):\dots P\left(m‴,z\right)$ holds. For $\forall m^{\prime },P\left(m^{\prime },m\right):P\left(m^{\prime },x\right)\wedge P\left(m^{\prime },y\right)\to P\left(m^{\prime },z\right)$ to be false, there must be $m_1^{\prime },P\left(m_1^{\prime },m\right)$, so that $P\left(m_1^{\prime },x\right)$ and $P\left(m_1^{\prime },y\right)$ must hold, but $P\left(m_1^{\prime },z\right)$ must be false. But then we also know that $\exists m‴,P\left(m‴,m″\right):\left(\neg \exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},y\right)\right)$ cannot hold for any $m″,P\left(m″,m_1^{\prime }\right)$. Thus, $\exists m‴,P\left(m‴,m″\right):P\left(m‴,z\right)$ must hold for all $m″$, and thus by (2) $P\left(m_1^{\prime },z\right)$.

We prove pre-linearity (55):

$$\begin{array}{l}{\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\left(x\Rightarrow y\right)\bigsqcup \left(y\Rightarrow x\right)=\top ,m\right)\equiv \\ \forall m^{\prime },P\left(m^{\prime },m\right):[\exists m″,P\left(m″,m^{\prime }\right):\forall m‴,P\left(m‴,m″\right):\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \left(\neg \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,x\right)\right)\vee P\left(m^{\mathit{iv}},y\right)]\\ \vee [\exists m″,P\left(m″,m^{\prime }\right):\forall m‴,P\left(m‴,m″\right):\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \left(\neg \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,y\right)\right)\vee P\left(m^{\mathit{iv}},x\right)]\end{array}$$

by showing for any$m^{\prime },P\left(m^{\prime },m\right):$

$$\begin{array}{l}\neg [\exists m″,P\left(m″,m^{\prime }\right):\forall m‴,P\left(m‴,m″\right):\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \left(\neg \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,x\right)\right)\vee P\left(m^{\mathit{iv}},y\right)]\\ \models [\exists m″,P\left(m″,m^{\prime }\right):\forall m‴,P\left(m‴,m″\right):\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\\ \left(\neg \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,y\right)\right)\vee P\left(m^{\mathit{iv}},x\right)]\end{array}$$

Proof: we obtain for the antecedent:

$$\begin{array}{l}\forall m″,P\left(m″,m^{\prime }\right):\exists m‴,P\left(m‴,m″\right):\forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\left(\exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,x\right)\right)\wedge \\ \neg P\left(m^{\mathit{iv}},y\right)\end{array}$$

Since this holds for all $m″,P\left(m″,m^{\prime }\right)$ it also holds for $m^{\prime }$ itself, i.e., it follows that:

$$\exists m‴,P\left(m‴,m^{\prime }\right):\forall m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\left(\exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,x\right)\right)\wedge \neg P\left(m^{\mathit{iv}},y\right)$$

We rename the variables to better show the structure:

$$\begin{array}{l}\exists m″,P\left(m″,m^{\prime }\right):\forall m‴,P\left(m‴,m″\right):\neg P\left(m‴,y\right)\wedge \left(\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},x\right)\right)\\ \equiv \exists m″,P\left(m″,m^{\prime }\right):\left(\forall m‴,P\left(m‴,m″\right):\neg P\left(m‴,y\right)\right)\wedge \\ \left(\forall m‴,P\left(m‴,m″\right):\left(\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):P\left(m^{\mathit{iv}},x\right)\right)\right)\end{array}$$

and by (2):

$$\equiv \exists m″,P\left(m″,m^{\prime }\right):\left(\neg \exists m‴,P\left(m‴,m″\right):P\left(m‴,y\right)\right)\wedge P\left(m″,x\right).$$

We now know that $m^{\prime }$ has a part $m″$ that is in $x$ and none of its parts is in $y$. With $P\left(m″,x\right)$, however we also know by transitivity of $P$ that all parts $m‴,P\left(m‴,m″\right)$ fulfill $P\left(m‴,x\right)$, and thus by reflexivity of $P$ that there is an $m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right)$, namely $m^{\mathit{iv}}=m‴$, for each $m‴$, which fulfills $P\left(m^{\mathit{iv}},x\right)$. Moreover, since all parts $m^v,P\left(m^v,m^{\mathit{iv}}\right)$ are by transitivity also parts of $m″$, we know that $\neg \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^{\mathit{iv}},y\right)$ and thus:

$$\begin{array}{l}\exists m″,P\left(m″,m^{\prime }\right):\forall m‴,P\left(m‴,m″\right):\exists m^{\mathit{iv}},P\left(m^{\mathit{iv}},m‴\right):\left(\neg \exists m^v,P\left(m^v,m^{\mathit{iv}}\right):P\left(m^v,y\right)\right)\wedge \\ P\left(m^{\mathit{iv}},x\right),\end{array}$$

which entails the consequent.

4.5 A note on mereological and ontological status

The mereologically interested reader may notice that adding even the weakened variant of the weak supplementation principle is sufficient to collapse context logic term structures to a single level by (2). The reason for this is that the weak supplementation principle considerably strengthens the expressiveness of negation, which given the principle always ensures the existence of a fully negative individual. This is the case, although our system mereologically speaking is an MM system, i.e., supports M1-M4 [30] only, with M4 acting as an axiom schema.

We may note also, that we need not ensure product (M5) or sum (M6) to exists, nor do we need or posit a universal $\top$ or null object $\perp$ to exist. The symbols $\top ,\perp ,\sqcap ,\bigsqcup ,-$ are, so to speak, “syntactic sugar” only. The assumed mereology thus is slightly weaker than MM and ontologically careful and minimalistic. For a deeper discussion, cf. [30, 31].

4.6 Example: set-theoretical model

To make the discussion more concrete, we briefly sketch a set-theoretical interpretation. An example of a suitable model is the set-theoretic lattice, assuming the set of all subsets of a base universe as the universe for the interpretation of the translation ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)$ of a context formula $\varphi$, and mapping $t$ to $\cap$ (17), $s$ to $\cup$ (18), and the residual $r$ according to (19). Note that, within this interpretation, the variables $m,m^{\prime },$etc., as well as the constants $a,b,c$, etc. of the translation ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)$ range over sets, not elements, of the base universe. With a set-theoretical model $\left(I,i,a,U,\subseteq ,B,\cap ,\cup \right)$, where $U\subseteq 2^B$ for $B$, the base set, we get:

$$i\left(v\right)=a\left(v\right) \text{for} v\in {\mathcal{V}}_C$$

$$i\left(\sim c\right)=1_T-i\left(c\right)=B-i\left(c\right)$$

$$i\left(c\sqcap d\right)=t\left(i\left(c\right),i\left(d\right)\right)=i\left(c\right)\cap i\left(d\right)$$

$$i\left(c\bigsqcup d\right)=s\left(i\left(c\right),i\left(d\right)\right)=i\left(c\right)\cup i\left(d\right)$$

$$I\left(c⊑d\right)=1 \mathrm{iff} i\left(c\right)\subseteq i\left(d\right)$$

$$I\left(\neg \varphi \right)=1-I\left(\varphi \right)$$

$$I\left(\varphi \wedge \psi \right)=min\left(I\left(\varphi \right),I\left(\psi \right)\right)$$

$$I\left(\varphi \vee \psi \right)=max\left(I\left(\varphi \right),I\left(\psi \right)\right)$$

We can show that, if the canonical interpretation $\left(I,i,a,U,\subseteq ,B,\cap ,\cup \right)$ is a model for formula $\varphi$, then there is a corresponding predicate logic model for ${\tau }_{\mathrm{CL}}^{\mathrm{PL}}\left(\varphi ,m\right)$ with interpretations for $m,m^{\prime }$ from $U\subseteq 2^B-\left\{\varnothing \right\}$, interpreting $P$ as $\subseteq$ and individuals $v\in V_C$ using an assignment function $a:{\mathcal{V}}_C\to 2^B$. While we allow the constants $v\in V_C$ to be empty, the variables used to describe their extension cannot.

The pre-order axioms for $P$ obviously hold for $\subseteq$. Also, the weak supplementation principle holds for $\subseteq$:

$$\begin{array}{l}\forall x:\left(\forall x^{\prime }\subseteq x:x^{\prime }\subseteq a\to x^{\prime }\subseteq b\right)\\ \wedge \left(\exists x^{\prime }\subseteq x:x^{\prime }\subseteq b\wedge \neg x^{\prime }\subseteq a\right)\\ \to \left(\exists x^{\prime }\subseteq x:x^{\prime }\subseteq b\wedge \neg \exists {x^{\prime }}^{\prime }\subseteq x^{\prime }:{x^{\prime }}^{\prime }\subseteq a\right).\end{array}$$

Proof: assume a set $x^{\prime }\subseteq x$ supports that $x^{\prime }\subseteq a$ implies $x^{\prime }\subseteq b$, and there is a set $x_1^{\prime }\subseteq x$ supporting $x_1^{\prime }\subseteq b$ but not $x_1^{\prime }\subseteq a$. We can then construct $x_2^{\prime }\subseteq x$ as $x_2^{\prime }=x_1^{\prime }-a$, which supports that $x_2^{\prime }\subseteq b$ and none of its subsets $x_2^{″}\subseteq x_2^{\prime }$ supports $x_2^{″}\subseteq a$.

We prove that $\cap ,\cup ,-$ over non-empty sets $m,m^{\prime },m″$ fulfill the characteristic properties for translations for $\sqcap ,\bigsqcup ,\sim$, respectively:

$$m\subseteq a\cap b\equiv m\subseteq a\wedge m\subseteq b$$E56

$$m\subseteq a\cup b\equiv \forall m^{\prime }\subseteq m:\exists m″\subseteq m^{\prime }:m″\subseteq a\vee m″\subseteq b$$E57

$$m\subseteq \sim a\equiv \forall m^{\prime }\subseteq m:\neg \exists m″\subseteq m^{\prime }:m″\subseteq a$$E58

The case of (20) is immediately clear. For (21), we look at the definition of $\cup$ in terms of elements $P\in B$, which we call points:

$$\begin{array}{l}m\subseteq a\cup b\equiv \forall P\in m:P\in a\vee P\in b\\ \equiv \forall m^{\prime }\subseteq m:\exists P\in m^{\prime }:P\in a\vee P\in b\\ \equiv \forall m^{\prime }\subseteq m:\exists m″\subseteq m^{\prime }:m″\subseteq a\vee m″\subseteq b\end{array}$$

Proof ($\models$): if the points in $m$ are in $a$ or in $b$ in the first step, then, since the $m^{\prime }$ are non-empty, it follows that each $m^{\prime }\subseteq m$ has a point either in $a$ or in $b$. In the second step, if there is a point $P$ in each $m^{\prime }$, that is in $a$ or in $b$, then there is a set $m″\subseteq m^{\prime }$, namely the singleton containing $P$, for which $m″\subseteq a$ or $m″\subseteq b$ must hold.

Proof (⫤): assume that for every $m^{\prime }$, there is a non-empty $m″\subseteq m^{\prime }$, with $m″\subseteq a$ or $m″\subseteq b$, then, since $m″$ non-empty, it must have a point $P\in a$ or $P\in b$. Since this holds for all non-empty sets $m^{\prime }$, including all singleton sets, which have only one element, it must hold for all points $P\in m$.

For (22), we similarly look at the definition of $-$ in terms of elements of $m$, i.e., points:

$$\begin{array}{l}m\subseteq \sim a\equiv \forall P\in m:\neg P\in a\\ \equiv \forall m^{\prime }\subseteq m:\neg \exists P\in m^{\prime }:P\in a\\ \equiv \forall m^{\prime }\subseteq m:\neg \exists m″\subseteq m^{\prime }:m^{\prime }\subseteq a\end{array}$$

Proof ($\models$): the property carries over to all parts $m^{\prime }$ of $m$ in the second step. The third step follows, because any set $m″\subseteq m^{\prime }$ must be non-empty, and if it contains a point, $m″\subseteq a$ cannot be true, since no point in $m^{\prime }$ is in $a$ and $\subseteq$ is transitive.

Proof (⫤): as in the proof for $\bigsqcup$, we can argue over singleton sets. If for all sets $m^{\prime }$, no subset $m″$ is subset of $a$, then this also holds for the singletons, and thus no set $m^{\prime }$ has a point $P$ in $a$, but this again holds also for singleton sets $m^{\prime }\subseteq m$, and thus all points of $m$ are outside $a$.

We have thus seen that the set-thoretical standard model is a concrete example of a structure for interpreting context terms and formulae.

5. A fuzzy context logic

The key to the proposed fuzzy context logic is to additionally provide a fuzzy interpretation for the atomic formulae, via the symbol $⊑$. To do that, we need a residual that takes two elements from the context lattice and produces a fuzzy value in $\left[0,1\right]$. Then we can apply one of the well-known standard fuzzy semantics to the formula level.

The fuzzy semantics is defined by two lattices: a bounded lattice $\left(L_T,{\preccurlyeq }_T,t_T,s_T,1_T\right)$ for the term level, and another bounded lattice $\left(L_F,{\preccurlyeq }_F,s_F,t_F,r_F,1_F\right)$, where $L_F=\left[0,1\right]$ for the formula level together with the interpretation functions $a:{\mathcal{V}}_C\to L_T$ for context variables, $i:{\mathcal{T}}_C\to L_T$ for terms, and $I:{\mathcal{L}}_C\to L_F$ for formulae. We interpret the terms as before based on $L_T$:

$$i\left(v\right)=a\left(v\right),\text{for} v\in V_C$$

$$i\left(\sim c\right)=1_T-i\left(c\right),$$

with the $1_T-i\left(c\right)$term-level pseudo-complement

$$\begin{array}{l}i\left(c\sqcap d\right)=t_T\left(i\left(c\right),i\left(d\right)\right)\\ i\left(c\bigsqcup d\right)=s_T\left(i\left(c\right),i\left(d\right)\right).\end{array}$$

We will need to characterize a fuzzified variant of ${\preccurlyeq }_T$ to obtain atomic formulae that can have a value outside of {0, 1}:

$$I\left(c⊑d\right)={\preccurlyeq }_{\mathit{TF}}(i\left(c\right),i\left(d\right).$$

On this basis, the interpretation of formulae can then follow one of the standard models of fuzzy logic in $L_F$:

$$\begin{array}{c}I\left(\neg \varphi \right)=1_F-I\left(\varphi \right)\\ I\left(\varphi \wedge \psi \right)=t_F\left(I\left(\varphi \right),I\left(\psi \right)\right)\\ I\left(\varphi \vee \psi \right)=s_F\left(I\left(\varphi \right),I\left(\psi \right)\right)\end{array}$$

The key is to provide a function ${\preccurlyeq }_{\mathit{TF}}:L_T\times L_T\to L_F$ for connecting the fuzzy term and formula layers. As usual, we want the relation to be conservative with respect to the classical partial order relation on the classical cases:

$$\begin{array}{c}{\preccurlyeq }_{\mathit{TF}}\left(x,y\right)=1_F\mathrm{iff} x{\preccurlyeq }_{T}y.\\ {\preccurlyeq }_{\mathit{TF}}\left(x,x\right)=1_F\text{holds\hspace{0.17em}for} \mathrm{all} x\in L_T.\\ \text{If}{\preccurlyeq }_{\mathit{TF}}\left(x,y\right)=1_F \text{and}{\preccurlyeq }_{\mathit{TF}}\left(y,x\right)=1_F\text{for} x,y\in L_T \text{then} x=y.\\ \text{If}{\preccurlyeq }_{\mathit{TF}}\left(x,y\right)=1_F \text{and}{\preccurlyeq }_{\mathit{TF}}\left(y,z\right)=1_F \text{then\hspace{0.17em}also}{\preccurlyeq }_{\mathit{TF}}\left(x,z\right)=1_F.\end{array}$$

What is a good choice depends on both $L_T$ and $L_F$, and given a particular choice, different functions may support this weak restriction. A candidate for spatial applications for $L_T=2^B$ for a base set $B$ and $L_F=\left[0,1\right]$ is a fuzzified variant of the qualitative granular relation systems proposed in [32]. Here, several types of granular relations between regions are distinguished based on an absolute ranking of sizes, such as the largest circle a spatial region is contained in, or its diameter, or the length of an interval. Complementing topological notions, such as part-of or overlap, granular relations can be defined [32]:

• Two regions are adjacent iff they overlap but only in a part smaller than grain-size.

• Two regions are spatially indistinguishable iff they differ only in a part smaller than grain-size.

• Two regions relevantly overlap iff they overlap in a part larger than grain-size and differ in a part larger than grain-size.

We can generalize this notion using a $\left[0,1\right]$ perspective instead of a discrete partitioning of the space of possible overlap-relations. For the example of a set-theoretical model, we could proceed, e.g., to find a fuzzification of $\subseteq$ into a function ${\subseteq }_{\mathit{TF}}$ mapping to $\left[0,1\right]$ by assessing the largest difference between two arguments $x,y$ in comparison to the diameter of $x$. The intervals $\left(14,46\right]$ and $\left[14,46\right)$, for instance differ only in boundary points. The intervals $x=\left(11,34\right)$ and $y=\left(12,36\right)$ overlap in $x\cap y=\left(12,34\right)$. With the overlap $\mid x\cap y\mid =\mid \left(12,34\right)\mid =12$ and $\mid x\mid =\mid \left(11,34\right)\mid =13$, this is an overlap of $\mid x\cap y\mid /\mid x\mid =12/13=92\%$.

Generally, we can employ a granularity function $\gamma :L_T\to {\mathbb{R}}^{+}$ to compute a mapping from entities of $L_T$ to ${\mathbb{R}}^{+}$. Based on this, we can use a suitable function $r:L_T\to L_F$ to make the transition between the term layer and the formula layer in such a way that it also connects appropriately to the basic properties of the residual $r_F$, e.g., by employing $r_F$ itself:

$${\preccurlyeq }_{\mathit{TF}}\left(x,y\right)=r_F\left(\gamma \left(x\right),\gamma \left(x\cap y\right)\right).$$

We obtain a fully specified family of fuzzy context logics. Note that with $r_F=r_{\text{prod}}$, we receive the conditional probability:

$$r_{\text{prod}}\left(\gamma \left(x\right),\gamma \left(x\cap y\right)\right)=\frac{\gamma \left(x\cap y\right)}{\gamma \left(x\right)}=\left\{\begin{array}{ll}1& \text{if} x\subseteq y\\ \frac{\gamma \left(x\cap y\right)}{\gamma \left(x\right)}& \text{otherwise}\end{array}\right.$$

For $r_F=r_{\min }$ we obtain:

$$r_{\min }\left(\gamma \left(x\right),\gamma \left(x\cap y\right)\right)=\left\{\begin{array}{ll}1& \mathrm{iff} x\subseteq y\\ \gamma \left(x\cap y\right)& \text{otherwise}.\end{array}\right.$$

Among the potential applications, a two-layered fuzzy logic can help to reason about fuzzy logic systems. The base logic being decidable for the classical semantics, we can, at least for the classical case, make absolute guarantees for a given system. We can prove whether a given fuzzy system, e.g., the output of a machine learning mechanism, such as an ANFIS, together with a description of possible situations in the domain and desirable properties yields a tautology, thus proving that the system has the desirable properties under all possible circumstances. If we are interested in gaining an understanding of systems that are not tautological in this sense, so as to obtain, e.g., degrees of possibility of failure under certain circumstances, more advanced fuzzy proof methods are required.

6. Conclusions

This chapter illustrated that the lwo-layered logic context logic and fuzzy logic can be combined in a meaningful way. We first mapped both logics to a predicate logical background language, so as to highllight their commonalities and differences and to obtain a background compatible with both. In both cases, we discussed a common set-theoretical model that can be used to interpret the background language. We formally proved that the lattice-based generalized $t$-norms of fuzzy logic provide a suitable semantics for the term-layer of context logic. To do this, we expressed context logic in terms of a single pre-order relation that additionally supports the weak supplementation principle and showed that, with this translation providing semantics, context logic fulfills the properties of a residuated lattice. We also derived that the language is decidable in EXPSPACE.

The formula-layer of context logic could then additionally be imbued with a $\left[0,1\right]$-based fuzzification. Proposals for adding either the product $t$-norm or the minimum $t$-norm for the formula layer on top of the lattice-based generalized $t$-norm of the context term layer were suggested, and a mechanism for combining this with granularity to further expand expressiveness was discussed.

Acknowledgments

This work was financially supported by the Hanse-Wissenschaftskolleg, Delmenhorst, Germany; and received infrastructural support from the University of Bremen, Germany.