On Fri, Mar 14, 2008 at 1:26 PM, Thomas Streicher <streicher@mathematik.tu-darmstadt.de> wrote:
Set theorists insist on formulating set theory in first order logic and therefore must formulate replacement as a schema since they can't quantify over families of sets (the ambient category is a logos or Heyting category but not cartesian closed). If they decided to formulate set theory within higher order logic they presumably would have formulated replacement not as a schema (see Bill's remarks on Goedel and Kreisel's suggestions).
I have read that Zermelo always insisted on a second-order interpretation of his axioms; in particular as regards his notion of a "definite" property. It was only later mathematicians who decided that "definite" should mean "first-order". Also, the perfectly classical von Neumann-Bernays-Godel set theory, which set theorists know about and make use of, does use classes to avoid axiom schemas in the same way that AST does, thereby obtaining a finitely axiomatizable theory equivalent to ZFC. Having said that, I will now dive off the deep end into what seems likely to be very hot water (-:, and say that it seems to me that "higher-order logic" is really first-order set theory in disguise. The interpretation of "higher-order quantifiers" ranging over "sets of blah objects" (or "predicates" or "classes") only makes sense with respect to an external set theory that specifies what counts as a "set"---or by introducing a new type called "set of blah objects", which brings you back into to a first-order set theory. I think this is more evident now than it was to Zermelo, now that we have, say, the independence of CH before our eyes to convince us that the extension of the notion of "subset of a given set" is not uniquely determined by the idea of "set"---at least, not obviously---and requires some sort of theory of sets to specify what it means. I think that this is one reason that modern set theorists usually stick to first-order logic. This is not to dispute the value and power of what is normally called second-order and higher-order logic. In particular, what is called higher-order logic is essential to topos theory and AST, for which I have a great appreciation and respect. But I think it does show that if you get down to the root, all mathematics is actually done in first-order logic. For instance, the "higher-order" formulation of replacement that you advocate is still part of a *first-order* theory of sets and classes (AST). Now I'm not saying there's anything wrong with that! It certainly gives rise to interesting, powerful, and useful mathematics, which I don't understand nearly as well as I would like to. But I don't think it is necessarily indicative of blindness on the part of set theorists that they choose to include only sets in their first-order logic. There is something about introducing classes as first-class objects that makes some of us slightly uneasy: what is it that distinguishes a set from a class? What exactly prevents us from talking about classes of classes? Why did we draw an arbitrary line at some point and say "any collection of things bigger than *this* is a class", and forbid ourselves from doing otherwise intuitive things to them like taking power objects and exponentials? Why shouldn't set theory be the *universal* theory of "collections of things"? Of course, it is likely that I am quite wrong, so I await correction. (-: Best, Mike