arXiv reader

Implication in finite posets with pseudocomplemented sections

Ivan Chajda and Helmut Länger

arXiv
2108.09548v1 · PDF · 21 August 2021
Categories
math.LO
Licence
CC BY 4.0 The site shows the text.

Abstract

It is well-known that relatively pseudocomplemented lattices can serve as an algebraic semantics of intuitionistic logic. To extend the concept of relative pseudocomplementation to non-distributive lattices, the first author introduced so-called sectionally pseudocomplemented lattices, i.e. lattices with top element 1 where for every element y the interval [y,1], the so called section, is pseudocomplemented. We extend this concept to posets with top element. Our goal is to show that such a poset can be considered as an algebraic semantics for a certain kind of more general intuitionistic logic provided an implication is introduced as shown in the paper. We prove some properties of such an implication. This implication is "unsharp" in the sense that the value for given entries need not be a unique element, but may be a subset of the poset in question. On the other hand, all of these values are as high as possible. We show that this implication even determines the poset and if a new operator is introduced in an "unsharp" way, such structure forms an "unsharply" residuated poset.

Items 28

Definition

Definition 2.1

XQQM

A finite poset with pseudocomplemented sections is an ordered quadruple \big(P,\leq,(^y;y\in P),1\big) where (P,\leq,1) is a finite poset with top element 1 and for every y\in P, ([y,1],\leq,{}^y,y) is a pseudocomplemented poset. For every y\in P and every subset B of [y,1] put B^y:=\{b^y\mid b\in B\}. Finally, for all x,y\in P define the implication x\rightarrow y as follows:

x\rightarrow y:=\big(\operatorname{Min} U(x,y)\big)^y.

A finite poset with 0 and pseudocomplemented sections is an ordered quintuple \big(P,\leq,(^y;y\in P),0,1\big) where \big(P,\leq,(^y;y\in P),1\big) is a finite poset with pseudocomplemented sections and 0 is the bottom element of (P,\leq).

Remark

Remark 2.2

NPZX

If \big(P,\leq,(^y;y\in P),1\big) is a finite poset with pseudocomplemented sections, b\in P and a\in[b,1] then

a^b=\max\{x\in P\mid L(a,x)\cap[b,1]=b\}.
Lemma

Lemma 2.3

IVSQ

Let \big(P,\leq,(^y;y\in P),1\big) be a finite poset with pseudocomplemented sections and a,b\in P. Then the following hold:

  1. If a\vee b exists in (P,\leq) then a\rightarrow b=(a\vee b)^b,

  2. if b\leq a then a\rightarrow b=a^b.

Proof of Lemma 2.3
  1. If a\vee b exists in (P,\leq) then

    a\rightarrow b=\big(\operatorname{Min} U(a,b)\big)^b=\big(\operatorname{Min} U(a\vee b)\big)^b=(a\vee b)^b.
  2. if b\leq a then because of (i) we have a\rightarrow b=(a\vee b)^b=a^b.

Proposition

Proposition 2.4

D1YT

Let \big(P,\leq,(^y;y\in P),1\big) be a finite poset with pseudocomplemented sections and a,b\in P. Then the following hold:

  1. a\leq b if and only if a\rightarrow b=1,

  2. if a\vee b exists then (a\vee b)\rightarrow b=a\rightarrow b,

  3. 1\rightarrow a=a,

  4. a\leq b\rightarrow a,

  5. a\rightarrow(b\rightarrow a)=1.

Uses Definition 2.1 · Used by Proof, Proof
Proof of Proposition 2.4
  1. The following are equivalent:

    \begin{aligned} a & \leq b, \\ \operatorname{Min} U(a,b) & =b, \\ x & =b\text{ for all }x\in\operatorname{Min} U(a,b), \\ x^b & =1\text{ for all }x\in\operatorname{Min} U(a,b), \\ \big(\operatorname{Min} U(a,b)\big)^b & =1, \\ a\rightarrow b & =1, \end{aligned}
  2. if a\vee b exists then

    (a\vee b)\rightarrow b=\big(\operatorname{Min} U(a\vee b,b)\big)^b=\big(\operatorname{Min} U(a\vee b)\big)^b=\big(\operatorname{Min} U(a,b)\big)^b=a\rightarrow b,
  3. 1\rightarrow a=\big(\operatorname{Min} U(1,a)\big)^a=\big(\operatorname{Min} U(1)\big)^a=1^a=a,
  4. a\leq\big(\operatorname{Min} U(b,a)\big)^a=b\rightarrow a,

  5. this follows from (iii) and from (i) of Lemma 2.3.

