11footnotetext: Support of the research of the first author by IGA, project
PřF 2023 010, and of the second author by the Austrian Science Fund (FWF),
project I 4579-N, entitled “The many facets of orthomodularity”, is gratefully
acknowledged.

# The intuitionistic-like logic based on a poset

Ivan Chajda and Helmut Länger1

###### Abstract

The aim of the present paper is to show that the concept of intuitionistic
logic based on a Heyting algebra can be generalized in such a way that it is
formalized by means of a bounded poset. In this case it is not assumed that
the poset is relatively pseudocomplemented. The considered logical connectives
negation, implication or even conjunction are not operations in this poset but
so-called operators since they assign to given entries not necessarily an
element of the poset as a result but a subset of mutually incomparable
elements with maximal possible truth values. We show that these operators for
negation and implication can be characterized by several simple conditions
formulated in the language of posets together with the operator of taking the
lower cone. Moreover, our implication and conjunction form an adjoint pair. We
call these connectives “unsharp” or “inexact” in accordance with the existing
literature. We also introduce the concept of a deductive system of a bounded
poset with implication and prove that it induces an equivalence relation
satisfying a certain substitution property with respect to implication.
Moreover, the restriction of this equivalence on the base set is uniquely
determined by its kernel, i.e. the class containing the top element.

AMS Subject Classification: 06A11, 06D15, 06D20, 03G25, 03B22

Keywords: Bounded poset, logic based on a poset, unsharp negation, unsharp
implication, adjoint operators, Modus Ponens, deductive system, equivalence
relation induced by a deductive system

##  1 Introduction

Intuitionistic logic was algebraically formalized by means of relatively
pseudocomplemented semilattices, see [1], [2] and [14] – [17]. If such a
semilattice is even a lattice, it is called a Heyting algebra, see [14] and
[17]. It is well-known that every relatively pseudocomplemented lattice is
distributive. The concept of relatively pseudocomplemented lattices was
extended by the first author to non-distributive lattices in [3] under the
name sectional pseudocomplementation. It was further extended also for posets
in [10]. Thus a kind of intuitionistic logic based on sectionally
pseudocomplemented lattices was realized.

However, there exist logics based on bounded posets, e.g. the logic of quantum
mechanics, see e.g. [7], [8], [13] and [18]. In particular, orthomodular
posets on which the logic of quantum mechanics is based are thoroughly studied
in [7], [8], [11] and [18].

In order to formalize a logic based on a poset, there are two possible ways
how to solve the problem that the operations meet and join need not be defined
everywhere. One method is to consider these operations as partial only and
then the logical connectives formalized by them and by partial operations
derived from them are also only partial. The disadvantage of this approach is
that in some cases, such a logic cannot answer the question what is a logical
conclusion of some reasoning (or sequential derivation). Hence we prefer
another approach, namely we consider so-called operators instead of operations
which assign to given entries not necessarily an element as the result, but a
certain subset of elements with maximal values. We work with such results of
logical connectives which are subsets, but their elements are mutually
incomparable. It means that one cannot prefer one element of this set with
respect to the other elements. Hence such a logic based on a poset gets an
answer concerning logical derivation in each case, but the result may be
“inexact” or “unsharp”, see e.g. [9] or [13]. We suppose that if an exact
logical derivation is impossible from the reasons mentioned above, it is
better to have an unsharp result than none. In our opinion unsharp reasoning
is an alternative to multiple-valued reasoning which is now generally accepted
though it was not accepted by all specialists at first.

In their recent paper [9] the authors showed that a certain intuitionistic-
like logic can be derived based on arbitrary meet-semilattices satisfying the
Ascending Chain Condition (ACC) regardless whether there exist (relative)
pseudocomplements or not. We can ask if similar logics may be derived also by
means of arbitrary posets with $0$ satisfying the ACC. Within meet-
semilattices the logical connective conjunction is usually formalized by the
meet operation. Then the unsharp implication as introduced in [9] forms an
adjoint operator to conjunction. In the case of a poset we must find another
operator formalizing conjunction. In [13] so-called unsharp properties of
formal logics were used. In [9] we considered unsharpness of implication as
well as of negation. This means that for given propositions $p$ and $q$ the
results of the implication $p\rightarrow q$ and of the negation $\neg p$,
respectively, need not be elements of the corresponding meet-semilattice
$\mathbf{L}$, but may be non-empty subsets of it consisting of mutually
incomparable maximal elements. When proceeding from meet-semilattices to
posets, we will apply this principle again for the connective conjunction in
such a way that implication and conjunction will still be connected by a
certain kind of adjointness, see e.g. [6]. Due to this fact, in such logics we
still have the derivation rule Modus Ponens.

##  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 implies that every element lies under a maximal one.
Of course, every finite poset satisfies the ACC.

In the sequel we will use the following notation: Let $\mathbf{P}=(P,\leq)$ be
a poset, $a,b,c\in P$ and $A,B$ be non-empty subsets of $P$.

$\displaystyle\operatorname{Max}A$ $\displaystyle:=\text{ set of all maximal
elements of }A,$ $\displaystyle L(a,b)$ $\displaystyle:=\\{x\in P\mid x\leq
a,b\\},$ $\displaystyle\Lambda(A,B)$ $\displaystyle:=\bigcup_{x\in A,y\in
B}L(x,y),$ $\displaystyle A\leq B$ $\displaystyle\text{ if }x\leq y\text{ for
all }x\in A\text{ and all }y\in B,$ $\displaystyle A\leq_{1}B$
$\displaystyle\text{ if for every }x\in A\text{ there exists some }y\in
B\text{ with }x\leq y,$ $\displaystyle A=_{1}B$ $\displaystyle\text{ if both
}A\leq_{1}B\text{ and }B\leq_{1}A.$

