Algebraic structures formalizing the logic with unsharp implication and negation Open Access

Abstract

1 Introduction

Intuitionistic logic is usually algebraically formalized by means of Heyting algebras, i.e. semilattices |$(S,\wedge ,*)$| where * denotes relative pseudocomplementation, which is considered as a formalization of the connective implication, see [1], [2], [12], [15] and [16]. If |$(S,\wedge ,*)$| has a |$0$|⁠, then |$x*0$| is the pseudocomplement of |$x$| usually denoted by |$x^{*}$| and considered as negation of |$x$| in this logic. Heyting algebras were introduced by L. E. J. Brouwer [1] and A. Heyting, see [14] and [17]. For posets, the authors extended and studied the concept of pseudocomplementation in [4] and [5].

It is well-known that every Heyting algebra is distributive. The concept of relative pseudocomplementation was extended by the first author to non-distributive lattices under the name sectional pseudocomplementation, see [3] and [9]. Hence, a kind of non-distributive intuitionistic logic can be created on sectionally pseudocomplemented lattices.

In their previous papers [6] and [8], the authors showed that some important logics can also be based on posets that need not be lattices. An example of such a logic is the logic of quantum mechanics based on orthomodular posets, see e.g. [6], [10], [11] and [18]. It is evident that in this case, some logical connectives such as disjunction or conjunction may be only partial operations or, as pointed out by the authors in [7] and [8], they may be considered in an ‘unsharp version’, i.e. their result need not be a single element but may be a subset of the poset in question. Thus also the connective implication is created in this way as ‘unsharp’ (for ‘unsharpness’ see also [13]). This motivated us to study algebraic structures based on lattices, which need neither be relatively pseudocomplemented nor even sectionally pseudocomplemented, but can be used for a formalization of a variant of intuitionistic logic whose connective implication is unsharp.

2 Preliminaries

In the following, we identify singletons with their unique element, i.e. we will write |$x$| instead of |$\{x\}$|⁠. Moreover, all posets considered in the sequel are assumed to satisfy the Ascending Chain Condition, which we will abbreviate by ACC. This condition says that within the considered poset there do not exist infinite ascending chains. This implies that every element lies under a maximal one. Of course, every finite poset satisfies the ACC. Let |$(P,\leq )$| be a poset and |$A,B\subseteq P$|⁠. By |$\operatorname {Max} A$|⁠, we will denote the set of all maximal elements of |$A$|⁠. We define

The relations |$\leq _{1}$| and |$\approx _{1}$| are a quasiorder relation on |$2^{P}$| and an equivalence relation on |$2^{P}$|⁠, respectively. It is easy to see that |$A\leq _{1}\operatorname {Max} B$| provided |$A\subseteq B$| and that |$A\leq _{1}b$| is equivalent to |$A\leq b \ (b\in P)$|⁠.

Let |$\mathbf S=(S,\wedge )$| be an arbitrary meet-semilattice and |$A,B\subseteq S$|⁠. We define

For the sake of simplicity, throughout the paper, we will use terms ‘negation’ and ‘implication’ for algebraic operators formalizing these logical connectives without explicitly establishing the corresponding logic.

3 Unsharp negation

Let |$(S,\wedge ,0)$| be a meet-semilattice with |$0$| satisfying the ACC, |$a\in S$| and |$A$| a non-empty subset of |$S$|⁠. We define

Hence, |$^{0}$| is a unary operator on the meet-semilattice |$(S,\wedge ,0)$| with |$0$| satisfying the ACC, which assigns to every element |$x\in S$| the non-void subset |$x^{0}\subseteq S$|⁠. The element |$a$| is called sharp if |$a^{00}=a$|⁠. Moreover, we define

We are going to prove the following properties of the operator |$^{0}$|⁠.

From (iii) of Theorem 3.1, we immediately obtain |$A^{0}\wedge B^{0}\leq _{1}(A\wedge B)^{0}$|⁠.

Figure 1.

Meet-semilattice.

Open in new tabDownload slide

Figure 2.

Modular lattice.

Open in new tabDownload slide

If |$a^{0}$| is a singleton, it need not be a complement of |$a$|⁠, even if the semilattice in question is a lattice. For instance, consider the four-element lattice with atoms |$a$| and |$b$| and with an additional greatest element |$1$|⁠. Then |$a^{0}=b$|⁠, but |$a\vee b\neq 1$|⁠, therefore |$a^{0}$| is not a complement of |$a$|⁠.

For every cardinal number |$n$|⁠, let |$\mathbf M_{n}=(M_{n},\vee ,\wedge )$| denote the bounded modular lattice of length |$2$| having |$n$| atoms.

The situation from Figure 2 can be generalized as follows.

This follows immediately from the fact that every element of a Boolean algebra or lattice of the form |$\mathbf M_{n}$| is sharp.

However, if the lattice |$\mathbf L$| is not a direct product of two-element lattices and various lattices of the form |$\mathbf M_{n}$|⁠, then the assertion of Remark 3.2 need not hold, see the following example.

Figure 3.

Lattice.

Open in new tabDownload slide

We are going to show that the operator |$^{0}$| can be characterized by means of four simple conditions.

