If a proposition can be proved nonconstructively, does a constructive version of it also hold?

Question

In this question, I define as follows.

• A sequence $\{a_n\}_{n\in\mathbb{N}}$ constructively converges to $a$ if there is a function $N:(0, \infty)\to\mathbb{N}$ such that $\forall \varepsilon>0, \forall n>N(\varepsilon), |a_n-a|<\varepsilon$ holds.
• A function $f:\mathbb{R}\to\mathbb{R}$ is constructively continuous if there is a function $\delta:\mathbb{R}\times (0, \infty)\to(0,\infty)$ such that $\forall x\in\mathbb{R}, \forall \varepsilon >0, \forall y\in\mathbb{R}, (|x-y|<\delta(x, \varepsilon)\Rightarrow |f(x)-f(y)|<\varepsilon)$.

(Added later: In the above, it turned out that "function" should be replaced by "computable function". )

Similarly, “constructively uniformly continuous”, “constructively differentiable”, “constructively integrable”, etc… can be defined. To do that, we rephrase the existential quantifier as the existence of a function.

Theorem If $\{a_n\}_{n\in\mathbb{N}}$ constructively converges to $a$ and $f:\mathbb{R}\to\mathbb{R}$ is constructively continuous, then $\{f(a_n)\}_{n\in\mathbb{N}}$ constructively converges to $f(a)$.

The above can be said to be a ”constitutive version” of the following.

Theorem If $\{a_n\}_{n\in\mathbb{N}}$ converges to $a$ and $f:\mathbb{R}\to\mathbb{R}$ is continuous, then $\{f(a_n)\}_{n\in\mathbb{N}}$ converges to $f(a)$.

In general, theorem X is the constructive version of theorem Y, if all the terms in Y are rephrased as “constructive~” in X.

Is there a theorem that says, "If a theorem holds, then its constructive version holds," or something similar?

We do not assume the axiom of choice here.

Answer 1

As Zhen Lin has mentioned in the comments, as written your notion of "constructive ______" agrees with the usual version (which you would likely call "nonconstructive ______"). This is basically because functions, as we usually define them, don't have to be "definable" in any sense. So the fact that, "nonconstructively" we have a witness to $|a_n - a| < \epsilon$ mean we can simply define a function to be a (choice of) witness!

However, all of this changes if you ask for these functions to be "Computable" (in the sense that it's represented by some computer program) then your definitions do become more in line with what someone might call "constructively continuous", etc. This is almost surely what you meant anyways, since the class of functions that a program can compute are a good analogue for the class of functions which you can actually "write down and work with". I'll use the more standard terminology of "computably continuous" instead of "constructively", going forwards, and I'll answer your question in the case that we want all of our witnesses to be computable.

Once you do this, there are theorems that say "computably uniformly continuous" implies "computably continuous" in your sense. And in fact, as you suspect, there are "metatheorems" saying that many theorems automatically have a "computable" analogue. As long as your reasoning is constructive (by which I mean you don't use the law of excluded middle or the axiom of choice -- though some weak variants like countable choice are allowed) then it holds in the "effective topos". This is an alternate universe where everything has a computable witness (unless you specify that it doesn't), and your constructions turn preexisting computable witnesses into new computable witnesses. Working in the effective topos lets you handle this plumbing automatically, so that you're guaranteed that your theorems always end up with computable content!

---

I hope this helps ^_^

Answer 2

I will assume your question has nothing to do with constructive mathematics as it is usually defined. Your definition of "constructively converges" is practically useless in this context (although perhaps your definition of "constructively continuous" does have some uses).

It turns out that even without the axiom of choice, your notions of constructive convergence and continuity are equivalent to their ordinary versions. To see this, note that your definitions clearly imply the ordinary versions. To go the other way, we begin by discussing "constructive convergence".

Suppose $\lim\limits_{n \to \infty} a_n = a$. Define $N(\epsilon)$ to be the smallest $j$ such that for all $n > j$, $|a_n - a| < \epsilon$ (at least one $j$ exists by the definition of $\lim$). This shows that $\{a_n\}_{n \in \mathbb{N}}$ constructively converges to $a$.

Similarly, suppose $f : \mathbb{R} \to \mathbb{R}$ is continuous. Fix a surjection $q : \mathbb{N} \to \mathbb{Q}$, so that $\mathbb{Q} = \{q_n \mid n \in \mathbb{N}\}$. Suppose we have some $x$ and $\epsilon$. Then take some $\delta > 0$ such that for all $y \in \mathbb{R}$, if $|y - x| < \delta$ then $|f(y) - f(x)| < \epsilon$. Note that any $\delta' \in (0, \delta)$ satisfies exactly the same property. And note there exists a rational number in $(0, \delta)$ by the Archimedean property and the fact that $\delta > 0$, which can be written as $q_n$ for some $n$. So there exists some $n$ such that $\forall y \in \mathbb{R}(|y - x| < q_n \implies |f(y) - f(x) < \epsilon)$. Take the smallest such $n$, and let $\delta(x, y) = q_n$. Then $f$ is constructively continuous.