The relations $\leq_{1}$ and $=_{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$.

If a poset $\mathbf{P}$ has a bottom and a top element, we will denote them by
$0$ and $1$, respectively, and we will express this fact by writing
$\mathbf{P}=(P,\leq,0,1)$. Such a poset is called bounded.

The element $c$ is called the relative pseudocomplement of $a$ with respect to
$b$, formally $c=a*b$, if $c$ is the greatest element $x$ of $P$ satisfying
$L(a,x)\leq b$. If $\mathbf{P}=(P,\leq,0)$ then the relative pseudocomplement
$a*0$ of $a$ with respect to $0$ is denoted by $a^{*}$ and called the
pseudocomplement of $a$, see e.g. [4] or [12]. Especially, we have
$L(a,a^{*})=0$.

##  3 Negation derived in posets

Consider a bounded poset $\mathbf{P}=(P,\leq,0)$ satisfying the ACC. For $a\in
P$ we define

$a^{0}:=\operatorname{Max}\\{x\in P\mid L(a,x)=0\\}.$

Clearly. $a^{0}$ need not be an element of $P$, but it is a non-empty subset
of $P$ since $L(a,0)=0$. From now on, we will call $a^{0}$ the unsharp
negation of $a$. Of course, if the pseudocomplement $a^{*}$ of $a$ exists then
$a^{0}=a^{*}$.

We extend this concept to subsets of $P$ as follows: If $A$ is a non-empty
subset of $P$ then

$A^{0}:=\operatorname{Max}\\{x\in P\mid L(x,y)=0\text{ for all }y\in A\\}.$

We are going to show that the negation 0 defined in this way shares several
properties with the negation in intuitionistic logic.

######  Theorem 3.1.

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC, $a,b\in
P$ and $A,B$ non-empty subsets of $P$. Then the following holds:

  1. (i)

$A^{0}$ is an antichain, in particular $a^{0}$ is an antichain,

  2. (ii)

$0^{0}=1$ and $1^{0}=0$,

  3. (iii)

$L(x,y)=0$ for all $x\in A$ and all $y\in A^{0}$, in particular $L(a,y)=0$ for
all $y\in a^{0}$,

  4. (iv)

$A\leq_{1}B$ implies $B^{0}\leq_{1}A^{0}$, in particular $a\leq b$ implies
$b^{0}\leq a^{0}$,

  5. (v)

$A^{0}=_{1}B^{0}$ implies $A^{0}=B^{0}$, in particular $a^{0}=_{1}b^{0}$
implies $a^{0}=b^{0}$; $A^{0}=_{1}b$ implies $A^{0}=b$, in particular
$a^{0}=_{1}b$ implies $a^{0}=b$,

  6. (vi)

$A\leq_{1}A^{00}$, in particular $a\leq_{1}a^{00}$; $A^{000}=A^{0}$, in
particular $a^{000}=a^{0}$,

  7. (vii)

$\Lambda\Big{(}a,\big{(}L(a,b)\big{)}^{0}\Big{)}=_{1}\Lambda(a,b^{0})$.

###### Proof.

  1. (i)

– (iii) follow directly from the definition of 0.

  2. (iv)

If $A\leq_{1}B$ then

$\\{x\in P\mid L(x,y)=0\text{ for all }y\in B\\}\subseteq\\{x\in P\mid
L(x,y)=0\text{ for all }y\in A\\}.$

  3. (v)

Assume $a\in A^{0}=_{1}B^{0}$. Because of $A^{0}\leq_{1}B^{0}$ there exists
some $b\in B^{0}$ with $a\leq b$, and because of $B^{0}\leq_{1}A^{0}$ there
exists some $c\in A^{0}$ with $b\leq c$. Together we obtain $a\leq b\leq c$
and hence $a\leq c$. Since $a$ and $c$ belong to the antichain $A^{0}$ we
conclude $a=c$ and therefore $a=b\in B^{0}$. This shows $A^{0}\subseteq
B^{0}$. Interchanging the roles of $A^{0}$ and $b^{0}$ yields $B^{0}\subseteq
A^{0}$. Together we obtain $A^{0}=B^{0}$. Now assume $a\in A^{0}=_{1}b$.
Because of $A^{0}\leq_{1}b$ we have $a\leq b$, and because of $b\leq_{1}A^{0}$
there exists some $c\in A^{0}$ with $b\leq c$. Together we obtain $a\leq b\leq
c$ and hence $a\leq c$. Since $a$ and $c$ belong to the antichain $A^{0}$ we
conclude $a=c$ and therefore $a=b$. This shows $A^{0}=b$.

  4. (vi)

We have $A\subseteq\\{x\in P\mid L(x,y)=0\text{ for all }y\in A^{0}\\}$ and
hence $A\leq_{1}A^{00}$. Replacing $A$ by $A^{0}$ we get
$A^{0}\leq_{1}A^{000}$. From $A\leq_{1}A^{00}$ and (iv) we obtain
$a^{000}\leq_{1}A^{0}$. Together we have $A^{000}=_{1}A^{0}$ whence
$A^{000}=A^{0}$ according to (v).

  5. (vii)

Any of the following statements implies the next one:

    1. (1)

$L(x,y)=0$ for all $x\in\big{(}L(a,b)\big{)}^{0}$ and all $y\in L(a,b)$,

    2. (2)

$L(b,y)=0$ for all $x\in\big{(}L(a,b)\big{)}^{0}$ and all $y\in L(a,x)$,

    3. (3)

$\Lambda\Big{(}a,\big{(}L(a,b)\big{)}^{0}\Big{)}\leq_{1}b^{0}$,

    4. (4)

$\Lambda\Big{(}a,\big{(}L(a,b)\big{)}^{0}\Big{)}\leq_{1}\Lambda(a,b^{0})$.

That (1) implies (2) can be seen as follows: If
$x\in\big{(}L(a,b)\big{)}^{0}$, $y\in L(a,x)$ and $c\in L(b,y)$ then $c\in
L(a,b)$ and $c\leq x$ and therefore $L(x,c)=0$ by (1) whence $L(c)=L(x,c)=0$,
i.e. $c=0$. From $L(a,b)\leq b$ we conclude
$b^{0}\leq_{1}\big{(}L(a,b)\big{)}^{0}$ according to (iv) and hence

$\Lambda(a,b^{0})\leq_{1}\Lambda\Big{(}a,\big{(}L(a,b)\big{)}^{0}\Big{)}.$

∎

######  Example 3.2.

Consider the bounded poset $\mathbf{P}=(P,\leq,0,1)$ visualized in Fig. 1:

$0$$a$$b$$c$$d$$e$$f$$1$Fig. 1Bounded poset

We have

$\begin{array}[]{l|l|l|l|l|l|l|l|l}x&0&a&b&c&d&e&f&1\\\ \hline\cr
x^{0}&1&f&ac&d&c&0&a&0\\\ \hline\cr x^{00}&0&a&b&c&d&1&f&1\end{array}$

(Here and in the following we write $a_{1}\ldots a_{n}$ instead of
$\\{a_{1},\ldots,a_{n}\\}$.) One can see that $x^{00}=x$ for all $x\in
P\setminus\\{e\\}$ and $e^{00}=1\neq e$. But $e^{000}=1^{0}=0=e^{0}$ and hence
$\mathbf{P}$ satisfies the identity $x^{000}\approx x^{0}$ in accordance with
(vi) of Theorem 3.1.

The following example shows that (iv) of Theorem 3.1 does not hold for $\leq$
instead of $\leq_{1}$.

######  Example 3.3.

Consider the bounded poset $\mathbf{P}=(P,\leq,0,1)$ depicted in Fig. 2:

$0$$a$$b$$c$$d$$e$$f$$1$Fig. 2Bounded poset

We have

$\begin{array}[]{l|l|l|l|l|l|l|l|l}x&0&a&b&c&d&e&f&1\\\ \hline\cr
x^{0}&1&ef&acde&abde&abce&af&ae&0\\\ \hline\cr
x^{00}&0&a&b&c&d&e&f&1\end{array}$

and hence $c\leq f$ and $f^{0}\leq_{1}c^{0}$, but
$f^{0}=\\{a,e\\}\not\leq\\{a,b,d,e\\}=c^{0}$.

The next question is whether the unary operator 0 can be characterized by
means of simple conditions formulated in the language of posets. This is
possible, see the following theorem.

######  Theorem 3.4.

Let $(P,\leq,0,1)$ be a bounded poset satisfying the ACC and 0 a unary
operator on $P$. Then the following conditions (1) and (2) are equivalent:

  1. (1)

$x^{0}=\operatorname{Max}\\{y\in P\mid L(x,y)=0\\}$ for all $x\in P$,

  2. (2)

the operator ${}^{0}\colon 2^{P}\rightarrow 2^{P}$ (restricted to $P$)
satisfies the following conditions for all $x\in P$:

    1. (P1)

$x^{0}$ is an antichain,

    2. (P2)

$L(x,y)=0$ for all $y\in x^{0}$,

    3. (P3)

$\Lambda\Big{(}x,\big{(}L(x,y)\big{)}^{0}\Big{)}=_{1}\Lambda(x,y^{0})$.

###### Proof.

(1) $\Rightarrow$ (2):
This follows from Theorem 3.1.
(2) $\Rightarrow$ (1):
If $L(x,y)=0$ then according to (P3) we have

$y=_{1}L(y,1)=\Lambda\Big{(}y,\big{(}L(x,y)\big{)}^{0}\Big{)}=\Lambda\Big{(}y,\big{(}L(y,x)\big{)}^{0}\Big{)}=_{1}\Lambda(y,x^{0})\leq_{1}x^{0}$

and hence $y\leq_{1}x^{0}$. Conversely, if $y\leq_{1}x^{0}$ then according to
(P2) we get

$L(x,y)\subseteq\Lambda(x,x^{0})=0$

which implies $L(x,y)=0$. This shows that $L(x,y)=0$ is equivalent to
$y\leq_{1}x^{0}$. We conclude

$\operatorname{Max}\\{y\in P\mid L(x,y)=0\\}=\operatorname{Max}\\{y\in P\mid
y\leq_{1}x^{0}\\}=x^{0}.$

The last equality can be seen as follows. Let $z\in\operatorname{Max}\\{y\in
P\mid y\leq_{1}x^{0}\\}$. Then $z\leq_{1}x^{0}$, i.e. there exists some $u\in
x^{0}$ with $z\leq u$. We have $u\leq_{1}x^{0}$. Then $z<u$ would imply
$z\notin\operatorname{Max}\\{y\in P\mid y\leq_{1}x^{0}\\}$, a contradiction.
This shows $z=u\in x^{0}$. Conversely, assume $z\in x^{0}$. Then
$z\leq_{1}x^{0}$. If $z\notin\operatorname{Max}\\{y\in P\mid
y\leq_{1}x^{0}\\}$ then there would exist some $u\in P$ with
$z<u\leq_{1}x^{0}$ and hence there would exist some $w\in x^{0}$ with $z<u\leq
w$ contradicting (P1). This shows $z\in\operatorname{Max}\\{y\in P\mid
y\leq_{1}x^{0}\\}$. ∎

##  4 Unsharp implication and conjunction

Let us recall that Brouwerion semilattices are relatively pseudocomplemented
meet-semilattices, see e.g. [15] and [16]. It is familiarly known that in
logics based on Brouwerian semilattices or on Heyting algebras the relative
pseudocomplement is considered as the logical connective implication, i.e.

$x\rightarrow y=x*y=\operatorname{Max}\\{z\in S\mid x\wedge z\leq y\\}.$

Of course, $\operatorname{Max}\\{z\in S\mid x\wedge z\leq y\\}$ is a
singleton, thus $x*y$ is an element of $S$. In our case we will use formally
the same definition, but the result $x\rightarrow y$ need not be an element of
the poset $\mathbf{P}$ in question, but may be a subset of $P$ in general.
However, the elements of $x\rightarrow y$ are mutually incomparable and of a
maximal possible value. Hence one cannot pick up one of them to be the
preferable element. Now we are going to define our main concept, i.e. the
operator $\rightarrow$ which formalizes the logical connective implication. As
mentioned above, for given entries $x$ and $y$ the result of $x\rightarrow y$
may be a subset of $P$. Due to this, if we combine this operator in several
formulas, we must define its value also for entries which are subsets. We
define:

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC, $a,b\in
P$ and $A,B$ non-empty subsets of $P$. Then

  1. (I)

$a\rightarrow b:=\operatorname{Max}\\{x\in P\mid L(a,x)\leq b\\}$,
---
$A\rightarrow B:=\operatorname{Max}\\{y\in P\mid L(x,y)\leq_{1}B\text{ for all
}x\in A\\}$.

  1. (C)

$a\odot b:=\operatorname{Max}L(a,b)$,
---
$A\odot B:=\operatorname{Max}\Lambda(A,B)$.

Of course, if $\mathbf{P}$ is a lattice then $a\odot b=a\wedge b$.

It is evident that $a\rightarrow 0=a^{0}$ as usual in intuitionistic logic.

In order to estimate how reasonable our definition of implication is we can
verify its relationship with conjunction. These two unsharp logical
connectives are related as follows:

  1. (AD)

$x\odot y\leq z$ if and only if $x\leq_{1}y\rightarrow z$

or, even more general,

$A\odot y\leq z\text{ if and only if }A\leq_{1}y\rightarrow z$

for every non-empty subset $A$ of $P$. This is a variant of adjointness of the
operators $\odot$ and $\rightarrow$. Hence the connectives introduced before
seem to be sound. We list some of their properties. It is evident that $\odot$
is commutative and $x\odot 1\approx 1\odot x\approx x$.

Moreover, from $x\rightarrow y=x\rightarrow y$ we infer by (AD)

$(x\rightarrow y)\odot x\leq_{1}y$

which is a kind of the Modus Ponens derivation rule in intuitionistic logic.
Namely, it says that the truth value of the proposition $y$ cannot be less
than the truth values of the propositions $x$ and $x\rightarrow y$ despite the
fact that $x\rightarrow y$ may consist of a number of propositions.

For the operator $\rightarrow$ we prove the following result.

######  Theorem 4.1.

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC, $a,b,c\in
P$ and $A,B$ non-empty subsets of $P$. Then the following holds:

  1. (i)

$a\rightarrow b$ is an antichain,

  2. (ii)

$b\leq_{1}a\rightarrow b$,

  3. (iii)

$a\leq_{1}(a\rightarrow b)\rightarrow b$,

  4. (iv)

$a\leq b$ implies $c\rightarrow a\leq_{1}c\rightarrow b$ and $b\rightarrow
c\leq_{1}a\rightarrow c$,

  5. (v)

$\Lambda(a,a\rightarrow b)=L(a,b)$,

  6. (vi)

$\Lambda(a\rightarrow b,b)=_{1}b$,

  7. (vii)

$1\rightarrow A=A$, especially $1\rightarrow a=a$

  8. (viii)

$A\rightarrow B=1$ if and only if $A\leq_{1}B$, especially $a\rightarrow b=1$
if and only if $a\leq b$,

  9. (ix)

$A\odot b\leq c$ if and only if $A\leq_{1}b\rightarrow c$,

  10. (x)

$a\odot(a\rightarrow b)=a\odot b$.

###### Proof.

  1. (i)

, (ii), (vii) and (ix) follow directly from the definition of $\rightarrow$.

  2. (iii)

follows from $L(x,a)=L(a,x)\leq b$ for all $x\in a\rightarrow b$

  3. (iv)

follows since $a\leq b$ implies

$\displaystyle\\{x\in P\mid L(c,x)\leq a\\}\subseteq\\{x\in P\mid L(c,x)\leq
b\\},$ $\displaystyle\\{x\in P\mid L(b,x)\leq c\\}\subseteq\\{x\in P\mid
L(a,x)\leq c\\}.$

  4. (v)

If $c\in\Lambda(a,a\rightarrow b)$ then there exists some $d\in a\rightarrow
b$ with $c\in L(a,d)$. Since $L(a,d)\leq b$ we have $c\in L(a,b)$. Conversely,
assume $c\in L(a,b)$. Since $L(a,b)\leq b$ there exists some $d\in
a\rightarrow b$ with $b\leq d$. Now $c\in
L(a,d)\subseteq\Lambda(a,a\rightarrow b)$.

  5. (vi)

Since $L(a,b)\leq b$ there exists some $c\in a\rightarrow b$ with $b\leq c$.
Now $b\in L(c,b)\subseteq\Lambda(a\rightarrow b,b)$ showing
$b\leq_{1}\Lambda(a\rightarrow b,b)$. Of course, $\Lambda(a\rightarrow
b,b)\leq_{1}b$.

  6. (viii)

The following are equivalent: $A\rightarrow B=1$, $L(x,1)\leq_{1}B$ for all
$x\in A$, $A\leq_{1}B$.

  7. (x)

According to (v) we have

$a\odot(a\rightarrow b)=\operatorname{Max}\Lambda(a,a\rightarrow
b)=\operatorname{Max}L(a,b)=a\odot b.$

∎

We can see that our operator $\rightarrow$ shares a lot of properties with the
connective implication in intuitionistic logic based on a Heyting algebra. In
particular, our $\rightarrow$ is antitone in the first and monotone in the
second entry.

######  Example 4.2.

Consider the bounded poset $(\\{0,a,b,c,d,e,1\\},\leq,0,1)$ visualized in Fig.
3:

$0$$c$$a$$b$$d$$e$$1$Fig. 3Bounded poset

The operator tables of $\rightarrow$ and $\odot$ are as follows:

$\begin{array}[]{l|l|l|l|l|l|l|l}\rightarrow&0&a&b&c&d&e&1\\\ \hline\cr
0&1&1&1&1&1&1&1\\\ \hline\cr a&bc&1&bc&bc&1&1&1\\\ \hline\cr
b&ac&ac&1&ac&1&1&1\\\ \hline\cr c&de&de&de&1&de&de&1\\\ \hline\cr
d&c&ac&bc&c&1&ce&1\\\ \hline\cr e&c&ac&bc&c&cd&1&1\\\ \hline\cr
1&0&a&b&c&d&e&1\end{array}\hskip
56.9055pt\begin{array}[]{l|l|l|l|l|l|l|l}\odot&0&a&b&c&d&e&1\\\ \hline\cr
0&0&0&0&0&0&0&0\\\ \hline\cr a&0&a&0&0&a&a&a\\\ \hline\cr b&0&0&b&0&b&b&b\\\
\hline\cr c&0&0&0&c&0&0&c\\\ \hline\cr d&0&a&b&0&d&ab&d\\\ \hline\cr
e&0&a&b&0&ab&e&e\\\ \hline\cr 1&0&a&b&c&d&e&1\end{array}$

Now we characterize the binary operator $\rightarrow$ in a similar way as it
was done for the unary operator 0 in Theorem 3.4.

######  Theorem 4.3.

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC and
$\rightarrow$ a binary operator on $P$. Then the following conditions (1) and
(2) are equivalent:

  1. (1)

$x\rightarrow y=\operatorname{Max}\\{z\in P\mid L(x,z)\leq y\\}$ for all
$x,y\in P$,

  2. (2)

the operator $\rightarrow\colon 2^{P}\times 2^{P}\rightarrow 2^{P}$
(restricted to $P\times P$) satisfies the following conditions for all
$x,y,z\in P$:

    1. (R1)

$x\rightarrow y$ is an antichain,

    2. (R2)

$L(x,z)\leq y$ implies $z\leq_{1}x\rightarrow y$,

    3. (R3)

$\Lambda(x,x\rightarrow y)=L(x,y)$.

###### Proof.

(1) $\Rightarrow$ (2):
This follows from Theorem 4.1.
(2) $\Rightarrow$ (1):
According to (R2) we have that $L(x,z)\leq y$ implies $z\leq_{1}x\rightarrow
y$. Conversely, if $z\leq_{1}x\rightarrow y$ then by (R3) we obtain

$L(x,z)\subseteq\Lambda(x,x\rightarrow y)=L(x,y)\leq y$

and hence $L(x,z)\leq y$. This shows that $L(x,z)\leq y$ is equivalent to
$z\leq_{1}x\rightarrow y$. We conclude

$\operatorname{Max}\\{z\in S\mid L(x,z)\leq y\\}=\operatorname{Max}\\{z\in
S\mid z\leq_{1}x\rightarrow y\\}=x\rightarrow y.$

The last equality can be seen as follows. Let $u\in\operatorname{Max}\\{z\in
S\mid z\leq_{1}x\rightarrow y\\}$. Then $u\leq_{1}x\rightarrow y$, hence there
exists some $v\in x\rightarrow y$ with $u\leq v$. We have
$v\leq_{1}x\rightarrow y$. Then $u<v$ would imply
$u\notin\operatorname{Max}\\{z\in S\mid z\leq_{1}x\rightarrow y\\}$, a
contradiction. This shows $u=v\in x\rightarrow y$. Conversely, assume $u\in
x\rightarrow y$. Then $u\leq_{1}x\rightarrow y$. If
$u\notin\operatorname{Max}\\{z\in S\mid z\leq_{1}x\rightarrow y\\}$ then there
would exist some $v\in S$ with $u<v\leq_{1}x\rightarrow y$ and hence there
would exist some $w\in x\rightarrow y$ with $u<v\leq w$ contradicting (R1).
This shows $u\in\operatorname{Max}\\{z\in S\mid z\leq_{1}x\rightarrow y\\}$. ∎

Let us note that using both (R2) and (R3) we can prove the adjointness (AD)
mentioned above.

######  Remark 4.4.

It is of some interest that the unsharp operator $\rightarrow$ can be
characterized by three exact and simple conditions in the language of posets
equipped with the operator $L$ of the lower cone.

##  5 Deductive systems

As mentioned in Section 4, we can involve in our logic the derivation rule
Modus Ponens. This rule is in fact closely related to the concept of a
deductive system. Hence we define:

######  Definition 5.1.

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC and
$\rightarrow$ defined by (I). A deductive system of $\mathbf{P}$ is a subset
$D$ of $2^{P}\setminus\\{\emptyset\\}$ satisfying the following conditions:

  1. (i)

$1\in D$,

  2. (ii)

if $x,y,z,u\in P$, $x\rightarrow y\in D$ and $(x\rightarrow
y)\rightarrow(z\rightarrow u)\in D$ then $z\rightarrow u\in D$,

  3. (iii)

if $x,y,z\in P$ and $x\rightarrow y,y\rightarrow x\in D$ then $(z\rightarrow
x)\rightarrow(z\rightarrow y)\in D$ and $(x\rightarrow
z)\rightarrow(y\rightarrow z)\in D$.

In the following we make use of the identities $x\odot 1\approx 1\odot
x\approx x$ and $1\rightarrow x\approx x$ (see Section 4).

######  Remark 5.2.

If $x\in D$, $y\in P$ and $x\rightarrow y\in D$ then according to (vii) of
Theorem 4.1 we have $1\rightarrow x=x\in D$ and $(1\rightarrow
x)\rightarrow(1\rightarrow y)=x\rightarrow y\in D$ and hence because of (ii)
of Definition 5.1 we get $y=1\rightarrow y\in D$. Therefore, $x\in D$ and
$x\rightarrow y\in D$ imply $y\in D$ which justifies the name “deductive
system” and illuminates the connection such systems with the derivation rule
Modus Ponens.

######  Example 5.3.

Consider the bounded poset $\mathbf{P}=(P,\leq,0,1)$ depicted in Fig. 4:

$0$$a$$b$$c$$d$$e$$1$Fig. 4Bounded poset

The operator table for $\rightarrow$ is as follows:

$\begin{array}[]{r|r|r|r|r|r|r|r}\rightarrow&0&a&b&c&d&e&1\\\ \hline\cr
0&1&1&1&1&1&1&1\\\ \hline\cr a&b&1&b&1&1&1&1\\\ \hline\cr b&c&c&1&c&1&1&1\\\
\hline\cr c&b&e&b&1&1&e&1\\\ \hline\cr d&0&a&b&c&1&e&1\\\ \hline\cr
e&0&c&b&c&d&1&1\\\ \hline\cr 1&0&a&b&c&d&e&1\end{array}$

We want to show that $D:=\\{d,e,1\\}$ is a deductive system of $\mathbf{P}$.
(The following considerations make heavy use of the operation table for
$\rightarrow$.) In order to make the proof of this statement short and clear
we define two subsets $A$ and $B$ of $P$ as follows:

$\displaystyle A$ $\displaystyle:=\\{(c,a),(c,e)\\}\cup D^{2}\cup\\{(x,y)\in
P^{2}\mid x\leq y\\},$ $\displaystyle B$ $\displaystyle:=\\{a,c\\}^{2}\cup
D^{2}\cup\\{(x,x)\mid x\in P\\}.$

Now let $x,y,z\in P$. Then we have

$\displaystyle x\rightarrow y\in D\text{ if and only if }(x,y)\in A,$
$\displaystyle x\rightarrow y,y\rightarrow x\in D\text{ if and only if
}(x,y)\in B,$ $\displaystyle 1\in D\text{ according to the definition of }D,$
$\displaystyle\text{if }x\in D\text{ and }(x,y)\in A\text{ then }y\in D,$
$\displaystyle\text{if }(x,y)\in B\text{ then }(z\rightarrow x,z\rightarrow
y),(x\rightarrow z,y\rightarrow z)\in B$

completing the proof that $D$ is a deductive system of $\mathbf{P}$.

Since in posets we do not have everywhere defined lattice operations join and
meet, we formulate a certain kind of compatibility in the following way.

######  Definition 5.4.

Let $(P,\leq,0,1)$ be a bounded poset satisfying the ACC and $\Phi$ be an
equivalence relation on $2^{P}\setminus\\{\emptyset\\}$. We say that $\Phi$
satisfies the substitution property with respect to $\odot$ if for all $x,y\in
P$ we have

$1\mathrel{\Phi}x\rightarrow y\hskip 5.69054pt\text{ implies }\hskip
5.69054ptx\odot 1\mathrel{\Phi}x\odot(x\rightarrow y).$

We say that $\Phi$ satisfies the substitution property with respect to
$\rightarrow$ if for all $x,y,z,u\in P$ we have

$\displaystyle x\mathrel{\Phi}y$ $\displaystyle\text{ implies }x\rightarrow
x\mathrel{\Phi}x\rightarrow y,$ $\displaystyle x\mathrel{\Phi}y$
$\displaystyle\text{ implies }(z\rightarrow x)\rightarrow(z\rightarrow
x)\mathrel{\Phi}(z\rightarrow x)\rightarrow(z\rightarrow y),$ $\displaystyle
x\mathrel{\Phi}y$ $\displaystyle\text{ implies }(x\rightarrow
z)\rightarrow(x\rightarrow z)\mathrel{\Phi}(x\rightarrow
z)\rightarrow(y\rightarrow z),$ $\displaystyle 1\mathrel{\Phi}x\rightarrow y$
$\displaystyle\text{ implies }1\rightarrow(z\rightarrow
u)\mathrel{\Phi}(x\rightarrow y)\rightarrow(z\rightarrow u).$

If an equivalence relation on $2^{P}\setminus\\{\emptyset\\}$ satisfies the
substitution property with respect to $\odot$ and $\rightarrow$ then we can
easily describe the relationship to its kernel.

######  Lemma 5.5.

Let $(P,\leq,0,1)$ be a bounded poset satisfying the ACC, $\Phi$ an
equivalence relation on $2^{P}\setminus\\{\emptyset\\}$ satisfying the
substitution property with respect to $\odot$ and $\rightarrow$ and $a,b\in
P$. Then $(a,b)\in\Phi$ if and only if $a\rightarrow b,b\rightarrow
a\in[1]\Phi$.

###### Proof.

If $(a,b)\in\Phi$ then

$\displaystyle a\rightarrow b\in[a\rightarrow a]\Phi=[1]\Phi,$ $\displaystyle
b\rightarrow a\in[b\rightarrow b]\Phi=[1]\Phi.$

If, conversely, $a\rightarrow b,b\rightarrow a\in[1]\Phi$ then according to
(x) of Theorem 4.1 we have

$a=a\odot 1\mathrel{\Phi}a\odot(a\rightarrow b)=a\odot b=b\odot
a=b\odot(b\rightarrow a)\mathrel{\Phi}b\odot 1=b.$

∎

When studying congruences in varieties of algebras, an important congruence
property is the so-called weak regularity. It means that if an algebra in
question has a constant $1$ and if for two of its congruences $\Phi$ and
$\Psi$ we have $[1]\Phi=[1]\Psi$ then $\Phi=\Psi$, see e.g. [5]. Surprisingly,
we obtain a similar result for posets and equivalence relations having the
substitution property with respect to $\odot$ and $\rightarrow$. In fact, this
is a consequence of Lemma 5.5.

######  Corollary 5.6.

If $(P,\leq,0,1)$ is a bounded poset satisfying the ACC, $\Phi,\Psi$ are
equivalence relations on $2^{P}\setminus\\{\emptyset\\}$ satisfying the
substitution property with respect to $\odot$ and $\rightarrow$ and
$[1]\Phi=[1]\Psi$ then $\Phi\cap P^{2}=\Psi\cap P^{2}$.

For varieties of algebras, the mentioned weak regularity was characterized by
B. Csákány, see e.g. [5] by means of certain binary terms satisfying a simple
condition. It is of some interest that such a binary term can be derived also
for posets.

######  Proposition 5.7.

Let $(P,\leq,0,1)$ be a bounded poset satisfying the ACC, put
$t(x,y):=(x\rightarrow y)\odot(y\rightarrow x)$ for all $x,y\in P$ and let
$a,b\in P$. Then $t(a,b)=1$ if and only if $a=b$.

###### Proof.

According to (viii) of Theorem 4.1 the following are equivalent:

$\displaystyle t(a,b)$ $\displaystyle=1,$ $\displaystyle(a\rightarrow
b)\odot(b\rightarrow a)$ $\displaystyle=1,$
$\displaystyle\operatorname{Max}\Lambda(a\rightarrow b,b\rightarrow a)$
$\displaystyle=1,$ $\displaystyle 1$ $\displaystyle\in\Lambda(a\rightarrow
b,b\rightarrow a),$ $\displaystyle\text{there exists some }x\in a\rightarrow
b\text{ and some }y\in b\rightarrow a\text{ with }1$ $\displaystyle\in
L(x,y),$ $\displaystyle\text{there exists some }x\in a\rightarrow b\text{ and
some }y\in b\rightarrow a\text{ with }x$ $\displaystyle=y=1,$ $\displaystyle
1$ $\displaystyle\in(a\rightarrow b)\cap(b\rightarrow a),$ $\displaystyle
a\rightarrow b$ $\displaystyle=b\rightarrow a=1,$ $\displaystyle a$
$\displaystyle\leq b\leq a,$ $\displaystyle a$ $\displaystyle=b.$

∎

We are going to show that the kernel of an equivalence relation satisfying the
substitution property with respect to $\odot$ and $\rightarrow$ is just a
deductive system.

######  Theorem 5.8.

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC and $\Phi$
an equivalence relation on $2^{P}\setminus\\{\emptyset\\}$ satisfying the
substitution property with respect to $\odot$ and $\rightarrow$. Then
$[1]\Phi$ is a deductive system of $\mathbf{P}$.

###### Proof.

Let $a,b,c,d\in P$.

  1. (i)

This is clear.

  2. (ii)

If $a\rightarrow b,(a\rightarrow b)\rightarrow(c\rightarrow d)\in[1]\Phi$ then
according to (vii) of Theorem 4.1 we have

$c\rightarrow d=1\rightarrow(c\rightarrow d)\in[(a\rightarrow
b)\rightarrow(c\rightarrow d)]\Phi=[1]\Phi.$

  3. (iii)

If $a\rightarrow b,b\rightarrow a\in[1]\Phi$ then $(a,b)\in\Phi$ according to
Lemma 5.5 and hence

$\displaystyle(c\rightarrow a)\rightarrow(c\rightarrow b)$
$\displaystyle\in[(c\rightarrow a)\rightarrow(c\rightarrow a)]\Phi=[1]\Phi,$
$\displaystyle(a\rightarrow c)\rightarrow(b\rightarrow c)$
$\displaystyle\in[(a\rightarrow c)\rightarrow(a\rightarrow c)]\Phi=[1]\Phi.$

∎

The question if a given deductive system $D$ on a bounded poset $(P,\leq,0,1)$
satisfying the ACC induces an equivalence relation on
$2^{P}\setminus\\{\emptyset\\}$ with kernel $D\cap P$ having a property
similar to the substitution property with respect to $\rightarrow$ is answered
in the next result. At first, we define the relation induced by $D$.

######  Definition 5.9.

For every bounded poset $(P,\leq,0,1)$ satisfying the ACC and every subset $E$
of $2^{P}\setminus\\{\emptyset\\}$ define a binary relation $\Theta(E)$ on
$2^{P}\setminus\\{\emptyset\\}$ as follows:

$(A,B)\in\Theta(E)\text{ if and only if }A\rightarrow B,B\rightarrow A\in E$

($A,B$ non-empty subsets of $P$). We call $\Theta(E)$ the relation induced by
$E$.

In Theorem 5.8 we proved that for every equivalence relation $\Phi$ on
$2^{P}\setminus\\{\emptyset\\}$ satisfying the substitution property with
respect to $\odot$ and $\rightarrow$, its kernel $[1]\Phi$ is a deductive
system of $\mathbf{P}$. The next theorem shows that there holds some converse
version of this result if we consider the restriction of the relation induced
by a deductive system of $\mathbf{P}$ to the base set $P$.

######  Theorem 5.10.

Let $\mathbf{P}=(P,\leq,0,1)$ be a bounded poset satisfying the ACC and $D$ a
deductive system of $\mathbf{P}$. Then the following hold:

  1. (i)

$\Theta(D)\cap P^{2}$ is an equivalence relation on $P$,

  2. (ii)

$[1]\big{(}\Theta(D)\cap P^{2}\big{)}=D\cap P$,

  3. (iii)

if $x,y,z\in P$ and $(x,y)\in\Theta(D)$ then $(z\rightarrow x,z\rightarrow
y)\in\Theta(D)$ and $(x\rightarrow z,y\rightarrow z)\in\Theta(D)$.

###### Proof.

Let $a,b,c\in P$.

  1. (i)

Evidently, $\Theta(D)$ is reflexive and symmetric. If
$(a,b),(b,c)\in\Theta(D)$ then

$b\rightarrow c,(b\rightarrow c)\rightarrow(a\rightarrow c),c\rightarrow
b,(c\rightarrow b)\rightarrow(c\rightarrow a)\in D$

and hence $a\rightarrow c,c\rightarrow a\in D$, i.e. $(a,c)\in\Theta(D)$. This
shows that $\Theta(D)$ is transitive and therefore an equivalence relation on
$P$.

  2. (ii)

The following are equivalent: $a\in[1]\big{(}\Theta(D)\big{)}$; $a\rightarrow
1,1\rightarrow a\in D$; $1,a\in D$; $a\in D$.

  3. (iii)

follows from Definition 5.1.

∎

######  Example 5.11.

For the deductive system $D$ from Example 5.3 we have

$\Theta(D)=\\{a,c\\}^{2}\cup D^{2}\cup\\{(x,x)\mid x\in P\\}.$

## References

  * [1] L. E. J. Brouwer, De onbetrouwbaarheid der logische principes. Tijdschrift Wijsbegeerte 2 (1908), 152–158.
  * [2] L. E. J. Brouwer, Intuitionism and formalism. Bull. Amer. Math. Soc. 20 (1913), 81–96.
  * [3] I. Chajda, An extension of relative pseudocomplementation to non-distributive lattices. Acta Sci. Math. (Szeged) 69 (2003), 491–496.
  * [4] I. Chajda, Pseudocomplemented and Stone posets. Acta Univ. Palack. Olomuc. Fac. Rerum Natur. Math. 51 (2012), 29–34.
  * [5] I. Chajda, G. Eigenthaler and H. Länger, Congruence Classes in Universal Algebra. Heldermann, Lemgo 2012. ISBN 3-88538-226-1.
  * [6] I. Chajda and H. Länger, Implication in finite posets with pseudocomplemented sections. Soft Computing 26 (2022), 5945–5953.
  * [7] I. Chajda and H. Länger, The logic of orthomodular posets of finite height. Log. J. IGPL 30 (2022), 143–154.
  * [8] I. Chajda and H. Länger, Operator residuation in orthomodular posets of finite height. Fuzzy Sets and Systems 467 (2023), 108589 (11 pp.).
  * [9] I. Chajda and H. Länger, Algebraic structures formalizing the logic with unsharp implication and negation. Logic J. IGPL (submitted). http://arxiv.org/abs/2301.02205.
  * [10] I. Chajda, H. Länger and J. Paseka, Sectionally pseudocomplemented posets. Order 38 (2021), 527–546.
  * [11] P. D. Finch, On orthomodular posets. J. Austral. Math. Soc. 11 (1970), 57–62.
  * [12] O. Frink, Pseudo-complements in semi-lattices. Duke Math. J. 29 (1962), 505–514.
  * [13] R. Giuntini and H. Greuling, Toward a formal language for unsharp properties. Found. Phys. 19 (1989), 931–945.
  * [14] A. Heyting, Die formalen Regeln der intuitionistischen Logik. I. Sitzungsberichte Akad. Berlin 1930, 42–56.
  * [15] P. Köhler, Brouwerian semilattices: the lattice of total subalgebras. Banach Center Publ. 9 (1982), 47–56.
  * [16] A. Monteiro, Axiomes indépendants pour les algèbres de Brouwer. Rev. Un. Mat. Argentina 17 (1955), 149–160.
  * [17] L. Monteiro, Les algèbres de Heyting et de Lukasiewicz trivalentes. Notre Dame J. Formal Logic 11 (1970), 453–466.
  * [18] P. Pták and S. Pulmannová, Orthomodular Structures as Quantum Logics. Kluwer, Dordrecht 1991. ISBN 0-7923-1207-4.

Authors’ addresses:

Ivan Chajda
Palacký University Olomouc
Faculty of Science
Department of Algebra and Geometry
17\. listopadu 12
771 46 Olomouc
Czech Republic
<EMAIL_ADDRESS>
Helmut Länger
TU Wien
Faculty of Mathematics and Geoinformation
Institute of Discrete Mathematics and Geometry
Wiedner Hauptstraße 8-10
1040 Vienna
Austria, and
Palacký University Olomouc
Faculty of Science
Department of Algebra and Geometry
17\. listopadu 12
771 46 Olomouc
Czech Republic
<EMAIL_ADDRESS>