Smooth Infinitesimal Analysis FAQ

This is Revision (30 July 2016) of the Smooth Infinitesimal Analysis FAQ.

Contents


1. Basic questions

1.1. What is the purpose of this FAQ?
1.2. What’s the intuition behind Smooth Infinitesimal Analysis?
1.3. Making infinitesimals nilsquare seems arbitrary. Is there a justification for this?

2. Logic Matters
2.1. I find Intuitionistic Logic… unintuitive. What kind of reasoning am I allowed to use?
2.2. I’ve heard in Algebra that fields don’t have nilpotent elements. Yet my SIA book calls the real line a field. Isn’t that a contradiction?**
2.3. Can you show me a non-zero nilsquare infinitesimal?

3. Microcancellation
3.1. How do I prove microcancellation?
3.2. I believe I’ve found a contradiction using microcancellation. What do I do?

4. Infinitesimal Calculus
4.1. I don’t know how to prove the chain rule. Can you help?
4.2. How do I prove that the exponential function is its own derivative?
4.3. What is the deal with the square root function?
4.4. Infinitesimals don’t have reciprocals, so how does the quotient rule work?

5. Counterexamples to Classical Theorems
5.1. Can I prove the Extreme Value Theorem in SIA?
5.2. Can I prove the Intermediate Value Theorem in SIA?
5.3. Can I prove the non-infinitesimal form of Taylor’s theorem in SIA?

6. Technical Stuff
6.1. Where can I find all the axioms of Smooth Infinitesimal Analysis?
6.2. Is Smooth Infinitesimal Analysis constructive?

1. Basic questions

1.1. What is the purpose of this FAQ?

Smooth Infinitesimal Analysis (abbreviated SIA) is a variant of Non-classical Real Analysis which uses nilpotent infinitesimal quantities to deal with concepts such as continuity and differentiability. The subject had its origins in Alexander Grothendieck’s work on Algebraic Geometry, as interpreted by F. William Lawvere, Anders Kock, John L. Bell and others.

The orginal formulation of Smooth Infinitesimal Analysis, and the wider Synthetic Differential Geomerty, was topos-theoretic. Later on, SIA was given a readily accessible axiomatic presentation. Since Kock’s textbook, “Synthetic Differential Geometry” became freely available, there’s been much interest in Smooth Infinitesimal Analysis. Unfortunately, SIA has a fair amount of initial hurdles: the necessary use of Intuitionistic Logic and the failure of many classical theorems of Analysis; worst of all, the real payoff (definitions that are easier to state, theorems that are easier to prove) comes much later, when one gets to the treatment of Differential Geometry.

This FAQ is not a self-contained introduction to SIA: its purpose is to get independent learners (readers of Kock’s book) past the aforementioned initial hurdles by answering the questions that often come up. The questions in this FAQ were collected in part from fellow students, and in part from Reddit, Stack Exchange and various online mailing lists. If you have a question that you’d like answered, feel free to write a comment.

1.2. What’s the intuition behind Smooth Infinitesimal Analysis?*

“Under the microscope”, the graph of a differentiable function is approximately a straight line. The idea is to extend the real numbers with infinitesimal values. Viewed at infinitesimal scales, the graph of every smooth function becomes an exact (i.e. not merely approximate) straight line.

In Smooth Infinitesimal Analysis, the set of real numbers \mathbb{R} is replaced with the real line \mathcal{R}. The real line contains a set of infinitesimal numbers \Delta = \{\varepsilon \in \mathcal{R} | \varepsilon^2 = 0 \}. The fact that every function is linear is formalized by the Kock-Lawvere axiom:

Axiom. (Kock-Lawvere). Every function f:\mathbb{R}\rightarrow\mathbb{R} has a unique slope m such that for all nilsquare infinitesimals \varepsilon, f(\varepsilon) = m \varepsilon + f(0).
Stated.

This unique slope m is called the derivative at zero of the function f. Generally, we can define the derivative at point a as the derivative at zero of the translated function g(x)=f(x+a).

Starting from here, infinitesimals allow us to do differential and integral calculus without invoking limits. Things get even better once we get to differential geometry: notions such as tangent vectors and jets can be given single-sentence definitions using infinitesimals.

1.3. Making infinitesimals nilsquare seems arbitrary. Is there a justification for this?

The end goal is not nilsquare infinitesimals: the end goal is to define infinitesimals that are so small that every smooth function looks linear on their scale. It just happens that as long as infinitesimals

  • Obey the Kock-Lawvere axiom
  • Come in positive-negative pairs, that is \varepsilon and -\varepsilon are both infinitesimal

