From: ross@math.hawaii.NOSPAM.edu (D. Ross) Subject: Re: Non standard analysis, proof strength Date: Sat, 01 Jul 2000 07:08:35 GMT Newsgroups: sci.math Summary: [missing] Socrates Meconium wrote: | "D. Ross" wrote: | | > the proof strength of NSA is much stronger than that of standard analysis. | | What is meant here by proof strength (and NSA)? References: Henson, C. Ward; Keisler, H. Jerome On the strength of nonstandard analysis. J. Symbolic Logic 51 (1986), no. 2, 377--386. Henson, C. Ward; Kaufmann, Matt; Keisler, H. Jerome The strength of nonstandard methods in arithmetic. J. Symbolic Logic 49 (1984), no. 4, 1039--1058. | What is the formal method referred to? Informally you can take any | proof of a concrete statement using NSA and replace quantifiers ranging | over infinite variables by standard quantifiers: "for all infinitely large | real x" --> | "for all sufficiently large x", "there exists infinitely large y" --> "there | exists | arbitrarily large y". Exercise: try this with any result using NSA which is nontrivial enough to be published somewhere other than an early chapter of an introductory text. (Several such are referenced in Nonstandard analysis. Theory and applications. Proceedings of the NATO Advanced Study Institute on Nonstandard Analysis and its Applications held in Edinburgh, June 30--July 13, 1996. Edited by Leif O. Arkeryd, Nigel J. Cutland and C. Ward Henson. NATO Advanced Science Institutes Series C: Mathematical and Physical Sciences, 493. Kluwer Academic Publishers Group, Dordrecht, 1997) - David R. ============================================================================== From: ross@math.hawaii.NOSPAM.edu (D. Ross) Subject: Re: Non standard analysis, proof strength Date: Tue, 04 Jul 2000 05:02:47 GMT Newsgroups: sci.math Me: | > | > the proof strength of NSA is much stronger than that of standard analysis. socrates meconium: | 1. Is NSA (in your sentence above) conservative over standard analysis, or not? Yes. | 2. If conservative, is there some result on NSA proofs tending to be | shorter than regular proofs? Yes, the papers I cited. | Is the method something like what I mentioned, or based on different ideas? "Something like" maybe, though they in fact prove that NSA has _third order_ proof strength (not just 2nd order). | Any result nontrivial enough to publish in a journal or conference proceedings | (such as the one you cited) is likely to be too technical to easily understand, | let | alone reprove in a different language, without serious effort. So the point of | your Exercise is not clear. [snip] | I have no access to this book. If you know of a concrete statement proved | with NSA and resilient to the informal translation I mentioned above, please | post it. Well, that's a problem. Suppose I come up with an elementary, Usenet-level example. This will likely come from elementary analysis (EA). We are quite capable of proving EA results with epsilons and deltas, and I would likely have a hard time convincing anyone that such a standard argument is *not* just an "informal translation". For example, a NSA proof that a continuous function f on a closed interval [a,b] is uniformly continuous goes as follows: (1) Let x\approx y in *[a,b] (2) x and y have a common standard part, call it z (3) Since f is continuous, *f(x)\approx f(z)\approx *f(y) (4) Hence *f(x)\approx *f(y), and so f is uniformly continuous (by the NSA criterion for unif. cont.) Now, implicit in step (2) is the statement that [a,b] is compact, and of course a standard proof can be given by finding standard versions of (1,3,4) and tacking on some different compactness argument. Is this what you might mean by "informal translation"? If so, I don't know any EA result which is immune from this. The most interesting results in NSA (in my opinion) are the ones using things like Loeb measures and nonstandard hulls of Banach spaces; these are well beyond EA, and much of their interest stems from their intrinsic reliance on "external" sets, which among other things means that the results using them cannot be formalized in 1st order language on which the original model is based. This means that the fact that NSA is conservative over standard analysis is largely irrelevant for such constructions. - DR ============================================================================== From: ross@math.hawaii.NOSPAM.edu (D. Ross) Subject: Re: Non standard analysis (sin h)/h Date: Tue, 04 Jul 2000 03:35:44 GMT Newsgroups: sci.math vaeth@mathematik.uni-wuerzburg.de (Martin Vaeth) wrote: | Now I am rather curious: Is there really an application of NSA which | *in principle* can not be done with an ultrapower model? [snip] | I am aware of the direct limit construction which was (to my knowledge) | introduced by Luxemburg to obtain models with various saturation properties | (see e.g. the book of Stroyan/Luxemburg). However, this does not answer my | question, since by using more sophisticated ultrafilters one can obtain | the same saturation properties for ultrapower models. There exist several natural examples which to date have have only been constructed in models satisfying quite subtle saturation properties, e.g. the "Special Model" axiom or the "kappa-isomorphism" property, and the models satisfying these properties are normally constructed as limits of ultrapowers. Search Math Reviews or Zentralblatt for papers by me, by Renling Jin, and/or by Shelah with terms like "special model axiom" or "isomorphism property" in the title. There is a nice survey article by Jin, "Better nonstandard universes with applications", in the 1997 Edinburgh NATO ASI proceedings. Now, the isomorphism property can indeed be satisfied by models which are ultraproducts (this by adapting Shelah's nontrivial extension of Keisler's well-known 'isomorphic ultrapowers' theorem). I believe, however, that one needs more than ZFC to satisfy the special model axiom as an ultrapower, and there is at least one nontrivial interesting result which to date has only been proved assuming SMA. (Namely, that every point-finite completely-measurable family of Loeb nullsets has null union.) - David R. ============================================================================== From: Aristotle Petroleum Subject: Re: Non standard analysis, proof strength Date: Thu, 13 Jul 2000 00:14:09 -0400 Newsgroups: sci.math David Ross wrote: > | > | > the proof strength of NSA is much stronger than that of standard analysis. > > | 1. Is NSA (in your sentence above) conservative over standard analysis, or not? > > Yes. The paper you cited has the stated purpose of showing NSA is *not* conservative over standard analysis. "It is often asserted in the literature that any theorem which can be proved using nonstandard analysis can be proved without it. The purpose of this paper is to show that this is wrong, and in fact there are theorems which can be proved with nonstandard analysis but cannot be proved without it." (Henson & Kiesler, On the Strength of Nonstandard Analysis, JSL 1986.) > | 2. If conservative, is there some result on NSA proofs tending to be > | shorter than regular proofs? > > Yes, the papers I cited. The papers you cited do not discuss proof length. > they [Henson & Kiesler] in fact prove that NSA has _third order_ > proof strength (not just 2nd order). Not really. They cite earlier work from the late 60's, showing that N'th order nonstandard and standard "analysis" (in their sense) have exactly the same proof strength (in their sense), and that this is unchanged if one also adds axioms expressing the transfer principle and the *-operation. The new feature of their 1984-86 JSL papers is to show that saturation axioms add extra logical strength. This suggests that saturation axioms, not nonstandard models per se, are what bolsters the strength of the system. However, their results are all for a weakened notion of "analysis" (N'th order arithmetic). For more conventionally expressive systems of analysis, such as ZFC, they cite results from the 1970's that nonstandard analysis together with saturation axioms is, once again, of exactly the same strength as standard analysis. In other words, it seems that you have to carefully pick and choose what to consider as standard analysis and what to consider as nonstandard analysis, to get NSA to come out as being stronger. (The JSL paper doesn't address the obvious question of whether their system of standard analysis with an analogue of the saturation axioms but no nonstandard elements, would also gain the same extra logical strength. If true this would also undermine the claim that nonstandard methods are of provably higher strength.) (Note to DR: this answers only the first half of your message. The rest I will consider later as time permits.) ============================================================================== From: Aristotle Petroleum Subject: Re: Non standard analysis, proof strength Date: Thu, 13 Jul 2000 02:51:55 -0400 Newsgroups: sci.math David Ross wrote: > | Is the method something like what I mentioned, or based on different ideas? > > "Something like" maybe, though they in fact prove that NSA has _third order_ > proof strength (not just 2nd order). The question was not what method H+K use to calibrate NSA proof strength, but rather what the "formal method" is that you and a previous poster mentioned, for translating nonstandard to standard proofs. > | If you know of a concrete statement proved with NSA and > | resilient to the informal translation I mentioned above, please post it. > > Well, that's a problem. Suppose I come up with an elementary, Usenet-level > example. This will likely come from elementary analysis (EA). Is EA a specific formal system? > We are quite > capable of proving EA results with epsilons and deltas, and I would likely > have a hard time convincing anyone that such a standard argument is *not* > just an "informal translation". I don't know what EA means. By informal translation I mean that: -- quantifiers over infinite variables can be replaced by (layered) quantifiers over standard variables. "for all infinite real x" = "for sufficiently large x", "exists infinitesimal x" = "exist arbitrarily small x". -- there is an older tradition of interpreting "infinitesimal" to mean a variable tending to zero. Using this and similar locutions one can sometimes give a direct standard reading of nonstandard arguments. (I think there are more sophisticated versions using sheaves to codify the notion of a family of (standard) reals, but in many cases you can get away with the naive translation.) -- NSA arguments using ultrapowers to prove standard results (not involving axiom of choice) must be independent of the ultrafilter used, so ultimately only the sets built into the filter are relevant and the proofs probably can be recast to reflect this. e.g. if a nonstandard real is a sequence of reals modulo sequences supported on sets of "measure" zero, the only relevant properties of measure 0 sets are that they include the finite sets, which leads back to the classical idiom of sequences tending to zero as being infinitesimal. > For example, a NSA proof that a continuous function f on a closed interval > [a,b] is uniformly continuous goes as follows: (1) Let x\approx y in *[a,b] > (2) x and y have a common standard part, call it z (3) Since f is > continuous, *f(x)\approx f(z)\approx *f(y) (4) Hence *f(x)\approx *f(y), > and so f is uniformly continuous (by the NSA criterion for unif. cont.) What NSA definitions of continuous and uniformly continuous are used here? At least one of them seems to refer to the *-operation, so the above would not yet prove anything standard without tacking on an additional "standard continuous = NSA continuous" argument. (And maybe in step 4 the definition of uniform continuity should read "x ~ y implies f(x) ~ f(y)"?) > Now, implicit in step (2) is the statement that [a,b] is compact, How do the details of step 2 and/or the compactness argument run in NSA? The proof sketch above does not yet use the fact that [a,b] is closed, without which the result is false. > and of course a standard proof can be given by finding standard versions of (1,3,4) > and tacking on some different compactness argument. > Is this what you might mean by "informal translation"? No, I mean finding a translation using ordinary standard locutions with recognizably similar meanings, that preserves the flow of concepts in the NSA argument. That other, possibly unrelated, standard proofs are known to exist for general reasons doesn't matter. > If so, I don't know any EA result which immune from this. > The most interesting results in NSA (in my opinion) are the ones using > things like Loeb measures and nonstandard hulls of Banach spaces; these are > well beyond EA, and much of their interest stems from their intrinsic > reliance on "external" sets, which among other things means that the results > using them cannot be formalized in 1st order language on which the original > model is based. This means that the fact that NSA is conservative over > standard analysis is largely irrelevant for such constructions. Well, I think we see the same issue in microcosm above. If the concepts involved are externally defined then at some point there is a divergence in subject matter. For simple concepts like continuity one can identify the pre-existing (or otherwise obvious) standard equivalents and so recover standard results as a byproduct of the NSA arguments. But as things get more sophisticated, this becomes harder. I guess it depends on the attitude of the NSA practitioners: are they generating standard results or exploring an alternate but equally valid universe, noting standard results as they arise? ============================================================================== From: ross@math.hawaii.NOSPAM.edu (D. Ross) Subject: Re: Non standard analysis, proof strength Date: Fri, 14 Jul 2000 07:53:30 GMT Newsgroups: sci.math Aristotle Petroleum wrote: | The paper you cited has the stated purpose of showing NSA is *not* conservative | over standard analysis. | "It is often asserted in the literature that any theorem which can be proved | using nonstandard analysis can be proved without it. The purpose of this | paper is to show that this is wrong, and in fact there are theorems which | can be proved with nonstandard analysis but cannot be proved without it." | (Henson & Kiesler, On the Strength of Nonstandard Analysis, JSL 1986.) There is also an old result of (I think) Harvey Friedman which shows that NSA *is* conservative over analysis; obviously, they are using different notions of "conservative" and "analysis" (where of course for the former one must specify the logic, and for the latter the appropriate language). | This suggests that saturation axioms, not | nonstandard models per se, are what bolsters the strength of the system. Well, yes. AFAIK there are few if any results in NSA published in the last decade where saturation isn't important. | In other words, it seems that you have to carefully pick and choose what | to consider as standard analysis and what to consider as nonstandard analysis, | to get NSA to come out as being stronger. Sure. | > Well, that's a problem. Suppose I come up with an elementary, Usenet-level | > example. This will likely come from elementary analysis (EA). | | Is EA a specific formal system? No, I mean informal elementary analysis, as in a third-year undergraduate course. My point was that the nonstandard machinery rarely adds much (other than a bit of brevity) to proofs of theorems at this level. | -- NSA arguments using ultrapowers to prove standard results (not involving | axiom of choice) must be independent of the ultrafilter used, Well, this is not obviously true. Example: one of the most common ways NSA is used to prove existence theorems in probability is the Loeb measure construction, and the properties of the object (measure, stochastic process, etc) which is constructed can depend on the underlying NS model. For example, let X be a hyperfinite set of internal cardinality H, let p be the internal counting measure on X giving each z\in X a measure 1/H. Write P for the standard part of p, then P is a perfectly genuine - external - finitely additive probability measure on (X,A) where A is the algebra of internal subsets of A. P can be extended to a standard countably-additive measure on the smallest (external) sigma-algebra extending A (proof uses a bit of saturation). Now, the properties of P - as a standard probability measure - can depend on the model in a nontrivial way; for example, Jin and Shelah have shown that the "compactness" of P (a standard concept I won't define here) can depend on the nonstandard model. Now, w/r to Loeb measures you said: | Well, I think we see the same issue in microcosm above. If the concepts | involved are externally defined then at some point there is a divergence in | subject matter [snip] | I guess it depends on the attitude of the NSA practitioners: are they | generating standard results or exploring an alternate but equally valid | universe, noting standard results as they arise? Results using things like the Loeb measure construction are clearly standard, since they assert the existence of standard objects (measures, Banach spaces, etc.) with standard properties. However, they are not obtained by proving a nonstandard equivalent of a standard result then invoking transfer, as is the usual case with nonstandard arguments in EA. I would say that for this latter kind of nonstandard reasoning - the kind which was dominant 25+ years ago - your arguments make sense. | > For example, a NSA proof that a continuous function f on a closed interval | > [a,b] is uniformly continuous goes as follows: (1) Let x\approx y in *[a,b] | > (2) x and y have a common standard part, call it z (3) Since f is | > continuous, *f(x)\approx f(z)\approx *f(y) (4) Hence *f(x)\approx *f(y), | > and so f is uniformly continuous (by the NSA criterion for unif. cont.) | | What NSA definitions of continuous and uniformly continuous are used | here? At least one of them seems to refer to the *-operation, so the above | would not yet prove anything standard without tacking on an additional | "standard continuous = NSA continuous" argument. | | (And maybe in step 4 the definition of uniform continuity should read | "x ~ y implies f(x) ~ f(y)"?) The usual nonstandard ones, yes, and yes. | > Now, implicit in step (2) is the statement that [a,b] is compact, | | How do the details of step 2 and/or the compactness argument | run in NSA? The proof sketch above does not yet use the fact | that [a,b] is closed, without which the result is false. Once you know that x and y have standard parts, their commonality is easy. So, it suffices to show that x has a standard part. If not, then every (standard) z in [a,b] has a neighborhood u(z) with x not in *u(z). By (standard) compactness, there's a finite subcover of [a,b], etc... Or, just somehow show that every _finite_ hyperreal x has a standard part, the proof of which either is like the one I just gave, but more often is done by considering inf{standard w | x Subject: Re: Non standard analysis, proof strength Date: Sat, 15 Jul 2000 02:28:26 -0400 Newsgroups: sci.math David Ross wrote: > Aristotle Petroleum wrote: > > | The paper you cited has the stated purpose of showing NSA is *not* | conservative > over standard analysis > There is also an old result of (I think) Harvey Friedman which shows that NSA *is* > conservative over analysis; The result for "analysis" meaning second order arithmetic is by Friedman, with extensions to higher order arithmetic by Kreisel. This was proved in the 1960's and is mentioned in the 1986 JSL paper you cited. > obviously, they are using different notions of "conservative" and "analysis" (where > of course for the former one > must specify the logic, and for the latter the appropriate language). They are using (essentially) the same notion of conservative, and the same notion of standard analysis, namely N'th order arithmetic for some N. What is different is the addition of saturation axioms on the NSA side. However... > | This suggests that saturation axioms, not nonstandard models per se, |are what > bolsters the strength of the system. > > Well, yes. For more usual notions of "analysis", such as ZFC, results of Nelson (from the 1970s) are cited to the effect that saturation axioms do *not* add any extra logical strength to nonstandard analysis. Since saturation adding strength is apparently not robust with respect to choice of formalization, the Henson/Kiesler results may be more an artifact of their choice of model than an inherent feature of NSA. > AFAIK there are few if any results in NSA published in the last > decade where saturation isn't important. If the Henson/Kiesler formalization is a realistic model of standard analysis (which I doubt since it e.g. forbids the powerset operation), then some of these results should be outright unprovable in standard analysis.