Sequential characterization of continuity - Is proof by contradiction unavoidable?

I have a question that's been bothering me lately.

Theorem. Let $$f:X\rightarrow Y$$ be a map between metric spaces. Then $$f$$ is continuous at $$x_{0}$$ if and only if $$x_{n}\rightarrow x_{0}$$ always implies $$f(x_{n})\rightarrow f(x_{0})$$.

Here is the standard proof that I'm aware of.

Proof. $$(\implies).$$ Let $$(x_{n})$$ be a sequence in $$X$$ that converges to $$x_{0}$$. Let $$\epsilon > 0$$. By continuity of $$f$$, there exists $$\delta > 0$$ such that $$d(x, x_{0}) < \delta \quad \implies\quad d(f(x), f(x_{0})) < \epsilon.$$ By convergence of our sequence, choose $$N\in\mathbb{N}$$ such that $$n\ge N$$ implies $$d(x_{n}, x_{0}) < \delta$$. Then the above implies $$n\ge N \quad \implies \quad d(f(x_{n}), f(x_{0})) < \epsilon,$$ and so $$f(x_{n})\rightarrow f(x_{0})$$.

$$(\impliedby).$$ For this, we will prove the contrapositive. Assume $$f$$ is not continuous at $$x_{0}$$. Then there exists $$\epsilon > 0$$ such that for all $$\delta > 0$$, there exists some $$d(\tilde{x}, x_{0}) < \delta$$ that has $$d(f(\tilde{x}), f(x_{0}))\ge \epsilon$$.

We use this to construct the following sequence. For $$\delta = \tfrac{1}{n}$$ we choose $$x_{n}$$ to be the element such that $$d(x_{n}, x_{0}) < \tfrac{1}{n}$$ but $$d(f(x_{n}), f(x_{0}))\ge\epsilon$$. Then we have $$x_{n}\rightarrow x_{0}$$ but $$f(x_{n})\not\rightarrow f(x_{0})$$. $$\;\square$$

For the backwards direction, we used the contrapositive, which boils down to proof by contradiction, as far as I'm aware. Usually I'm okay with these kinds of proofs, but I find it strange that we need to use proof by contradiction. I can't seem to find a proof that doesn't rely on contradiction here.

My Attempt

Suppose $$x_{n}\rightarrow x_{0}$$ always implies $$f(x_{n})\rightarrow f(x_{0})$$. Let $$\epsilon > 0$$.

I want to show that there exists $$\delta > 0$$ such that $$d(x, x_{0})<\delta$$ implies $$d(f(x), f(x_{0}))<\epsilon$$.

Perhaps I can consider the set of all possible sequences $$S = (x_{n})$$ for which $$d(x_{n}, x_{0}) < \tfrac{1}{n}$$. By hypothesis, each sequence $$S$$ has an index $$N_{S}$$ for which $$n\ge N_{S} \implies d(f(x_{n}),f(x_{0}))<\epsilon$$. By the well-ordering principle, we may take $$N_{S}$$ to be the least such natural number for $$S$$.

Let's say I take $$\delta = \inf \tfrac{1}{N_{S}}$$ (where the infimum is over all those $$S$$). What exactly prevents us from having $$\delta = 0$$?

I see that every sequence $$S$$ has $$N_{S}$$, but if there are uncountably many possible $$S$$, it feels as though you can choose some contrived sequence that gets closer and closer to $$x_{0}$$ but has nonetheless an arbitrarily large $$N_{S}$$.

My Questions

My main question is, is the use of the law of non-contradiction unavoidable? Is there a convincing argument one way or the other?

• Your proof uses the well-ordering principle. I wonder its use can be justified. Nov 5, 2017 at 5:28
• According to an article by Ishihara, even the equivalence of two concepts over separable metric spaces requires a non-trivial assumption, which is not basically assumed in the constructive mathematics. Nov 5, 2017 at 5:34
• @HanulJeon That's really interesting. Nov 5, 2017 at 7:16
• Possible duplicate of math.stackexchange.com/questions/1312873/… Nov 5, 2017 at 7:42

Notice that the contrapositive is not the same as a 'proof by contradiction'.

Say we wish to prove $P$. In a proof by contradiction, we first assume $\neg P$, and then deduce $\neg Q$. However, we know that $Q$ holds from before our assumption of $\neg P$. This is the contradiction, and therefore, our assumption of $\neg P$ must be incorrect; in other words, $P$ must hold.

The contrapositive shows up when proving implications. Its essence is the observation that

$$(P \implies Q) \iff (\neg Q\implies\neg P),$$

that is, proving that '$P$ implies $Q$' is logically equivalent to proving that 'the negation of $Q$ implies the negation of $P$'.

• I see; I admit that I brushed over this detail a little too fast. However, doesn't the contrapositive require proof by contradiction to be proven? I don't see how this changes things. Nov 5, 2017 at 5:47
• @SpiralRain You are correct. The $\impliedby$ direction is equivalent to double negation elimination. Simply pick $P\equiv\top$ and assume $\neg Q\equiv(Q\Rightarrow \bot)$. Nov 5, 2017 at 9:07
• The proof of the contrapositive does not rely on contradiction. It is a mere symbolic manipulation/rewriting of $P\implies Q$ after noting that it is logically equivalent to $\neg P \lor Q$. See this link. Nov 5, 2017 at 14:40
• @Fimpellizieri Showing that $P\Rightarrow Q$ is logically equivalent to $\neg P \lor Q$ relies on contradiction. Simply choose $Q=P$ and you get $P\Rightarrow P$ which is surely true even constructively, and $\neg P\lor P$ which is the law of excluded middle. Nov 5, 2017 at 17:37
• @Fimpellizieri My assumption is the question isn't: "How can I superficially rewrite my proof to not use proof by contradiction but an equivalent principle?", but is more like: "Can this be proven constructively? if so, how?" If my assumption is correct, no amount of manipulation of generic classical propositional formulas is going to help. Nov 5, 2017 at 18:38