3
$\begingroup$

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.

$\endgroup$
4
  • 3
    $\begingroup$ $\frac{1}{2}+\frac{1}{4}+\frac{1}{8}+\dots=\sum\limits_{n=1}^\infty \frac{1}{2^n} = \lim\limits_{N\to\infty}\sum\limits_{n=1}^N\frac{1}{2^n}$. This expression on the far right should still be well understood and although $\infty$ appears in the notation, no infinite quantities are involved in the meaning. $\endgroup$
    – JMoravitz
    Commented Aug 4, 2021 at 18:11
  • 2
    $\begingroup$ You should mention which system of "constructive mathematics" you are using. See, for example, E. Bishop, Foundations of Constructive Analysis. $\endgroup$
    – GEdgar
    Commented Aug 4, 2021 at 18:13
  • 1
    $\begingroup$ You may be interested in the book "Reverse Mathematics Proofs from the Inside out" by John Stillwell. Here is a link to one book seller biggerbooks.com/reverse-mathematics-stillwell-john/bk/… $\endgroup$
    – Jay
    Commented Aug 4, 2021 at 18:40
  • 1
    $\begingroup$ From what little I know about these things, I would think that your example would not be provable in a framework of finitism or ultrafinitism, which is different from constructivism. $\endgroup$
    – user13618
    Commented Aug 5, 2021 at 4:18

4 Answers 4

10
$\begingroup$

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.

$\endgroup$
0
9
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ I am familiar with Turing machines. Thank you for your clear analysis. $\endgroup$ Commented Aug 4, 2021 at 19:56
  • 1
    $\begingroup$ @StephenMorgan If you found my answer helpful, please upvote it (grey arrow pointed up on the left), and do the same for the other good answers. If there is an answer fitting your needs best, you can accept it by selecting the checkmark. $\endgroup$
    – Arno
    Commented Aug 4, 2021 at 20:03
  • $\begingroup$ Precisely: constructive sense is not able to decide if it converges or not. It does not mean it does not converge because then we would have some information about Turing machines. We have none. $\endgroup$
    – user953399
    Commented Aug 5, 2021 at 17:39
  • $\begingroup$ @AlexPeter Its meant to be read "doesn't (converge in a constructive sense)" not "(doesn't converge) in a constructive sense". For the latter statement it matters a lot what framework we use. Eg BISH will sit on the fence regarding convergence, whereas Russian constructivism can prove that the sequence doesnt converge. $\endgroup$
    – Arno
    Commented Aug 6, 2021 at 14:12
0
$\begingroup$

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.

$\endgroup$
0
-2
$\begingroup$

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.

$\endgroup$
13
  • 1
    $\begingroup$ There is a difference between "Turing Machines" and "constructive Math". Constructive math is achieved by using a different logical system for doing mathematical proofs; one that does not use the law of excluded middle (but there are even different flavors of constructivism as mentioned by Arno). Turing machines are a model of how computation works, and this model can be defined/described in ordinary classical math or constructive math. Talking about Turing machines does not automatically mean you are working in constructive mathematics. $\endgroup$
    – Léreau
    Commented Aug 14, 2021 at 6:44
  • $\begingroup$ In this case it means that to constructively show that your mentioned sum converges to $1$, there is no reason to bring Turing machines into the discussion. We only need to make sure that the proof only uses constructive logic. $\endgroup$
    – Léreau
    Commented Aug 14, 2021 at 6:47
  • $\begingroup$ According to the Internet Encyclopedia of Philosophy, “Constructive mathematics is often mis-characterized as classical mathematics… without the Law of Excluded Middle” (see iep.utm.edu/con-math). While I agree that CM excludes the LEM, I believe that follows from the definition of CM, that every term of every proposition introduced be construtible (ibid). Classical mathematics without LEM allows one to reach conclusions that are not provable according to the constructive definition. The sum in question does not seem to be constructible on a Turing machine, so not introducible. $\endgroup$ Commented Aug 14, 2021 at 12:44
  • $\begingroup$ Yes, the "logic without LEM" is a simplified, very incomplete description, but a good way to give the jist of it. Your description does indeed strongly point to there being no Turing machine computing the result of the series. The point is however that CM can prove that the series converges and Turing machines play no role in that proof. $\endgroup$
    – Léreau
    Commented Aug 14, 2021 at 15:48
  • 1
    $\begingroup$ At this point I can just refer you back to the answer by @MarkSaving. He describes the series in constructive mathematics and shows why we can still prove that it converges to $1$. $\endgroup$
    – Léreau
    Commented Aug 16, 2021 at 6:02

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .