Date: Wed, 24 Mar 1999 11:18:12 -0700 From: Randall Holmes Subject: FOM: second order logic, reference of mathematical language I suggest that one of the difficulties in the second-order logic thread is that the participants are talking past each other. It would be nice to get out of this state and figure out what the real concerns underlying this dispute are. Thesis 1: I think that the issues here have nothing to do with the actual practice of mathematics. I agree with Simpson and Friedman that the way to do our business is to work in a formalization which looks like first-order ZFC, using definitions which can be phrased in the language of first-order ZFC, and prove theorems from that as a starting point (I don't see any reason to think that any others who might agree with me would think differently). Under some circumstances, it is necessary to move to a stronger formal theory; there is a natural (though not formalizable) way of getting stronger and stronger extensions of ZFC in which we have confidence. The questions are in the area of f.o.m., not of mathematics. Thesis 2: The questions have to do with the motivation of definitions of mathematical concepts. One side of the debate sees a problem with them which the other does not. The problem is perhaps philosophical rather than genuinely mathematical (but nonetheless falls within the scope of f.o.m.) Mayberry and I both hold the view that the first-order theory ZFC is the theory of the class of models of ZFC (just as group theory is the theory of structures which satisfy the group axioms). On this basis, first-order ZFC cannot express the notion "the set of natural numbers", because there is no term in the language of ZFC which will always define the set of natural numbers. On the other hand, in any model of second-order ZFC (this is a far stronger theory than is needed!) the usual definition of "the set of natural numbers" will refer to an implementation of the set of natural numbers. Thus I would say that second-order ZFC allows us to express the notion "the set of natural numbers" and first-order ZFC does not. This usage of the word "express" may be eccentric, but I should now have made it clear what I mean by it. The effect of this on mathematical practice is nil, for the following reasons (already belaboured in this thread): we can't do anything in second-order ZFC without adopting a partial formalization (a complete formalization is impossible). The formalized theory will include first-order ZFC (actually, the natural formalization will give the slightly stronger Kelley-Morse set theory). I don't think Simpson or Friedman would regard an insistence on working in Kelley-Morse set theory as more than a mild eccentricity! In any event, the formalization will be a first-order theory fitting in the hierarchy of natural extensions of ZFC. In this framework, it is natural to study models of first-order ZFC (or of Kelley-Morse set theory) both for their own intrinsic interest and because this study allows one to look at alternative possible situations which might hold in the ambient second-order ZFC. So the practice of studying consistency and independence results makes perfect sense from the "second-order ZFC" standpoint; the only difference is one of philosophical perspective. No change in the actual mathematics being pursued is to be expected! I suppose that it is possible that the mathematician with the second-order standpoint might become convinced through his study of consistency and independence results that he ought to adopt some additional axioms in his second-order theory -- but a mathematician taking a different approach might adopt additional axioms for reasons which would look much the same on the surface! The advantages of such an approach (if any) cannot lie in the actual mathematics being done, because the mathematics being done (even re consistency and independence results) will be the same. The point for me is that the approach via second-order logic (be it logic or not -- that's another terminological argument) allows the exact definition of basic mathematical concepts in topic-neutral terms (something like the logicist program). This is a philosophical issue (but one proper to f.o.m.); it may be disputed whether it is possible or desirable, and I would be interested in discussing its value or lack thereof. There is no claim (on my part at least) that there should be any fundamental change in mathematical practice. Note that the argument about the mathematical or topic-neutral character of second-order logic is relevant here. I have already said something about this: second-order quantifiers can be taken to range over predicates or properties rather than the specifically mathematical "sets". Of course, the legitimacy of this proceeding is open to debate. The question of what the natural numbers (for example) are, or what we mean when we talk about the natural numbers (or other mathematical structures) is certainly a legitimate topic for f.o.m. (though not necessarily of great interest to a working mathematician). Incidentally, questions like this should also be important in mathematical pedagogy. (An interesting incidental side effect of an approach using second-order logic is that it makes the claim of ZFC to be the proper foundation (as opposed to alternatives like Ackermann set theory or NFU) much stronger. The comprehension axioms of ZFC have elegant second-order analogues, while the comprehension axioms of Ackermann set theory or NFU are much harder to motivate in second-order terms; there is a nice second-order version of NFU which I have studied, but it is extremely strong! This isn't directly relevant, but there have been side comments on my fondness for NFU. As a first-order formalism, NFU is really not bad at all; I'm doing theorem proving work using stratified lambda-calculus (theory of functions rather than sets) and it appears to be quite convenient to use this as a "higher-order logic" (it is not a true higher-order logic)). So I would like to hear from other parties. How do we define "the set of natural numbers" in ZFC (this is not a request for the text of the definition!), and what is the relation of this definition to our pre-formal notions? I do not understand the legitimacy of a definition in a formal language prior to the adoption of axioms or rules of inference -- or at least for the sake of this argument I don't. The only way I can understand this proceeding involves the implicit interpretation of the primitives of first-order ZFC as having the meanings which they have in second-order ZFC. But I'm not going to presuppose that this is what is happening in the heads of other mathematicians. And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes the gates of Cantor's paradise, that the | Boise State U. (disavows all) slow-witted and the deliberately obtuse might | holmes@math.idbsu.edu not glimpse the wonders therein. | http://math.idbsu.edu/~holmes