12
$\begingroup$

In this MathOverflow thread, a comment states:

Any proof using a transfer principle can be rewritten without it, so in some sense it can't play an “essential” role in a proof.

Is there a known theorem or proof-theoretic result (analogous to cut-elimination or conservativity results for IST) that guarantees that any proof that uses the transfer principle can be effectively transformed into a proof that does not use it?

References would be especially appreciated.

New contributor
Super Cool Guy is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
$\endgroup$
11
  • 6
    $\begingroup$ There are multiple formal results that one can invoke to eliminate certain specific appeals to the Transfer principle from arguments. For example, Nelson's The syntax of nonstandard analysis gives an algorithm that eliminates the Idealization, Standardization and Transfer axioms from arguments with internal conclusions in Internal Set Theory. In the 2010s Sanders and others gave more sophisticated algorithms that accomplish the same in other contexts. 1/ $\endgroup$ Commented yesterday
  • 4
    $\begingroup$ If your conclusion is a sufficiently simple, arithmetical statement, you can use results such as Shoenfield absoluteness to extract a ZF proof from any ZFC proof. The extracted ZF proof will not appeal to the general transfer principle, since one cannot prove general transfer in ZFC. In particular, if ZFC proves the twin prime conjecture, then ZF also proves it, and the ZF proof won't appeal to the transfer principle. 2/ $\endgroup$ Commented yesterday
  • 8
    $\begingroup$ I don't think the MO comments in question ever intended to imply that appeals to transfer can always be eliminated from every ZFC proof of every sort. It's not clear how one would formalize such a statement, and even if one could somehow formalize it, the current "tech level" of proof theory would likely be insufficient for proving or refuting such a result. The commenter is fully aware of this, so his assertion is intended to say something about mathematical results that resemble ones appearing in the question, and the basic kind of applications of transfer suggested in the question. 3/3 $\endgroup$ Commented yesterday
  • 2
    $\begingroup$ @DietrichBurde, your dismissive comment about nonstandard analysis is along the lines of what was preached by Paul Halmos decades ago, and was disproved many times over; see for example this: u.cs.biu.ac.il/~katzmik/infinitesimals.html#16b $\endgroup$ Commented yesterday
  • 2
    $\begingroup$ @MikhailKatz I am sorry, there was nothing "dismissive" intended (and I don't believe this). I was trying to say how I interpret the MO comment, which had a different motivation (for some approaches to the twin prime conjecture). $\endgroup$ Commented yesterday

2 Answers 2

Reset to default
16
$\begingroup$

"Is this statement ill-formed, and otherwise, how can we prove/disprove it?"

Yes, the claim is ill-formed, and one can disprove it from Chow's comment itself. He does not claim that there are no applications that were first proved using nonstandard analysis; rather he claims that there are "not many". While one can disagree even with such a claim, it is more important to note that what Chow did not mention is that there are a number of applications where the only proof available is via nonstandard analysis.

In broader terms, note that the transfer principle you referred to is the distinguishing feature that makes hyperreal fields superior to other non-Archimedean fields (such as the surreals or Levi-Civita fields), because it enables a full development of analysis and other fields using infinitesimals and unlimited numbers. So we are really talking about the usefulness of nonstandard analysis (and not merely the transfer principle).

The usefulness of nonstandard analysis (NSA) can be illustrated at several levels. Since you are a fairly new contributor, I am not sure what level you expect an answer to be at, so I will mention several of them.

  1. NSA is useful at the pedagogical level. Key notions like continuity have a more transparent definition if one is allowed to use infinitesimals. More specifically, NSA definitions have fewer quantifier alternations, which have been the bugaboo of undergraduate math education for several generations.

  2. NSA is useful at the level of the history of mathematics. It enables a better understanding of the procedures of key pioneers like Fermat, Leibniz, Euler, and Cauchy (whose definition of continuity was not the one you are probably thinking). Many recent articles on the subject can be found at https://u.cs.biu.ac.il/~katzmik/infinitesimals.html

  3. NSA is useful at the research level. A particularly powerful tool is provided by Loeb measures, which have been used in a number of fields to go further than what traditional non-infinitesimal approaches allow.

  4. For folks worried about ultrafilters, I have good news: Hrbacek and I proved that you don't need them to use infinitesimals. See Hrbacek, K.; Katz, M. "Infinitesimal analysis without the Axiom of Choice." Annals of Pure and Applied Logic 172 (2021), no. 6, 102959. https://doi.org/10.1016/j.apal.2021.102959, https://arxiv.org/abs/2009.04980, https://mathscinet.ams.org/mathscinet-getitem?mr=4224071 See also an introduction at https://u.cs.biu.ac.il/~katzmik/spot.html

  5. Here is an example of an infuential result whose proof relies on NSA while there is no infinitesimal-avoiding proof: Di Nasso, Mauro; Goldbring, Isaac; Jin, Renling; Leth, Steven; Lupini, Martino; Mahlburg, Karl. On a sumset conjecture of Erdős. Canad. J. Math. 67 (2015), no. 4, 795–809.

$\endgroup$
10
  • 2
    $\begingroup$ In addition to Prof. Katz's points, nonstandard analysis aids computer-assisted proof verification (e.g., in Isabelle/HOL) and automated theorem proving (e.g., in SAT/SMT solvers), as its quantifier-reduced formulations often yield shorter, more natural proofs that are easier for provers to discover and check. While rigorous complexity lower bounds remain open, empirical evidence from formalized libraries supports this advantage. Reference: Fleuriot, Jacques D., and Lawrence C. Paulson. "Mechanizing nonstandard real analysis." LMS Journal of Computation and Mathematics 3 (2000): 140-190. $\endgroup$ Commented yesterday
  • 1
    $\begingroup$ What is an example of an application where the only proof is via nonstandard analysis? My impression from when I studied the subject is that there was a straightforward proof that the infinitesmal approach is logically equivalent to the usual limit proof. My actual experience matches Chow's claim (at least as far as I went in NSA) - there was always a fairly mechanical translation from the infinitesmal proof to an $\epsilon-\delta$ proof. $\endgroup$ Commented yesterday
  • 5
    $\begingroup$ Pedagogically, my experience differs. I found NSA to be an exemplar of the "sweep it under someone else's carpet" school of emulated simplicity. My reaction once I actually untangled ultrafilters was, "You don't need the axiom of choice to define the derivative of $x^2$." I do agree that it helped me in understanding the history of mathematics. I have no exposure to NSA at the research level. $\endgroup$ Commented yesterday
  • 3
    $\begingroup$ @btilly, you wrote: "there was always a fairly mechanical translation from the infinitesmal proof to an ϵ−δ proof". If this is true, I would very much like to see your mechanical translation of the proof in Di Nasso et al. mentioned in my answer. $\endgroup$ Commented yesterday
  • 2
    $\begingroup$ By "there is no infinitesimal-avoiding proof", you mean "for which the infinitesimal-avoiding proof has not been written down". Translating their proof into an infinitesimal-avoiding one would be a routine application of existing techniques. (I'm not sure one would want to - it's a very clean proof that would just become a mess of quantifiers if one did that.) $\endgroup$ Commented 21 hours ago
8
$\begingroup$

Yes, there are a number of results showing that proofs using nonstandard analysis can be translated into standard proofs in a variety of contexts - "On the Strength of Nonstandard Analysis" (Henson and Keisler), "Weak Theories of Nonstandard Arithmetic and Analysis" (Avigad), "The unreasonable effectiveness of Nonstandard Analysis" (Sanders), and of course my favorite is "What do Ultraproducts Remember about the Original Structure?" (me).

Note that this isn't at all the same as saying the transfer principle or nonstandard analysis is useless. All these results show that there's a cost to the translation - the standard proofs involve more complicated statements and objects than the nonstandard ones (necessarily so, as Henson and Keisler's paper shows). So the transfer principle and nonstandard analysis may be useful in terms of making proofs easier to understand, or in finding new results which would be very difficult to find using only conventional means (and indeed, in various parts of mathematics, this is the case).

But, as the comment says, it can't be essential - if something can be proven with nonstandard analysis, it can (in principle) be proven without.

$\endgroup$
11
  • 2
    $\begingroup$ Henry, I think that your comment "in principle", instead of being parenthetical, should be emphasized. The reduction to a non-infinitesimal proof is a purely theoretical result. Imagine if every time you wanted to log into your bank account, you had to program a Turing machine for this purpose. In principle this would be possible, but who in his right mind would want to work that way? $\endgroup$ Commented yesterday
  • $\begingroup$ @MikhailKatz: In what sense is the reduction purely theoretical? It has been carried out in multiple actual cases (usually to strengthen results with explicit quantitative bounds). $\endgroup$ Commented 21 hours ago
  • 1
    $\begingroup$ Henry, which reduction procedures are you referring to exactly? I am familiar with two types: (1) fairly algorithmic procedures developed by Sanders and others to obtain quantitative bounds from proofs using infinitesimals. I admire this work but it involves a limitation to a fairly small quantifier alternations; and (2) conservativity proofs that do not involve limitations on the number of quantifier ... $\endgroup$ Commented 16 hours ago
  • 1
    $\begingroup$ ... alternations, but which are "theoretical" in the sense that beyond the existence of such a translation, the actual outcome of the translation would be unreadable. I am therefore surprised by your comment below my answer that you expect that the result by Di Nasso et al. mentioned in my answer could be mechanically translated. Can you clarify this point? $\endgroup$ Commented 16 hours ago
  • $\begingroup$ @MikhailKatz The procedure in the paper of mine that I cited is mechanical and applies to statements in $L_{\omega_1,\omega}$, so well beyond finite alternations of quantifiers. It’s been applied in practice to statements with five quantifiers (though the result isn’t especially readable), which should be enough for what’s in Di Nasso et al. Further, the methods in Di Nasso et all are similar to the sort of measure theoretic decomposition results where this translation has been used a lot, so large portions of the translation would be quite routine for someone who knows the literature well. $\endgroup$ Commented 8 hours ago

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.