The first solution to the "logic of cartesian categories" (I insist that Descartes invented equalizers as much as he invented products) presented itself with the introduction of essentially algebraic theories in 1971. It's an exercise. But it was always clear to me -- long before 1971 --that unique existential quantification was the central feature. (Yes, of course you can avoid it in the same way you can avoid ordinary existential quantification. Skolem taught us that.) There's no question one can assert unique existentials using finite limits. (As a sample: given a couple of binary predicates P on objects A,B and Q on objects B,C (modeled by maps from P to A and B and from Q to B and C) the assertion that for all a,b such that aPb there's a unique c such bQc is equivalent to the assertion that the map Pullback[P -> B, Q -> B] -> P is an iso. The rules of inference for unique existential quantification is what I saw as the central question. I wrote in Cartesian Logic: Twenty-five years ago this writer started listing these rules. Their remarkable inelegance caused him to conclude that he was staring at one of the very reasons for category theory. The notion of a cartesian category is much simpler than that of cartesian syntax. The language of cartesian categories has permeated mathematics as a whole, even among those who are convinced that there is nothing worth noting in the theory of categories (the usefulness of a language does not, in fact, imply the usefulness of its associated theory) and there is no chance that cartesian syntax is going to do any such thing....The particular impetus that propelled the present effort arose from the necessity [in an attempt to formalize the semantics of "logical programming"] of getting a handle on the process of adjoining generic subobjects to objects in cartesian categories. [The 25 years ago referred to the very first NY topos seminar. The rules at that point were horrendous.] Yes, once the solution for the generic subobject is stated one doesn't need cartesian logic. But it's a useful tool to find the solution. So here's a challenge. Take an arbitrary cartesian category and an object C therein. Now adjoin a generic category structure to the object C (use the one-sorted "pure category" theory). What are the objects? Try it just for the free cartesian category on C, in other words, what's the free cartesian category on a category-object? What are its objects? And harder: what are its maps? 18-Dec-2002 14:45:54 -0400,2705;000000000001-00000000