they are necessarily nilsquare. Why? Well, the function f(x) = x^2 is even, that is, f(x)=f(-x) for all x. Let \varepsilon be an infinitesimal that obeys the too conditions above. By the Kock-Lawvere axiom, we have both f(\varepsilon) = f'(0) \varepsilon and f(\varepsilon) = f(-\varepsilon) = - f'(0) \varepsilon. Thus, by algebra f'(0) \varepsilon = 0.

It follows that \varepsilon^2 = f(\varepsilon) = f'(0) \varepsilon = 0.

2. Logic Matters

2.1. I find Intuitionistic Logic… unintuitive. What kind of reasoning am I allowed to use?

First of all, watch Andrej Bauer’s Five Stages of Accepting Constructive Mathematics, where he clears up some common misconceptions about intuitionistic logic.

In my experience, there’s one more thing that trips people up: switching back and forth between affirmative and negative sentences. The good news is that in most cases, you can use De Morgan’s laws in Intuitionistic Logic. The bad news is that you’ll have to remember to avoid the three exceptions listed below (needless to say, valid replacements work “the other way round” in the hypotheses).

Replacing … with … is …
the book is thick it is not the case that the book is not thick valid.
it is not the case that the book is not thick the book is thick INVALID.
the book is either not thick or not blue the book is not thick and the book is not blue valid.
the book is not both thick and blue the book is either not thick or not blue INVALID.
there is a book that is not thick not all books are thick valid.
not all books are thick there is a book that is not thick INVALID.
2.2. I’ve heard in Algebra that fields don’t have nilpotent elements. Yet my SIA book calls the real line a field. Isn’t that a contradiction?**

Both are right, from a certain point of view. In Classical Logic, fields don’t have nilpotent elements.

Thm. Let x^n=0. Then x=0.
Proof.
Induction on n. The base case with n=1 is trivial.
In the inductive case, we know that x^{k+1}=0. There are two possibilites. Either x^k = 0 as well, or x^k \neq 0. In the former case, x=0 by inductive hypothesis. In the latter case, x^k has a multiplicative inverse x^{-k}, and therefore x=x^{-k}x^{k+1}=x^{-k}0=0.
Qed.

Fortunately, the proof above relies on the statement that “either x^k = 0 or x^k \neq 0“. When we work inside Intuitionistic Logic, this is a non-admissible instance of the Law of Excluded Middle. So the proof does not go through in the context of Smooth Infinitesimal Analysis, and the contradiction is avoided.

2.3. Can you show me a non-zero nilsquare infinitesimal?

No. Imagine that you produce an infinitesimal \mathfrak{o}^2 = 0 that is non-zero, i.e. \mathfrak{o}\neq 0. Since it is non-zero, it has to have a multiplicative inverse, \mathfrak{o}^{-1}. That gives us the equation \mathfrak{o} = \mathfrak{o}^{-1}\mathfrak{o}^2 = 0, a contradiction.

Infinitesimals are not non-zero. This is not the same as being zero, since we’re working in intuitionistic logic. However, this does mean that they are so close to zero that we can’t tell them apart from zero. The only way to produce an infinitesimal is to pick an arbitrary one: infinitesimals only occur in proofs, introduced by the sentence “take any \varepsilon \in \Delta“.

3. Microcancellation

3.1. How do I prove microcancellation?

When proving non-trivial equalities in SIA, the trick is usually to pick a suitable function, calculate its derivative in two ways, and argue that the results must be equal due to the uniqueness clause of the Kock-Lawvere axiom.

Thm. (Microcancellation). Let a,b be real numbers (i.e. elements of the real line) such that \varepsilon a = \varepsilon b for every nilsquare infinitesimal \varepsilon. Then a=b.
Proof.
Consider the function f(x) = ax. On one hand, the derivative of ax is f'(x) = a, since f(x+\varepsilon) = a(x+\varepsilon) = ax + a\varepsilon. On the other hand, since a\varepsilon=b\varepsilon, we also have a(x + \varepsilon) = ax + a\varepsilon = ax + b\varepsilon, so f'(x) = b. Therefore, a=b.
Qed.

3.2. I believe I’ve found a contradiction using microcancellation. What do I do?

Since SIA is known to be consistent, chances are you have misused microcancellation. A common “paraproof” goes as follows:

Take an arbitrary infinitesimal \varepsilon^2 = 0. We get the equality \varepsilon\varepsilon=\varepsilon 0, and by microcancellation \varepsilon = 0, contradicting the fact that zero is not the only infinitesimal.

