Hi, I gave a correct syntax for lex logic, and a completeness theorem, in "Left exact logic", Journal of Pure and Applied Algebra, 41 (1986) 63-66. The point is, that you must be able assert existence (that is, existence of a value in some equalizer sort) conditional on equations. So you need sequents with equations on the the lefthand side. And of course you could do it all as a term logic with only conjunctions of equations as formulas, or with just atomic formulas and sequences with lists of atomic formulas on both sides. In fact, you can radically shorten the lefthand sides by a trick I explain in exercises 21-23 of chapter 20 of ELEMENTARY CATEGORIES, ELEMENTARY TOPOSES. the point of that is that, by looking at the righthand side, you can tell what equations are required as presuppositions, and suppress them. best, Colin 17-Dec-2002 19:04:30 -0400,1619;000000000001-00000000