Propositional calculus under adjointness

We develop a formal system for the class of all implications A and conjunctions K, on partially ordered sets (L, less than or equal to) with top elements 1, such that A and K are related by adjointness and they satisfy the neutrality principle (that is, 1 is their left identity element). We call the resulting logic propositional calculus under adjointness, abbreviated AdJPC. Most algebraic theorems on those (L, less than or equal to), A and K are inequalities in the posets (L, less than or equal to) of truth values. In consequence, we have to find means for abstracting inequalities within syntax; which must be free from partial truth values. This is achieved by employing a further, implication-like adjoint H of A and K, whereby the partial order of (L, less than or equal to) coincides with the binary relation H(.,.) = 1. Accordingly, the semantical domain for AdjPC should become the class of all such quintuples (L,less than or equal to ,A,K,H), which we call adjointness algebras. Our axiom scheme for AdjPC features seven axioms. However, it may be the case that no finite set of axioms can complete AdjPC if inference is carried out by means of modus ponens (MP) alone. This is because AdjPC is too general; it lacks some basic theorems of the more restricted logics (such as residuated logic and intuitionistic logic). As a result, we have to adopt four inference rules for AdjPC; namely, MP and three bits of the substitution theorem. We deduce enough theorems and inferences in AdjPC to delineate its basic structure. This enables us to establish the completeness of AdjPC for the semantical domain of adjointness algebras; by means of a quotient-algebra structure (a Lindenbaum type of algebra). We also show how certain models can help disprove some incorrect inferences in AdjPC. We end by developing complete syntax (with fewer axioms and inference rules) for the smaller semantical domain of all adjointness algebras whose implications satisfy the exchange principle. (C) 2002 Elsevier Science B.V. All rights reserved.