Quoting Makarius <makarius at sketis.net>: > Does it mean that there is no particular > advantage in the NSA part anymore, unless you are specifically interested > in the non-standard thing?
Quoting Lawrence Paulson <lp15 at cam.ac.uk>: > I see a giant misconception coming. The point of nonstandard analysis > is that it makes properties of limits, derivatives, and so forth much > easier to prove than can be done with the standard definitions. They > eliminate the necessity of arguments involving epsilon and delta. So > it would be a mistake to imagine that the nonstandard theories are > only useful for people who are exploring nonstandard analysis. They > should be valuable to anybody who wants to prove anything in analysis. > It would be a shame to see them buried somewhere. Here's how I see it: If all you want to do is *use* analysis (e.g. maybe you just want to calculate derivatives) then you won't notice any difference between NSA and standard analysis. The same theorems have been proved in either version. I expect that the users who benefit most from having the real number theories in HOL would generally fall into this camp. On the other hand, if you want to *prove* things *in* analysis, then the difference between standard and non-standard is immediately apparent. I wouldn't consider NSA to be "buried" - until very recently, the NSA theories were located in a logic image separate from the main HOL image. If we split NSA as I have proposed, then it will be in a logic image separate from HOL, just as it was before. - Brian
