The logic of tied implications, part 2: Syntax

An implication operator A is said to be tied if there is a binary operation T that ties A; that is, the identity A(a,A(b,z))=A(T(a,b),z) holds for all a,b,z. We aim at the construction of a complete predicate logic for prelinear tied adjointness algebras. We realize this in three steps. In the first step, we establish a propositional calculus AdjTPC, complete for the class of all tied adjointness algebras on partially ordered sets; without prelinearity and ignoring the lattice operations. For that we supply a Hilbert system based on seven axioms and one deduction rule (modus ponens). In the second and third steps, we extend AdjTPC to propositional and predicate calculi; complete for prelinear tied adjointness algebras. We apply a duality principle, due to Morsi, in all three calculi; through which we manage to cut down the number of proofs.