What’s the mistake here? Stated formally, the microcancellation principle says the following: (\forall \varepsilon. \varepsilon^2=0 \rightarrow \varepsilon a = \varepsilon b) \rightarrow a = b. The scope of the quantifier (\forall \varepsilon) is the parenthesized expression only. That is, if you’re using microcancellation correctly, \varepsilon cannot occur in either a or b.

4. Infinitesimal Calculus

4.1. I don’t know how to prove the chain rule. Can you help?

Hint: every multiple of a nilsquare infinitesimal is also a nilsquare infinitesimal.

Thm. (Chain rule). The derivative of the function (f \circ g) is g'(f' \circ g).
Proof.
We have f(g(x+\varepsilon)) = f(g(x) + \varepsilon g'(x)) by the Kock-Lawvere axiom. Let g(x) = y,\: \varepsilon g'(x) = \delta. Notice that \delta^2 = 0, so we can apply the Kock-Lawvere axiom to f(y + \delta)=f(y)+\delta f'(y). Observe that f(y)+\delta f'(y)=f(g(x))+\varepsilon g'(x) f'(g(x)). On the other hand, by the Kock-Lawvere axiom, we have f(g(x+\varepsilon)) = (f \circ g)(x+\varepsilon) = (f\circ g)(x) + \varepsilon (f \circ g)'(x)).
This gives us the equality \varepsilon (f \circ g)'(x) = \varepsilon g'(x) f'(g(x)) and therefore, by microcancellation (f \circ g)'(x)=g'(x) f'(g(x)).
Qed.

4.2. How do I prove that the exponential function is its own derivative?

For any exponential function g(x) = b^x, we have g(\varepsilon) = b^\varepsilon = 1 + \varepsilon g'(0) by the Kock-Lawvere axiom, and g'(0) clearly depends on b only. Thus, we can take g'(0) = 1 to be the defining property of the number e.

Thm. The derivative of f(x)=e^x is itself.
Proof.
We have f(x+\varepsilon) = e^x+\varepsilon = e^x e^\varepsilon by the algebraic properties of exponentials. Since the defining property of the number e is e^\varepsilon = 1 + \varepsilon, we get e^x e^\varepsilon = e^x (1 + \varepsilon) = e^x + \varepsilon e^x. On the other hand, by the Kock-Lawvere axiom, f(x+\varepsilon) = e^{x+\varepsilon} = e^x + \varepsilon f'(x).
This gives us the equality \varepsilon f'(x) = \varepsilon e^x and therefore, by microcancellation f'(x)=e^x.
Qed.

4.3. What is the deal with \sqrt{\varepsilon}?

Now, what is the domain of the square root function? Negative numbers don’t have square roots, so the square root function has domain \{x \in \mathcal{R}|x = 0\:\:or\:\:x>0 \}. It is not true that \varepsilon > 0 (since that would imply \varepsilon^2 = 0 > 0). However, since \varepsilon is an arbitrary nilsquare infinitesimal, you can’t prove that \varepsilon = 0. Therefore, \varepsilon is outside the domain of the square root function, and \sqrt{\varepsilon} is undefined.

4.4. Infinitesimals don’t have reciprocals, so how does the quotient rule work?

This is a common source of confusion. Many people think that you cannot divide by g(x)^2, since the value g(x) may be an infinitesimal.

However, the quotient rule works only when the function in the denominator is non-zero (this is the same in ordinary real analysis). Fortunately, if x \neq 0, then you are free to divide by x (why? see Question 2.3).

5. Counterexamples to Classical Theorems

5.1. Can I prove the Extreme Value Theorem in SIA?***

To talk about the Extreme Value Theorem, we have to discuss the definition of the partial order on \mathcal{R}. We define x \geq a to mean the same thing as x = a \vee x > a. In this case, the Extreme Value Theorem is not merely unprovable, but explicitly false in SIA. Informally: we can’t tell if an infinitesimal is positive or negative, so we can’t find the maximum of a linear function with infinitesimal slope. Formally:

Thm. (neg-EVT) Not every function f:[0,1]\rightarrow\mathcal{R} attains its maximum.
Proof.
Assume that every such function attains a maximum. Choose an arbitrary infinitesimal \varepsilon^2 = 0. Then in particular the function f(x) = \varepsilon x attains its maximum at some m\in [0,1]. This means that for any x \in [0,1], \varepsilon m \geq \varepsilon x, and thus \varepsilon (m-x) \geq 0. As a special case, we have \varepsilon m \geq 0, so if m > 0, then \varepsilon \geq 0. Otherwise, m = 0, and thus -\varepsilon \geq 0. In both cases, since infinitesimals cannot be provably greater than zero, we get \varepsilon = 0.
Qea.

However, in the literature it is more common to let x \geq a denote the preorder given by the negation of x < a. In this case, the Extreme Value Theorem is still not provable. Can we actually prove neg-EVT in this case? I don’t know, but please contact me with any information.

5.2. Can I prove the Intermediate Value Theorem in SIA?

No. The Intermediate Value Theorem is false in Smooth Infinitesimal Analysis. There is an explicit counterexample (given in Bell’s book), but the proof is quite involved.


5.3. Can I prove the non-infinitesimal form of Taylor’s theorem in SIA?

Yes! Initially, most people think that this can’t be done. I certainly used to believe that, until I actually tried to prove it and realized that the simplest inductive argument goes through.

Thm. (Taylor’s theorem) Let f:[x,y]\rightarrow\mathcal{R}, \delta \in [0,y-x]. Choose any natural number n. Then we have \displaystyle{f(x+\delta) = \sum_{k=0}^n \frac{f^{(k)}(x)}{k!} \delta^k + \int_x^{x+\delta} \frac{f^{(n+1)}(t)}{n!} \delta^n dt}.
Proof.
Induction on n. The base case is n=0, which reduces to the identity f(x+\delta) = f(x) + \int_x^{x+\delta} f(t) dt = f(x) + f(x+\delta) - f(x). For the inductive case, notice that integration by parts on the error term produces the next term of the Taylor series and a higher order error term.
Qed.

6. Technical Stuff

6.1. Where can I find all the axioms of Smooth Infinitesimal Analysis?

The following three axioms are sufficient for a course in multivariable calculus or undergraduate differential geometry.

  1. Algebra. The real line \mathcal{R} is an Archimedean ordered field (its elements are called real numbers). Every positive real number has a square root, there is no polynomial of odd degree that has no roots, and every element of \in \mathcal{R} gives rise to a corresponding exponential function with the usual properties.
  2. Kock-Lawvere. Every function f:\{\varepsilon\in\mathcal{R}|\varepsilon^2=0\} \rightarrow\mathbb{R} is linear.
  3. Integration. Every function f:[0,1]\rightarrow\mathcal{R} has a unique antiderivative F:[0,1]\rightarrow\mathcal{R} such that F(0)=0. If the function f is positive, so is the antiderivative F.

For all twenty axioms, see the book Models of Smooth Infinitesimal Analysis (the additional axioms concern the general form of the Kock-Lawvere axiom, the properties of smooth natural numbers, non-standard analysis, and topology).

6.2. Is Smooth Infinitesimal Analysis constructive?

No. Like constructive mathematics, Smooth Infinitesimal Analysis is built on intuitionistic logic. However, SIA itself is not constructive. For example, the Kock-Lawvere axiom asserts that every smooth function has a slope, without giving us any construction (~ method of finding) of that slope. One may hope, and I personally believe that this is the case, that Smooth Infinitesimal Analysis will ultimately inspire a new constructive treatment of differentiability. For example,it seems that SIA is somehow related to numerical stability, so a constructive interpretation could potentially lead to type systems that can check the numerical stability of simulations, etc.

 

Footnotes

* Anachronistically, one can say that we introduce the real numbers to get rid of an annoying approximation process. Functions such as f : \mathbb{Q} \rightarrow \mathbb{Q} f(x) = x^2 - 2 have many “approximate” roots, but no exact roots, so we fill up the rationals with exact roots of all kinds of functions, yielding the real numbers \mathbb{R}. We could totally do analysis on \mathbb{Q}, but it would be a pain. For example, continuous functions of a rational variable on a closed interval are sometimes not uniformly continuous, but they are always “approximately” uniformly continuous.

The above (again, totally anachronistic) motivation for SIA does something similar: we have a zooming-in approximation process that we make exact by introducing some new numbers. At the risk of sounding controversial: doing Differential Calculus without the machinery of nilpotent infinitesimals is as much an artificial difficulty as doing Real Analysis without irrational numbers.

** Actually, in the constructive setting, the notion of field falls apart into two rather different notions. Weak fields have the law that “every non-zero element has a multiplicative inverse”, while strong fields also have the law that “every element is either zero or it has a multiplicative inverse”.

Leave a Reply

Your email address will not be published. Required fields are marked *