What does constructive mathematics say about limits?

Question

Suppose I want to construct a mathematical proof using constructive mathematics. Let's say I've reached a proof statement where I've shown that, say, x = 1/2 + 1/4 + 1/8 + ..., whereupon I would like to introduce the proposition, x = 1. Clearly, this would be allowed in conventional mathematics, but are limits considered valid in constructive mathematics? That is, is there a constructive proof that this infinite sequence converges, given that it is an infinite series? (Is an infinite series constructible?) Please take into account that I'm just a novice when it comes to constructive mathematics.

Answer 1

Yes, limits are valid in constructive mathematics.

The statement $\lim\limits_{n \to \infty} a_n = x$ is, as usual, defined to mean $\forall \epsilon > 0 \exists N \in \mathbb{N} \forall n \in \mathbb{N} (n \geq N \implies |a_n - x| < \epsilon)$.

It can be shown constructively that $\lim\limits_{n \to \infty} \frac{1}{2^n} = 0$. For consider some $\epsilon > 0$. Then take $N \in \mathbb{N}$ such that $\frac{1}{\epsilon} < N$. Now consider some $m > N$. Then $0 < \frac{1}{\epsilon} < N < m < 2^m$, so therefore $0 < \frac{1}{2^m} < \epsilon$. Thus, $|\frac{1}{2^m} - 0| < \epsilon$.

Notice that only constructive logic was required to do this proof. Similarly, only constructive logic is required to show that $1/2 + 1/4 + ... + \frac{1}{2^n} = 1 - \frac{1}{2^n}$. This can be done easily by induction.

So we see that $\sum\limits_{n = 1}^\infty \frac{1}{2^n} = \lim\limits_{n \to \infty} 1 - \frac{1}{2^n} = 1 - \lim\limits_{n \to \infty} \frac{1}{2^n} = 1 - 0 = 1$.

Note that in the absence of a very weak form of countable choice known as $AC_{0, 0}$, a second, stronger definition of limit is sometimes required. This definition is: $\lim\limits_{n \to \infty} a_n = x$ if and only if there exists a function $f : \mathbb{N} \to \mathbb{N}$ such that for all $n > 0$, for all $m > f(n)$, $|a_m - x| < \frac{1}{n}$. This stronger definition implies the weaker definition, but not necessarily vice versa.

Answer 2

The situation where limits get problematic in a constructive treatment is if the speed of convergence is not known. For very concrete examples such as yours, the speed of convergence is obviously known, and everything is fine.

Lets construct an example of a sequence which is converging classically but not constructively (for most flavours of "constructive").

Let $a_t := \sum_{\{n \in \mathbb{N} \mid \text{the $n$-th TM halts in at most $t$ steps}\}} 2^{-n}$. This is a computable sequence of reals. This sequence clearly is monotonely increasing and bounded above by $2$. Classically, this would mean that it converges. However, if we knew its (classical) limit $a_\infty := \sum_{\{n \in \mathbb{N} \mid \text{the $n$-th TM halts}\}} 2^{-n}$, we could solve the Halting problem. Hence, $a_\infty$ is not a computable real -- hence $(a_t)_{t \in \mathbb{N}}$ doesn't converge in a constructive sense.

In case you aren't familiar with Turing machines yet: Unfortunately, there isn't a good way around them to get decent counterexample to stuff being constructive.

Answer 3

The difference between classical and constructive definition is that you are not taking for granted, using the fact that it is as close as you want to $1$, that

$$\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+\frac{1}{16}+\frac{1}{32}...=1$$

Constructively, you are saying that you want to know if this has any sense:

$$\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+\frac{1}{16}+\frac{1}{32}...+\frac{1}{2^n}=1$$

because that is the best you can do. Now, purely constructively, you say, ok I want this to be close to $1$ by $\epsilon$. And now you find that if you take

$$n=\ln_2(\frac1{\epsilon})$$

you are right there since

$$\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+\frac{1}{16}+\frac{1}{32}...+\frac{1}{2^n}=1-\frac{1}{2^n}=1-\epsilon$$

Since, by this construction, you can get as close as you specifically(!) wish, you consider these expressions equal. Notice that in constructive math it is not exactly about the expression itself, it is about the process. Both of these together are $1$

$$f(n)=\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+\frac{1}{16}+\frac{1}{32}...+\frac{1}{2^n}, g(n)=n$$

This is to say: since I can select always a specific natural number by which I am getting close to $1$ by any predefined distance, I consider this equal to $1$ (because there is no difference between them which you could fix in advance and call it the difference between $1$ and the expression. If you do, I can use the above expression and quickly calculate which $n$ to take and disprove that difference of yours).

In constructive math, you never get into some classical realm of meta, you are firmly routed into procedural steps of getting from one point to another.

Answer 4

I am especially confused by references in the provided answers to Turing machines, as that is what prompted my question in the first place. As I understand it, the sum 1/2 + 1/4 + 1/8 + 1/16 + … cannot be constructed on a Turing machine in a finite number of steps. Suppose we agree that a mark at a certain tape location stands for 1/2, and a mark one place to its right stands for 1/4, and the mark to its right 1/8, ad infinitum. It would take the entire right-hand side of the Turing machine tape to represent the infinite-precision real number corresponding to the sequence, and an infinite sequence of steps merely to construct the sequence, to say nothing of the program necessary to conclude that the sum was equal to 1. Given that the sum is therefore not constructible on a Turing machine, I assumed (possibly incorrectly) that it was not allowable in constructive mathematics.