Proposition

Proposition 2.5

G97U

Let \big(P,\leq,(^y;y\in P),1\big) be a finite poset with pseudocomplemented sections and a,b,c\in P. Then the following hold:

  1. If a\leq b and a\vee c exists in (P,\leq) then b\rightarrow c\leq a\rightarrow c,

  2. if a\vee b exists in (P,\leq) then a\leq(a\rightarrow b)\rightarrow b,

  3. if a\vee b exists in (P,\leq) then a\rightarrow b=\big((a\rightarrow b)\rightarrow b\big)\rightarrow b.

Proof of Proposition 2.5
  1. Since a\vee c exists in (P,\leq), we have a\rightarrow c=(a\vee c)^c according to (i) of Lemma 2.3. Now, by (P2), everyone of the following assertions implies the next one:

    \begin{aligned} a & \leq b, \\ U(b,c) & \subseteq U(a,c), \\ \operatorname{Min} U(b,c) & \subseteq U(a\vee c), \\ a\vee c & \leq x\text{ for all }x\in\operatorname{Min} U(b,c), \\ x^c & \leq(a\vee c)^c=a\rightarrow c\text{ for all }x\in\operatorname{Min} U(b,c), \\ b\rightarrow c & =\big(\operatorname{Min} U(b,c)\big)^c\leq a\rightarrow c \end{aligned}
  2. Because of (P3) and (i) and (ii) of Lemma 2.3 we have

    a\leq a\vee b\leq\big((a\vee b)^b\big)^b=(a\rightarrow b)\rightarrow b.
  3. Because of (i) of Lemma 2.3, (P4) and (ii) of Lemma 2.3 we have

    a\rightarrow b=(a\vee b)^b=\Big(\big((a\vee b)^b\big)^b\Big)^b=\big((a\rightarrow b)\rightarrow b\big)\rightarrow b.
Remark

Remark 2.6

G731

Let (P,\leq,1) be a poset with top element 1 and a,b\in P with b\leq a. Further assume that the sectional pseudocomplement a\circ b of a with respect to b and the pseudocomplement of a^b of a in [b,1] exist. Then a\circ b\leq a^b.

Proof of Remark 2.6

Since b\in L(b)=L\big(U(a,b),a\circ b\big), we have b\leq a\circ b. Moreover,

L(a,a\circ b)\cap[b,1]=L\big(U(a),a\circ b\big)\cap[b,1]=L\big(U(a,b),a\circ b\big)\cap[b,1]=L(b)\cap[b,1]=\{b\}.

Hence a\circ b\leq a^b.

Example

Example 2.7

K9EH

The poset shown in Figure 2:

The paper has a picture here, which this page does not show.

has pseudocomplemented sections and is simultaneously relatively pseudocomplemented. The tables for x^y, \rightarrow and * look as follows:

\begin{array}{c|cccccc} x^y & 0 & a & b & c & d & 1 \\ \hline 0 & 1 & - & - & - & - & - \\ a & b & 1 & - & - & - & - \\ b & a & - & 1 & - & - & - \\ c & 0 & d & d & 1 & - & - \\ d & 0 & c & c & - & 1 & - \\ 1 & 0 & a & b & c & d & 1 \end{array} \quad \begin{array}{c|cccccc} \rightarrow & 0 & a & b & c & d & 1 \\ \hline 0 & 1 & 1 & 1 & 1 & 1 & 1 \\ a & b & 1 & \{c,d\} & 1 & 1 & 1 \\ b & a & \{c,d\} & 1 & 1 & 1 & 1 \\ c & 0 & d & d & 1 & d & 1 \\ d & 0 & c & c & c & 1 & 1 \\ 1 & 0 & a & b & c & d & 1 \end{array} \quad \begin{array}{c|cccccc} * & 0 & a & b & c & d & 1 \\ \hline 0 & 1 & 1 & 1 & 1 & 1 & 1 \\ a & b & 1 & b & 1 & 1 & 1 \\ b & a & a & 1 & 1 & 1 & 1 \\ c & 0 & a & b & 1 & d & 1 \\ d & 0 & a & b & c & 1 & 1 \\ 1 & 0 & a & b & c & d & 1. \end{array}

The intuitionistic implication, i.e. the relative pseudocomplement * differs from our “unsharp” implication \rightarrow, e.g. a*b=b whereas a\rightarrow b=\{c,d\}. Hence, although a\rightarrow b is an “unsharp” implication because its result is a two-element subset of P, its values c and d are greater than the value of intuitionistic implication a*b.

