Propositional calculus for adjointness lattices

Recently, Morsi has developed a complete syntax for the class of all
adjointness algebras $\left( L,\leq ,A,K,H\right) $. There, $\left( L,\leq
\right) $ is a partially ordered set with top element $1$, $K$ is a
conjunction on $\left( L,\leq \right) $ for which $1$ is a left identity
element, and the two implication-like binary operations $A$ and $H$ on $L$
are adjoints of $K$.

In this paper, we extend that formal system to one for the class $ADJL$ of
all 9-tuples $\left( L,\leq ,1,0,A,K,H,\wedge ,\vee \right) $, called \emph{%
adjointness lattices}; in each of which $\left( L,\leq ,1,0,\wedge ,\vee
\right) $ is a bounded lattice, and $\left( L,\leq ,A,K,H\right) $ is an
adjointness algebra. We call it \emph{Propositional Calculus for Adjointness
Lattices}, abbreviated $AdjLPC$. Our axiom scheme for $AdjLPC$ features four
inference rules and thirteen axioms. We deduce enough theorems and
inferences in $AdjLPC$ to establish its completeness for $ADJL$; by means of
a quotient-algebra structure (a Lindenbaum type of algebra). We study two
negation-like unary operations in an adjointness lattice, defined by means
of $0$ together with $A$ and $H$. We end by developing complete syntax for
all adjointness lattices whose implications are $S$-type implications.