Modus Tollens and Limit Definition In intro Real Analysis,limits at $c$ are proved in reverse order of the definition. You want to find a $\delta$ so that $|x-c|<\delta \implies |f(x)-L|<\epsilon$. To find that $\delta$, you usually work in the opposite direction. Assume $|f(x)-L|<\epsilon$. By algebraic manipulations deduce a minimum of $|x-c|$ in terms of $c$, and $\epsilon$. Then chose $\delta$ as a function of $\epsilon$ less than that minimum. Finally demonstrate that if $|x-c|<\delta$, then $|f(x)-L|<\epsilon$.
I was wondering if you could cut the work in half with Modus Tollens.
The definition is $\forall \epsilon>0, \exists \delta>0$ so that $ |x-c|<\delta \implies |f(x)-L|<\epsilon$.
Modus Tollens would have $\forall \epsilon>0, \exists \delta>0$ so that $|f(x)-L|\ge \epsilon \implies |x-c|\ge\delta$
I find this variation more intuitive and more suggestive of the proof process. It has potential for cutting the work in half, yet it doesn't seem to appear in text books. Is there a reason to avoid it?
EXAMPLE
Suppose you want to prove $\lim_{x \to 1} \frac{1}{x+1}=1/2$.
METHOD A:
$|\frac{1}{x+1}-1/2|=|\frac{1-x}{2(x+1)}|$
We want $|\frac{1-x}{2(x+1)}|<\epsilon$. If we restrict $x\in [0,2]$ the minimum of $2\epsilon(x+1)$ is $2\epsilon$. So we are motivated to let $\delta=$ min ( 1,$2\epsilon$).
$|x-1|<2\epsilon\implies 2-2\epsilon<x+1<2+2\epsilon\implies \frac{1}{2}(1-\epsilon)<\frac{1}{1+x}<\frac{1}{2}(1+\epsilon)$
$\implies -\epsilon/2<\frac{1}{x+1}-\frac{1}{2}<\epsilon/2$
So the chosen value of $\delta$ indeed yields the result.
METHOD B
Suppose $|\frac{1-x}{2(x+1)}|\ge \epsilon$
Then $|x-1|\ge  2(x+1)\epsilon$ force $|x-1|<1$, as above,  then the minimum value on the right is $2\epsilon$, thus $|x-1|>2\epsilon$.
We have proven $|f(x)-L|\ge \epsilon \implies |x-c|\ge2\epsilon$
By Modus Tollens then $|x-c|< 2\epsilon\implies |f(x)-L|<\epsilon$
So the existence of the minimum alone proves the limit. No need to formally prove $|x-c|<\delta \implies ...$
The methods are similar. In the first method, you do the scratch work, then prove the deduced value of $\delta$ works. In the second method, the scratchwork itself is the proof.
 A: (Too long for a comment)
Of course one can prove a proposition by contrapositive.
I think you overestimate the "savings". Usually, the chain of reasoning that leads from $|f(x)-L|\lt\epsilon$ to $0\lt|x-a|\lt \delta$ is via equivalences/biconditionals, so that one does not need to "unwound" the process to get to the valid result, any more than most (but not all) methods of solving an equation by algebraic manipulation (which technically are also a kind of 'analysis' in the sense of Pappus).
However, I would point out that the standard definition accurately captures the intuition of the meaning of $\lim_{x\to a} f(x)=L$, while the contrapositive, although logically equivalent, runs into the Black Raven paradox. Essentially we are saying "anything that does not land close to $L$ was not close to $a$ to being with", and that really sounds like "every non-black object is a non-raven." It seems somewhat unsatisfying, even if it is logically equivalent.
Your example is eliding some of the difficulties in the second method. I think that in the end, you would end up with a similar-length proof if written out in full.
A: There is a small mistake actually. When one considers the limit of function $f(x)$ at point $a$ the $f(x)$ may not be defined at $a$, that is why we need to take the deleted neighborhood, i.e. the correct definition would be $$\forall \varepsilon>0 \ \exists \delta>0 \ \forall x\in D(0<|x-a|<\delta) \Rightarrow |f(x)-L|<\varepsilon ,$$ where $D$ is the domain of $f(x)$.