Example

Example 2.8

T9K8

The poset shown in Figure 3:

The paper has a picture here, which this page does not show.

has pseudocomplemented sections, but is not relatively pseudocomplemented since the relative pseudocomplement of b with respect to a does not exist. The tables for x^y and \rightarrow look as follows:

\begin{array}{c|ccccccc} x^y & 0 & a & b & c & d & e & 1 \\ \hline 0 & 1 & - & - & - & - & - & - \\ a & c & 1 & - & - & - & - & - \\ b & c & a & 1 & - & - & - & - \\ c & b & - & - & 1 & - & - & - \\ d & 0 & a & e & e & 1 & - & - \\ e & 0 & a & d & d & - & 1 & - \\ 1 & 0 & a & b & c & d & e & 1. \end{array} \quad\quad\quad \begin{array}{c|ccccccc} \rightarrow & 0 & a & b & c & d & e & 1 \\ \hline 0 & 1 & 1 & 1 & 1 & 1 & 1 & 1 \\ a & c & 1 & 1 & \{d,e\} & 1 & 1 & 1 \\ b & c & a & 1 & \{d,e\} & 1 & 1 & 1 \\ c & b & a & \{d,e\} & 1 & 1 & 1 & 1 \\ d & 0 & a & e & e & 1 & e & 1 \\ e & 0 & a & d & d & d & 1 & 1 \\ 1 & 0 & a & b & c & d & e & 1. \end{array}
Used by Example 4.3
Definition

Definition 3.1

93X0

A finite I-algebra is an ordered triple (A,\rightarrow,1) with a finite set A, an operator \rightarrow:A^2\rightarrow2^A\setminus\{\emptyset\} and 1\in A satisfying the following conditions:

  1. (I1) x\rightarrow x\approx x\rightarrow1\approx1,

  2. (I2) x\rightarrow y=y\rightarrow x=1\Rightarrow x=y,

  3. (I3) x\rightarrow y=y\rightarrow z=1\Rightarrow x\rightarrow z=1,

  4. (I4) y\rightarrow z=z\rightarrow x=z\rightarrow(x\rightarrow y)=1\Rightarrow z=y,

  5. (I5) \big(y\rightarrow x=y\rightarrow u=1\text{ and }(y\rightarrow z=z\rightarrow x=z\rightarrow u=1\Rightarrow z=y)\big)\Rightarrow u\rightarrow(x\rightarrow y)=1,

  6. (I6) x\rightarrow y=\{z\rightarrow y\mid x\rightarrow z=y\rightarrow z=1,\text{ and }x\rightarrow u=y\rightarrow u=u\rightarrow z=1\Rightarrow u=z\}.

Theorem

Theorem 3.2

H8T1

Let \mathbf P=\big(P,\leq,(^y;y\in P),1\big) be a finite poset with pseudocomplemented sections and put x\rightarrow y:=\big(\min U(x,y)\big)^y for all x,y\in P. Then \mathbb I(\mathbf P):=(P,\rightarrow,1) is a finite I-algebra.

Proof of Theorem 3.2

Let a,b\in P. According to (i) of Proposition 2.4, a\leq b if and only if a\rightarrow b=1, and according to (ii) of Lemma 2.3, b\leq a implies a\rightarrow b=a^b. Now (I1) follows since \leq is reflexive and 1 is the top element of (P,\leq), (I2) and (I3) follow by antisymmetry and transitivity of \leq, respectively. Let x,y,z,u\in P. If y\leq z\leq x and z\leq x^y then z\in L(x,x^y)\cap[y,1]=\{y\}, i.e. z=y which shows that (I4) holds. Now for x,u\in[y,1] the following are equivalent:

\begin{aligned} y\rightarrow z=z\rightarrow x=z\rightarrow u=1 & \Rightarrow z=y, \\ z\in L(x,u)\cap[y,1] & \Rightarrow z=y, \\ L(x,u)\cap[y,1] & \subseteq\{y\}, \\ L(x,u)\cap[y,1] & =\{y\}. \end{aligned}

Since for x,u\in[y,1], L(x,u)\cap[y,1]=\{y\} implies u\leq x^y, we have (I5). Finally, (I6) follows from the definition of \rightarrow.

Theorem

Theorem 3.3

XRKH

Let \mathbf A=(A,\rightarrow,1) be a finite I-algebra and define

