Oops, I forgot about hat's being tilde'd by bitnet or whoever. The following replaces hat by backquote, in case you haven't sent it off yet. Since quote is only used on 0 and 1, which are their own converse, no confusion should result. There are three tilde's at the end of the message that will turn into c's, but since those tilde's denote a congruence the c can be read as c for congruence (cuch cerendipity!) ORDERED ALGEBRAS Vaughan Pratt Stanford Univ. June 20, 1990 I'd like to ask the group what it knows about the following notion, which out of ignorance of the standard term if any I will here call an ordered algebra. Which is more fundamental, = or < ? Frequency of usage gives little clue, both are in heavy use. When x+y (disjunction, sup, max) or xy (conjunction, inf, min) is in the language we can take = as basic and view x<y as merely an abbreviation for x+y = y, or x = xy. However what if x+y or xy is in the language solely so that we *can* so express x<y as an equation? This is the situation we find in the theory of residuated posets, where x\y and x/y can be defined inequationally via x;(x\y) < y < x\(x;y) (y/x);x < y < (y;x)/x without reference to x+y or xy other than that implicit in the expansion of x<y to x+y=y. Having so defined residuation we may, based on the axioms in Judith Ng's thesis (UCB Math, 1984), proceed to define reflexive transitive closure x* as the monotone operation satisfying 1' < x* (x* is reflexive) x*;x* < x* (x* is transitive) x < x* (x\x)* = x\x (pure induction, or "iteration preserves invariance") all in terms of equations that continue to make no other reference to x+y or xy beyond that implied by reading x<y as x+y=y. (Incidentally it may be verified, see e.g. the section on star in my article in LNCS 425, that x* is implicitly defined, i.e. uniquely determined as an operation on a residuated poset, by these inequations.) These considerations indicate a need for a notion along the following lines. An ordered algebra is a poset (A,<) equipped with (m,n)-ary operations f: (A,>)?m x (A,<)?n -> (A,<), where (A,>) denotes the order dual of A. We say that such a function f is of arity (m,n), having m antimonotone arguments and n monotone arguments. The application of such an f to its m+n arguments is written f(x1,...,xm;y1,...,yn). For example the signature of a relation algebra (R, +, ., -, ->, #, ;, `, 0, 1, 0', 1') would be (0,2),(0,2),(1,0),(1,1),(2,2),(0,2),(0,1),(0,0),(0,0),(0,0),(0,0). That is, disjunction x+y and conjunction xy are of arity (0,2) and hence monotone in both arguments, negation x- of arity (1,0) would be antimonotone in its one argument, material (Boolean) implication x->y of arity (1,1) would be antimonotone in one argument and monotone in the other, exclusive-or x#y would have to be viewed as a quaternary (2,2)-ary operation rather than a binary operation, relative product x;y of arity (0,2) would be monotone in both arguments, converse x` of arity (0,1) would be monotone in its one argument, and the constants 0,1,0',1' are of course all of arity (0,0). Specifying the signature takes care of the otherwise awkward question of how to axiomatize monotonicity itself without using Horn clauses or x+y; it simply becomes part of the syntax. The notion of equational theory is now replaced by that of an inequational theory, defined in the obvious way, which the following examples should make more obvious. Example 1. Semilattices. A semilattice (X,+) consists of just one operation x+y, of arity (0,2), satisfying the following inequations. x < x + y y < x + y x + x < x The first two inequations say that x+y is an upper bound on x and y, and the third says that it is the least such (easy exercise). The signature (0,2) and these three inequations constitute the entire definition of "semilattice." We may further equip it with constants 0 and 1, each of arity (0,0), defined via: 0 < x x < 1 Example 2. Ordered monoids. An ordered monoid (X,;,1') consists of an operation x;y of arity (0,2) and a constant 1' of arity (0,0) satisfying x;(y;z) = (x;y);z x;1' = x = 1';x We read x=y as abbreviating the pair of inequations x<y<x. (But we could shorten the four inequations of x;1' = x = 1';x to three via x < x;1' < 1';x < x.) We may expand an ordered monoid to a residuated poset by adding right and/or left residuation, both of arity (1,1). The official syntax calls for \(x;y) and /(x;y) in order to indicate that it is antimonotone in x and monotone in y, but we write these standardly as x\y and y/x respectively, remembering the relationship to the official syntax in order to keep track of the arity. The defining inequations are: x;(x\y) < y < x\(x;y) (y/x);x < y < (y;x)/x Had we thought earlier to introduce converse x`, of arity (0,1), satisfying x`` = x (x;y)` = y`;x` we could have dispensed with one of the two equations for 1', and done away with y/x altogether by treating it as just an abbreviation for (x`\y`)`. And we could weaken x;(y;z) = (x;y);z to x;(y;z) < (x;y);z. We may further extend this algebra to include star (ancestral, reflexive transitive closure) exactly as defined in the introduction. Exercise. Define a residuated unital semilattice with converse and star to be the combination of examples 1 and 2. Show in such: x;(y+z) = x;y + x;z (x+y);z = x;z + y;z x;0 = 0 = 0;x (x+y)` = x`+y` x;(y;x)* = (x;y)*;x (x+y)* = (x*;y*)* Now for my main questions. 1. Does this notion of ordered algebra occur in the equational logic or universal algebra literature? 2. What does that literature or any other literature (e.g. the categorical literature) have to say about the following? (i) Semantic completeness. What is the analog for ordered varieties of Birkhoff's HSP theorem for varieties? (ii) Syntactic completeness. If an equational theory Th(V) is exactly a substitutive congruence on an algebra of terms over a set V of variables, what exactly is an inequational theory on an ordered algebra of terms? (Call a congruence ^ *substitutive* when u^v implies s(u)^s(v) for any substitution s, i.e. any endomorphism s:T(V)->T(V).) (iii),(iv) Ditto for ordered quasivarieties. Vaughan Pratt