I found the following proof to be constructive:
- There is a bijection from $[0,1]$ to $(0,1]$. Have $0\mapsto \frac12, \frac12\mapsto\frac23,\frac23\mapsto\frac34,$ and so on. That
takes care of $\left\{0, \frac12, \frac23, \frac34,\ldots\right\}$.
For any other $x$, just map $x\mapsto x$.
This is from https://math.stackexchange.com/a/183383/1125430 .
However, it seems to be using the law of excluded middle $x\in \left\{0, \frac12, \frac23, \frac34,\ldots\right\}\vee x\notin \left\{0, \frac12, \frac23, \frac34,\ldots\right\}$ to define the function.
Is the above proof constructive?
Best Answer
This is not an acceptable proof in constructive mathematics, because it relies essentially on the law of excluded middle.
One can use your argument to construct a function with domain $P \cup [0,1]\setminus P$ and codomain $(0,1]$ where $P = \left\{0,\frac{1}{2},\dots \right\}$, and that in itself is an acceptable construction in constructive mathematics. But unfortunately you cannot show that $P \cup ([0,1]\setminus P) = [0,1]$ without using (a non-constructive instance of) the law of excluded middle.
You never actually write down an argument showing that the function you construct is a bijection -- and if you did, you'd find that showing this requires another use of the law of excluded middle.
In fact, using arguments that are acceptable in all flavours of constructive mathematics, it's not possible to construct a discontinuous function $[0,1] \rightarrow [0,1]$ at all! And the function you define above is clearly discontinuous (NB this is a very hard constraint for your problem: as an exercise, think about compact sets, and whether it's possible to have a continuous bijection between an open and a closed interval in classical mathematics.)