  It is easy to prove certain facts about these operations directly from the adjunctions. Consider, for instance, implication. Let \(Z = X.\) Then we get at the numerator that \(Y \wedge X \le X\), which is always true in a poset (as is easily verified). Hence, \(Y \le X \Rightarrow X\) is also true for all \(Y\) and this is only possible if \(X \Rightarrow X = \top\), the top element of the lattice. Not only can logical operations be described as adjoints, but they naturally arise as adjoints to basic operations. In fact, adjoints can be used to define various structures, distributive lattices, Heyting algebras, Boolean algebras, etc. (See Wood, 2004.) It should be clear from the simple foregoing example how the formalism of adjointness can be used to give syntactic presentations of various logical theories. Furthermore, and this is a key element, the standard universal and existential quantifiers can be shown to be arising as adjoints to the operation of substitution. Thus, quantifiers are on a par with the other logical operations, in sharp contrast with the other algebraic approaches to logic. (See, for instance Awodey 1996 or Mac Lane &amp; Moerdijk 1992.) More generally, Lawvere showed how syntax and semantics are related by adjoint functors. (See Lawvere 1969b.)