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

*To*: fom@math.psu.edu*Subject*: FOM: NYC panel discussion/formalization*From*: Harvey Friedman <friedman@math.ohio-state.edu>*Date*: Tue, 28 Dec 1999 12:10:37 -0500*In-Reply-To*: <14411.2587.756323.727056@boole.math.psu.edu>*Sender*: owner-fom@math.psu.edu

Simpson 10:55PM 12/26/99 wrote: >A special event at the conference was a lively and wide-ranging panel >discussion on > > The Role of Set Theory and its Alternatives > in the Foundations of Mathematics > >The moderator of the panel discussion was Rohit Parikh. The panelists >were Haim Gaifman, myself, Alex Heller, and Harvey Friedman. The >entire discussion was videotaped. Perhaps Joel Hamkins can provide >information about how to obtain the videotape. >In his opening remarks, Gaifman set the tone by giving an overview of >the subject. One of Gaifman's memorable points was an analogy between >the ZFC formalism and the gold in Fort Knox. Gaifman's said that, >even if nobody ever formalizes mathematical practice in ZFC, it is >possible in principle to do so, and this is the currently accepted >basis of mathematical rigor, just as gold backing is the basis of a >sound currency. In my opinion, there are a number of very interesting deep issues connected with this common claim by logicians that ZFC is a formalization of mathematical practice. Ultimately, people may have sharply different views of what a formalization of mathematical practice is, and whether ZFC provides it or not. But there is extremely interesting basic knowledge lacking in connection with ZFC and mathematical practice that would definitely affect most in depth discussions of the matter. And taking a dogmatic view on the matter of ZFC and mathematical practice is likely to inhibit certain important research and create missed opportunities. There is no question that many respected scholars feel that in some sense essentially all of actual mathematics can be formalized in ZFC, and are happy to leave it at that for a motivation for various research in mathematical logic. But the really interesting issue is: what does it really mean? And again, no doubt many respected scholars don't really care what it really means. What it means to them is that we have sufficient motivation for studying formal systems such as ZFC. Some of the issues surrounding ZFC have been discussed on the FOM in these postings: Trybulec, April 12, 1999 Friedman, April 12, 1999 Shipman April 12, 1999 Trybulec April 22, 1999 Trybulec April 26, 1999 Trybulec is a principal of the Mizar project and an FOM subscriber. A principal application of the claim that "all mathematical proofs can be done in ZFC" is that if one shows that ZFC cannot prove a sentence phi, then mathematicians are never going to prove phi. But of course, mathematicians may some day accept more than what is in ZFC as a proof and then perhaps mathematicians might prove phi anyways. But the obvious retort is: either this is never going to happen, or if it does happen, it will be a monumental controversial event - or at least be preceded by monumental controversial events. In other words, some major change from the status quo must occur in order for this to happen. I believe in all this, even though I recognize the interest and difficulties involved in making this more precise. However, I can tell you something perhaps shocking to many: A significant percentage of mathematicians do not relate to this at all. In particular, they do not perceive the reasoning patterns that are so clear to us as mathematical logicians. Reasoning patterns in some sense embedded in ZFC. In particular, they have never even seen a single example of a formal proof of any nontriviality. So it is natural to have some presentable examples of formal proofs of nontrivialities. If one is actually going to present these, then, first of all, *they must be of some reasonable length (i.e., number of symbols). They can't be of length, say, 2^50.* But also, *they must be readable.* The latter has been a big bugaboo of mine in this area. I know that mathematicians are very fussy about what they are willing to read. It must conform to either very standard mathematical notation, or at least mathematical notation that can be viewed as an improvement on very standard mathematical notation. For example, mathematicians generally are not totally wedded to the sometimes vague dx notation, and are willing to consider operator notation, even in relatively elementary contexts when dx notation is always used. I definitely get the sense that this aspect of things is inadequately dealt with by any work I have ever seen in this area. I worked on this problem of the syntax and semantics of mathematical notation (which I looked at as preliminary to any consideration of formalization of proofs), most recently with Randy Dougherty. This is a doable problem. But somewhat independently of this, is the crucial issue of length. This can be profitably addressed without having a fully satisfactory notational scheme. In particular, I asked this question of Trybulec, and got this response: >> E.g., how long is an appropriately formal proof of Fermat's Last Theorem? >I have no idea. In other words, the crucial issue regarding lengths of formalizations is whether or not there is an impractical blowup that asserts itself when one is dealing with a particularly involved mathematical proof. In particular, a proof with a seriously nested structure. I.e., where the proof cleverly combines several major results, each of which are proved by cleverly combining several major results, etcetera, for quite a while down (up) a tree. If there is in fact some nonlinearity going on in the formalization in ZFC, then it just might assert itself in a situation like this where the completely formalized proof is of unreasonable size. And what does unreasonable size mean here? Well, certainly if the number of symbols needed is, say, more than the total number in the currently published mathematical literature. Or is it going to be even more than 2^50? Well, I don't think so. But this is because I believe in the power of formalization - if done right. I believe that we are talking about a linear phenomena. These issues have a lot in common with the analogous situation with regard to formal verification of software (and hardware, of course). In this context, the issues assume great practical importance - already of some significant importance, but perhaps much greater potential importance. It is still extremely expensive to create formally verified software for various reasons. I want to discuss this matter in greater detail in a later posting. What do the results of Mizar so far indicate about the lengths of actual formalizations of deep mathematical proofs? Of that I am not sure, but I tend to think that Mizar is evidence that we are dealing with a linear phenomenon with manageable constant factor. Incidentally, I have been told the following: a. That an investigator in the automated theorem proving project at SRI wrote a formally verified proof of the Godel first incompleteness theorem for his PhD. b. That the Godel second incompleteness theorem is regarded as very difficult to get a formally verified proof of - estimate of at least two years of hard work needed. c. That Constable at CS/Cornell is the man to talk about this project, which has not yet been started. d. Oh!! Constable is an FOM subscriber.

**References**:**Stephen G Simpson**- FOM: NYC logic conference and panel discussion

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

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