Propositional calculus for adjointness lattices

Abstract

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.