\begin{aligned} x\leq y & :\Leftrightarrow x\rightarrow y=1, \\ x^y & :=x\rightarrow y\text{ whenever }y\leq x \end{aligned}

(x,y\in A). Then \mathbb P(\mathbf A):=\big(A,\leq,(^y;y\in A),1\big) is a finite poset with pseudocomplemented sections.

Proof of Theorem 3.3

Because of (I1) – (I3), (A,\leq,1) is a finite poset with top element 1, because of (I4), L(x,x^y)\cap[y,1]\subseteq\{y\} for all x,y\in I with y\leq x and hence L(x,x^y)\cap[y,1]=\{y\} for all x,y\in I with y\leq x, and because of (I5), y\in A, x,u\in[y,1] and L(x,u)\cap[y,1]=\{y\} imply u\leq x^y. Hence for all y\in A, ([y,1],\leq,{}^y,y) is a pseudocomplemented poset.

Remark

Remark 3.4

GCZI

In the above proof, condition (I6) of Definition 3.1 is not needed. We need this condition in order to prove that the above described correspondence is one-to-one.

Theorem

Theorem 3.5

9YTL

The correspondence described in Theorems 3.2 and 3.3 is one-to-one.

Proof of Theorem 3.5

Let \mathbf P=\big(P,\leq,(^y;y\in P),1\big) be a finite poset with pseudocomplemented sections, put

