[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: misunderstandings*From*: holmes@catseye.idbsu.edu*Date*: Tue, 1 Jun 1999 11:57:21 -0600*Sender*: owner-fom@math.psu.edu

Quoting (with approval!) Friedman thus: It is not easy to talk about formalization in a clear way. Unless one is almost unprecedently careful, one is surely going to be misunderstood. I will attempt to be that careful. (end quote) I suggest that Simpson should carefully consider the possibility that he is misunderstanding Conway's intentions in his "foundational" remarks in _On Numbers and Games_. I see no "anti-foundational views" in this passage; neither, I think, do many other respondents in the discussion thus far. What Conway is opposing (if he can be said to be opposing anything) is "formalization in some specific system", with the accent on commitment to some specific system, rather than on formalization. I think that Conway can be understood as objecting to views which regarded some specific system (say ZFC) as the indispensible core of foundations of mathematics: of course, Simpson either holds or appears to hold views of exactly this kind, which Conway might be expected to find objectionable on the basis of the remarks in ONAG. But it is also clear from Conway's remarks that he regards the possibility of formalizing mathematical results in specific formal systems (he mentions ZFC) as an important standard of reliability; he hopes for results which will allow us (under suitable conditions) to certify reliability under this standard without actually having to carry out the formalization, which would not be at all a bad thing, if it were possible. There is nothing in this which suggests that Conway is opposed to formalization per se or does not recognize that it is important; rather the reverse. So much for what I think Conway is saying. As for what I think (Simpson asked for _my_ views...) Bodies of mathematical knowledge are prior to formalizations, which are a retrospective activity. This is less obvious in the case of set theory (and very much less obvious in the case of logic) where formalization and mathematical investigation go hand in hand, but I think that there is truth in this even there. Using an analogy which Conway makes in his discussion in ONAG, formalizations can be regarded as analogous to coordinate systems. A coordinate system is a valuable tool for talking about a space; one should note, though, that the same space admits different coordinate systems, and that one can also learn things about the space by investigating invariants which are independent of the coordinate system used. In an area that I know about, much the same piece of the mathematical universe is formalized by the following theories: 1. Russell's theory of types with infinity and choice (as simplified by Ramsey). 2. Mac Lane set theory (Zermelo set theory with comprehension restricted to delta-zero formulas) 3. NFU + Infinity + Choice 4. topos theory ("category theoretic foundations") with a natural numbers object. These systems have precisely the same consistency strength (I might have to specify 4 more precisely to make this true). Classical mathematics (outside set theory) can be formalized in any of these systems (with the same caveat about 4; I'm not sure that just having a natural numbers object is enough to give the needed consistency strength; of course one has to do some kind of double negation interpretation to interpret classical results in the intuitionistic logic of 4 -- perhaps Colin McLarty could help here?). I would find any of the systems 1-3 about equally easy to work in (though 1 is notationally awkward). I would find 4 _extremely_ hard to work in. As regards mathematical intuition, I find 1 and 2 equally reliable (bedrock!); I know that 3 is reliable (this relies on mathematical results (Jensen's consistency proof for NFU) which I would think of initially as carried out in 1 or 2); I believe that 4 is reliable due to mathematical work (known to me mostly by reputation) which I would regard as having been carried out in system 2 or extensions (much harder than the work needed to certify 3 as reliable!) The reliability of 1 or 2 for me rests on direct intuition of what the theories are about (my preformal understanding of set theory, typed or untyped), plus the fact that extensive work in these systems has revealed no inconsistency (if a contradiction were found I would conclude that my preformal intuitions had been incoherent). I am willing to regard 3 as similarly resting on a direct intuition, but I don't regard this intuition as obviously correct (the proof of the consistency of NFU is needed to firm it up for me, but I do understand this proof...); however, I can regard 3 as an autonomous foundation, because 3 is an extension of the system 1 (in a direction unexpected to a ZF-iste, and only if 1 starts without strong extensionality), and the consistency proof needed to justify 3 can be carried out in 1. I have no intuition at all (or very little) for 4, and find it hard to understand how 4 can be regarded as an autonomous foundational proposal (though I can imagine that the intuitive understanding of 4 needed for this could be developed). I would be willing to use any of the systems 1, 2, or 3 (or extensions -- note that ZFC is an extension of 2, and my reasons for restricting to 2 have to do only with the fact that this makes it easier to get systems with exactly the same strength) as my official (formalized) foundation for mathematics. Results in classical mathematics obtained from any of these formalizations are demonstrably equally reliable. I do not think that anything is gained by a fanatical devotion to one of these systems (even 3 :-) ) as opposed to any of the others. I would find it extremely difficult to use 4 as an official foundation, and I am curious about the mindset that makes this appear possible...as I suppose some are curious about the mindset that makes it possible to consider 3...but this does _not_ mean that I regard it as impossible to sincerely adopt 4 as a foundation. I have used Conway's analogy in my own thinking: 1,2,3 and perhaps 4 are "coordinate systems" covering essentially the same mathematical terrain. Results in any of these systems can be "translated" with more or less difficulty to any other of these systems (1,2,3 being quite close to each other and 4 rather distant from the others in terms of ease of communication). What I am actually studying is not any of these formal systems, but the "terrain" itself. If a program like what Conway proposes in ONAG were possible, I might have tools which would allow me to evaluate another proposed formal system 5 and recognize (under suitable conditions) that 5 was another map of the same terrain. No commitment to the existence of "mathematical terrain" (platonism) is required for such a program to make sense; it could equally well be expressed in terms of features of formal theories. Note that such a program could only be carried out with the full (and very clever) use of the same kinds of logical tools that are needed in the formalization of mathematics in a fixed system. It isn't clear to me that an adequate description of "invariants" of formal theories that would certify them as being as reliable as (say) ZFC would not be effectively a formalization of mathematics in its own right, usable as an official foundation of mathematics. (I.e., I think that a program like Conway's might be formally interesting, but I think that the result might simply be another formulation of ZFC foundations). I return to Friedman's quote and reiterate his warning that these things are extremely hard to talk about! 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

**Follow-Ups**:**Stephen G Simpson**- FOM: role of formalization in f.o.m.; coordinate systems

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]