4 Unsharp implication

In the sequel, we extend the operation of relative pseudocomplementation to arbitrary meet-semilattices with |$0$| satisfying the ACC as follows: let |$\mathbf S=(S,\wedge ,0)$| be a meet-semilattice with |$0$| satisfying the ACC, |$a,b\in S$| and |$A,B\subseteq S$|⁠. We define

Thus, |$\rightarrow $| is a binary operator on |$S$| assigning to every pair |$(x,y)\in S^{2}$| the non-void subset |$x\rightarrow y\subseteq S$|⁠. It is evident that

Moreover, we define

Now we prove some properties of the binary operator |$\rightarrow $|⁠. Let us remark that if |$(P,\leq )$| is a poset satisfying the ACC and |$A$| a non-empty subset of |$P$| then |$\operatorname {Max} A\neq \emptyset $|⁠.

From Theorem 4.1, it becomes evident that the binary operator |$\rightarrow $| shares properties of the logical connective implication in intuitionistic logic despite the fact that it is unsharp, which means that for |$x,y\in S$| the result of |$x\rightarrow y$| need not be a singleton. This extends the intuitionistic logic based on a Heyting algebra |$(L,\vee ,\wedge ,*,0)$| where |$\vee $|⁠, |$\wedge $|⁠, |$\rightarrow $| and |$^{0}$| formalize disjunction, conjunction, unsharp implication and unsharp negation, respectively. Note that |$x\rightarrow 0 = x^{0}$| as remarked at the beginning of Section 4.

Figure 4.

Modular lattice.

Open in new tabDownload slide

Similarly as for the unary operator |$^{0}$|⁠, we can characterize the binary operator |$\rightarrow $| on a meet-semilattice with |$0$| satisfying the ACC as follows.

5 Deductive systems

It is well-known that the connective implication in intuitionistic logic is closely related to the so-called deductive systems in the corresponding Heyting algebra. Let us show that a certain modification of the concept of a deductive system plays a similar role for logics with unsharp implication. We define

In a Heyting algebra, there are everywhere defined operations |$\vee $| and |$\wedge $| since it is a lattice and hence the definition of a deductive system is different as follows: if |$x\in D$| and |$x\rightarrow y\in D$|⁠, then |$y\in D$|⁠.

Recall that a filter of a meet-semilattice |$\mathbf S=(S,\wedge )$| is a non-empty subset |$F$| of |$S$| satisfying the following conditions for |$x,y\in S$|⁠:

• (F1)

  |$x,y\in F$| implies |$x\wedge y\in F$|⁠,

• (F2)

  |$x\in F$| and |$x\leq y$| imply |$y\in F$|⁠.

It is clear that if |$S$| is finite then all filters of |$\mathbf S$| are given by the sets |$[x):=\{y\in S\mid x\leq y\}$|⁠, |$x\in S$|⁠, and hence the poset of all filters of |$\mathbf S$| is dually isomorphic to |$\mathbf S$| and therefore a join-semilattice where |$[x)\vee [y)=[x\wedge y)$| for all |$x,y\in S$|⁠.

For every non-empty subset |$A$| of the universe of a meet-semilattice |$(S,\wedge )$|⁠, we define a binary relation |$\varTheta (A)$| on |$S$| as follows:

Although the following result is known, for the reader’s convenience, we present a proof.

Although our definition of a deductive system differs from that one known for relatively pseudocomplemented semilattices, we are still able to prove the following relationships between the concepts mentioned before.

It is well known that for a filter |$F$| of a relatively pseudocomplemented semilattice, we have |$(a,b)\in \varTheta (F)$| if and only if both |$a\rightarrow b\in F$| and |$b\rightarrow a\in F$|⁠. However, we can also modify this result for an arbitrary meet-semilattice with |$0$| satisfying the ACC provided our unsharp implication is considered.

Conclusion

Although the operator used for a formalization of implication based on the structure |$(S,\wedge ,0,\rightarrow )$| is unsharp, i.e. |$x\rightarrow y$| may be a subset |$I$| of |$S$|⁠, which need not be a singleton, it has some logical meaning. Namely, we ask that |$x\rightarrow y$| consists of the maximal elements |$c$| of |$S$| satisfying |$x\wedge c\leq y$| (here |$\wedge $| denotes conjunction). Moreover, the elements of |$I$| are mutually incomparable. Thus, there is no need to prefer one of them with respect to others. However, the expression

is nothing else than the derivation rule Modus Ponens (both in classical as well as in non-classical logic) since it properly says that the truth value of |$y$| cannot be less than the truth value of the conjunction |$x\wedge (x\rightarrow y)$| of |$x$| and the implication |$x\rightarrow y$|⁠. Hence, despite of the fact of unsharpness, such a logic based on our algebraic structure is sound although it is derived from an arbitrary meet-semilattice with |$0$| satisfying the ACC.

Acknowledgements

The authors are grateful to the anonymous referees whose valuable remarks helped to increase the quality of the paper. Support of the research of the authors by the Austrian Science Fund (FWF), project I 4579-N, and the Czech Science Foundation (GAČR), project 20-09869L, entitled ‘The many facets of orthomodularity’, is gratefully acknowledged.

References