\begin{aligned} \mathbb I(\mathbf P) & =(P,\rightarrow,1), \\ \mathbb P\big(\mathbb I(\mathbf P)\big) & =\big(P,\leq',(_y;y\in P),1\big) \end{aligned}

and let a,b\in P. Then because of the definition of \leq' and (i) of Proposition 2.4 the following are equivalent:

\begin{aligned} a & \leq'b, \\ a\rightarrow b & =1, \\ a & \leq b. \end{aligned}

If b\leq a then because of the definition of a_b and (ii) of Lemma 2.3 we have a_b=a\rightarrow b=a^b This shows \mathbb P\big(\mathbb I(\mathbf P)\big)=\mathbf P. Now let \mathbf A=(A,\rightarrow,1) be a finite I-algebra, put

\begin{aligned} \mathbb P(\mathbf A) & =\big(A,\leq,(^y;y\in I),1\big), \\ \mathbb I\big(\mathbb P(\mathbf A)\big) & =(A,\Rightarrow,1) \end{aligned}

and let a,b\in A. Then

a\Rightarrow b=\big(\operatorname{Min} U(a,b)\big)^b=\{x^b\mid a,b\leq x,\text{ and }a,b\leq y\leq x\text{ implies }y=x\}=a\rightarrow b

because of the definition of \leq and (I6). This shows \mathbb I\big(\mathbb P(\mathbf A)\big)=\mathbf A.

Remark

Remark 3.6

9K19

Condition (P2) expresses the fact that our negation and implication satisfy the contraposition law, i.e.

\text{if }x\rightarrow y=1\text{ then also }\neg y\rightarrow\neg x=1.
Proposition

Proposition 3.7

Z8DK

Let \mathbf P=(P,\leq,{}',0,1) be a bounded pseudocomplemented poset. Then (P',\leq,{}',0,1) with P':=\{x'\mid x\in P\} is a complemented poset.

Proof of Proposition 3.7

Clearly, P'=\{x\in P\mid x''=x\}. Let a,b\in P'. Then a'\in P'. Moreover, L(a,a')=0. If b\in U(a,a') then b'\in L(a',a'')=L(a,a')=0 and hence b=b''=0'=1. This shows U(a,a')=1, i.e. a' is a complement of a.

Example

Example 3.8

QAFC

If (P,\leq,{}',0,1) is the bounded pseudocomplemented poset of Example 2.8 then the complemented poset (P',\leq,{}',0,1) is depicted in Figure 4:

The paper has a picture here, which this page does not show.
Definition

Definition 4.1

A5AZ

A poset \mathbf P=(P,\leq,\odot,\rightarrow,1) with top element 1 and two operators \odot and \rightarrow, both mappings from P^2 to 2^P, such that

  1. \odot is commutative and associative and x\odot1\approx x,

  2. if x\leq y and z\in P then there exists some t\in y\odot z with x\odot z\leq t,

  3. z\in x\odot y if and only if (z\leq x,y and x\leq y\rightarrow z)

will be called unsharply residuated. Condition (iii) will be called unsharp adjointness. We call an unsharply residuated poset \mathbf P divisible if for all x,y\in P with x\geq y we have that x\rightarrow y is a singleton and \big(x\odot(x\rightarrow y)\big)\cap[y,1]=\{y\}.

Theorem

Theorem 4.2

23RM

Let \big(P,\leq,(^y;y\in P),1\big) be a finite poset with pseudocomplemented sections and for x,y\in P define

\begin{aligned} x\odot y & :=\operatorname{Max} L(x,y), \\ x\rightarrow y & :=\big(\operatorname{Min} U(x,y)\big)^y. \end{aligned}

Then (P,\leq,\odot,\rightarrow,1) is unsharply residuated and divisible.

Proof of Theorem 4.2

Let a,b,c\in P. Then

a\odot1=\operatorname{Max} L(a,1)=\operatorname{Max} L(a)=a

and, clearly, \odot is commutative. Moreover,

\begin{aligned} (a\odot b)\odot c & =\operatorname{Max} L\big(\operatorname{Max} L(a,b),c\big)=\operatorname{Max}\Big(L\big(\operatorname{Max} L(a,b)\big)\cap L(c)\Big)= \\ & =\operatorname{Max}\big(L(a,b)\cap L(c)\big)=\operatorname{Max} L(a,b,c)=\operatorname{Max}\big(L(a)\cap L(b,c)\big)= \\ & =\operatorname{Max}\Big(L(a)\cap L\big(\operatorname{Max} L(b,c)\big)\Big)=\operatorname{Max} L\big(a,\operatorname{Max} L(b,c)\big)=a\odot(b\odot c). \end{aligned}

Thus \odot satisfies (i) of Definition 4.1. If a\leq b then

a\circ c=\operatorname{Max} L(a,c)\subseteq L(a,c)\subseteq L(b,c)

and hence there exists some d\in\operatorname{Max} L(b,c) with a\odot c\leq d. This shows (ii) of Definition 4.1. Now unsharp adjointness remains to be proved. Because of Lemma 2.3 (ii) the following are equivalent:

\begin{aligned} & c\in a\odot b, \\ & c\in\operatorname{Max} L(a,b), \\ & L(a,b)\cap[c,1]=\{c\}, \\ & c\leq a,b\text{ and }a\leq b^c, \\ & c\leq a,b\text{ and }a\leq b\rightarrow c. \end{aligned}

Now assume a\geq b. Then a\rightarrow b=a^b and

\big(a\odot(a\rightarrow b)\big)\cap[b,1]=\big(\operatorname{Max} L(a,a^b)\big)\cap[b,1]\subseteq L(a,a^b)\cap[b,1]=\{b\}.

On the other hand, b\in L(a,a^b) and if b\leq c\in L(a,a^b) then c\in L(a,a^b)\cap[b,1]=\{b\}, i.e. c=b. This shows that b\in\operatorname{Max} L(a,a^b) and hence b\in\big(\operatorname{Max} L(a,a^b)\big)\cap[b,1], thus

\big(\operatorname{Max} L(a,a^b)\big)\cap[b,1]=\{b\}.

proving divisibility of (P,\leq,\odot,\rightarrow,1).

Example

Example 4.3

2HO5

Let us consider the poset from Example 2.8. The table for \odot looks as follows:

\begin{array}{c|ccccccc} \odot & 0 & a & b & c & d & e & 1 \\ \hline 0 & 0 & 0 & 0 & 0 & 0 & 0 & 0 \\ a & 0 & a & a & 0 & a & a & a \\ b & 0 & a & b & 0 & b & b & b \\ c & 0 & 0 & 0 & c & c & c & c \\ d & 0 & a & b & c & d & \{b,c\} & d \\ e & 0 & a & b & c & \{b,c\} & e & e \\ 1 & 0 & a & b & c & d & e & 1. \end{array}

We can see that d\odot e=\{b,c\} is not a singleton, and b\in d\odot e implies b\leq d,e and d\leq d=e\rightarrow b; also, conversely, c\leq e,d and e\leq e=d\rightarrow c imply c\in\{b,c\}=e\odot d.

Source and licence

The text on this page is from arXiv:2108.09548v1 by Ivan Chajda and Helmut Länger, under the licence CC BY 4.0. The corpus made these changes: it read the items out of the LaTeX source, it expanded the macros of the paper, it put each proof after its statement, and it converted the text to HTML. The formulas are the TeX of the paper, and KaTeX renders them. A formula or a reference can look different from the PDF. The page is published under CC BY 4.0.

The record of each item is in analysis/objects/2108/2108.09548.jsonl.