Date: Tue, 23 Mar 1999 13:24:42 -0700 From: Randall Holmes Subject: FOM: denunciation of formalized mathematics? Simpson said: Randall Holmes 18 Mar 1999 16:00:03 disputes the well known fact (*): mathematics can be formalized in formal systems based on first-order logic such as ZFC. I find this position remarkable. The well known fact (*), which Holmes disputes, is of course well known to be crucial for current f.o.m. research. I know of no scientific reason why Holmes would want to undercut (*), especially since Holmes himself has credentials as an f.o.m. researcher. Holmes replies: I find the whole tenor of your response(s) remarkable. When you find your interpretation of what your respondent in a debate is saying _too_ remarkable, it might be profitable to check your premises (as to what your "opponent" means); some of them may be wrong. What I'm saying is that mathematics is not _completely_ formalized by ZFC. You admit this yourself later. I am certainly not an opponent of formalized mathematics. A large part of my work is in computer assisted theorem proving, which would be a really remarkable pursuit if I did not value formalized mathematics!!! The context is: (earlier message from Holmes) In this note, I discuss Simpson's claim that "mathematics can be formalized in ZFC" This is a very common claim; I often make it myself (more often I claim that mathematics can be formalized in strong extensions of NFU, a claim to which the same strictures apply that I apply below to the commoner claim about ZFC). It is true in a certain practical sense. But I think that there are also good grounds (which most of us know about, though I will tiresomely summarize them below) for the contrary claim that "arithmetic (and so most of mathematics) cannot be formalized at all". (end of earlier message from Holmes) A complete reading of the message would make it clear that I am not issuing a blanket denunciation of formalized mathematics. Even a reading of the excerpt should suggest this. The specific, and well-known point which I make in the rest of the excerpted post is that first-order ZFC (or any first-order theory) (in a sense which I discuss further below) is not adequate for the definition of the natural numbers (in a precise sense which I make clear below, and made clear in that post). This is an uncontroversial mathematical fact. I also make the philosophical point, with which one may agree or disagree, that the informal standpoint from which one starts to understand mathematics is never completely captured or replaced by any formal system; this is not a denial that formalizations of mathematics are important and useful. A serious discussion of such philosophical issues in f.o.m. is what I would really like to hear. Simpson said: In his subsequent posting of 18 Mar 1999 16:25:52, Holmes backs down a little bit: > I must hasten to add that ... first-order logic does capture a > (nearly) universal standard of formalized proof. Holmes replies: I wasn't "backing down" at all. This is an essential part of my position. You seem to think that because I recognize the importance of second-order logic for definition I do not recognize the crucial importance of first-order logic for inference and cannot avail myself of first-order tools. I exhibit this remark of Simpson: However, he doesn't back down from his denunciation of formalized mathematics. I respond, for the record: I did not issue a denunciation of formalized mathematics. If anyone other than Simpson thinks that I was denouncing formalized mathematics, please tell me; such was far from my intention. Simpson asserted: When well known facts are in dispute, somebody needs to stand up and be counted. I want to put on record that I disagree with Holmes and reject his rejection of the idea of formalized mathematics. Holmes comments: I want to put it on the record (as I have already) that I do not reject the idea of formalized mathematics. I do reject the idea that first-order ZFC, all by itself, constitutes a complete formalization of the fundamentals we need for f.o.m. It is seriously flawed, _if considered as a foundation all by itself_ (in my opinion). Arguments could be given against the position that these flaws are flaws at all, or against the position that these flaws, if they are flaws, are avoidable or worth avoiding. Simpson has not attempted this; he simply continues to misunderstand me. The reasons why Simpson steadfastly refuses to understand my argument, in which I use well-known facts, just as he does, are a complete mystery to me, especially as this argument is not especially novel. For the record: if one's entire aim is to prove theorems whose usual interpretation captures (almost all of) classical mathematics, then first order ZFC is completely adequate as a foundation of mathematics. This is not disputed by me, and I think that Simpson wants to defend (without ever quite saying it) the position that this is all that matters. It is not, in my opinion, all that matters for philosophically adequate foundations of mathematics. I can imagine philosophical viewpoints from which my additional concerns would not be significant; such positions have been clearly stated by others on this list. Simpson has not clearly stated such a position. Simpson said: The truth is that there is an extremely important sense in which ZFC *does* allow us to refer to the natural numbers and other familiar structures and *does* contain a categorical axiomatization of those structures. Namely, the isomorphism types of these structures are straightforwardly definable in ZFC. Holmes says: This is the crux of the matter. I claim that there is a perfectly precise (and well-known) sense in which the isomorphism type of the natural numbers (to take the simplest case) is NOT definable in ZFC (or any first-order theory). If ZFC is consistent, it has models in which the isomorphism type of the "natural numbers" (as usually defined in ZFC) in the model is not the same as the order type of the standard model of the natural numbers. You know that as well as I do. I find it very hard to interpret this quote as anything but a _deliberate_ misunderstanding of what I am saying. I also understand perfectly well that if I agree to understand the usual definition of N in ZFC as referring to the natural numbers, and the elements of P(N) as usually defined in ZFC as referring to the natural numbers, I will be able to use the machinery of ZFC to prove many correct theorems of second-order arithmetic; in fact, a lot more theorems of second-order arithmetic than I can prove in the first-order two-sorted theory usually called "second-order arithmetic". If you have read what I have written, I think that you once again know perfectly well that I understand this. In second-order ZFC, the definitions you refer to are correct. I suspect that your claim that first-order ZFC is an adequate foundation is based on an equivocation between first-order and second-order ZFC. My formulation is _not_ misleading (though it may require careful reading of the context to understand it), and I have worked very hard to make it clear exactly what I am talking about. Simpson says: > "What we can say" is a philosophical concern necessarily prior to > "what we can prove". If I asked a philosopher what branch of > philosophy this question belonged to, I think the answer might be > ... logic. So what? Regardless of what a hypothetical philosopher might say, logic is still the science of correct inference. Second-order logic is not logic in this sense, because it lacks rules of inference. Why deny this obvious point? Holmes replies: We have already looked at dictionary definitions. Logic (as a branch of philosophy) is not invariably defined as being _only_ the science of correct inference, though it is always defined so as to include that. A traditional part of the science of logic is the principles of correct (and adequate) _definition_. The advantages of second-order logic in defining well-known, basic mathematical structures are well-known; the inadequacy of first-order logic for this purpose is also well-known. The absence of complete (though _not_ of sound) systems of inference for second-order logic is also well-known, and have been granted by myself and others. The adequacy of ZFC as a foundation for mathematics if one's only concern is inference has been explicitly granted by me. Simpson said: (replying to Holmes:) > Formal logics for the purpose of expression or definition may annoy > Simpson Not at all. Where did you get that idea? Holmes replies: You repeatedly assert that logic is exhaustively defined as the science of correct inference. My position that second-order logic is an indispensible part of logic has to do with its function as a (formal!!!) language for formulating adequate definitions of basic mathematical concepts. Thus Simpson (replying to Holmes): > one may note correctly that [second-order logic] does not allow one > to prove any theorems about the natural numbers that cannot be > proved ... in ZFC, Actually, second-order logic does not allow one to prove anything at all, because it has no rules of inference. Holmes replies: The deductive principles of first-order logic are sound, though not complete, for second-order logic. I've made this point repeatedly, and so have you (though not with the same intention). They are certainly available for anyone taking a second-order approach. Simpson said: No, it's not beside the point. It goes directly to my point that any proposed approach to f.o.m. via second-order logic is useless and sterile. All of the most important f.o.m. advances (G"odel's incompleteness theorem, the work of G"odel and Cohen on the continuum hypothesis, etc etc, not to mention reverse mathematics, etc) are concerned with inference and therefore require a first-order approach and could not have happened under a second-order approach. Holmes says: We are perfectly free to use all the first-order machinery we want (including the rules for second-order quantifiers analogous to those for first-order quantifiers) while taking a second-order approach. We can also talk about models of first-order ZFC, including nonstandard ones, to our hearts' content. I can't imagine that you don't understand that. Simpson said: A comment for Holmes: I am beginning to think that your remarks may indicate some fundamental misunderstanding or off-beat assumption about current research in f.o.m. But I am having a hard time placing my finger on exactly where you are going wrong. Tell me, is your advocacy of second-order logic somehow bound up with your advocacy of NF? NF strikes most people as a rather off-beat and unintuitive kind of set theory .... Holmes replies: This has nothing to do with NF. NF is a first-order theory. I sometimes put in a good word for strong extensions of NFU (not NF itself) as alternative foundations for mathematics, but such extensions are readily intertranslatable with strong extensions of ZFC. Suitable extensions of NFU have some formal advantages and some formal disadvantages compared with ZFC; I think that ZFC has a better intuitive justification overall, but I think that the fact that there are alternative approaches is worth keeping in mind. NFU has a less satisfactory second-order metatheory (or at least a more complicated one) than ZFC, because there are small (countable!) proper classes in any model of NFU. I think that you either have or (I am really beginning to fear) feign a fundamental misunderstanding of what I have been saying in this entire thread. It is very discouraging to be treated in this way. I would like to see evidence that this is not what is actually happening. Some of the disagreement between us _may_ hinge on my using terminology in odd ways; however, I have repeatedly explained myself, with references to well-known results, to the point where it ought to be perfectly clear what I actually mean. In particular, I have not denounced formalized mathematics. I quote from a posting of Mayberry's with which I agree: Strictly speaking - and we ought to speak strictly here - a formal 1st order theory is the theory of the class of structures that satisfy it. Formal first order group theory is about all groups, i.e., all those structures that satisfy the familiar axioms of group theory; formal first order Zermelo-Fraenkel set theory is about all those structures that satisfy the axioms of ZFC. Simpson is muddled here. ZFC does not provide the foundation for mathematics. *Set theory* provides the foundation for mathematics, and ZFC is a first order formalisation of set theory. Since it is a formal, first order theory it has all sorts of interpretations that are radically different from its intended interpretation. That means that we cannot simply *identify* set theory with ZFC as a formal 1st order theory. But, as everybody knows, some of those non-intended interpretations have important uses. What makes the formal theory ZFC so important for foundations is the fact that any proof in ordinary mathematics has a formal counterpart in ZFC. (Naturally, this is not a mathematically exact claim, since "ordinary mathematics" is not an exact concept.). It is this fact that gives significance to theorems to the effect that such and such a formal proposition (e.g., the formal sentence corresponding to CH) is not among the formal theorems of ZFC. The point of setting up that formal theory is NOT to provide a foundation for mathematics - set theory performs that task. The point is rather to provide us with the means for applying rigorous mathematical reasoning to questions about what we can prove. (end Mayberry quote) 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