# $\left( \lnot a \implies a \right) \stackrel{?}{\implies} a$

Consider the following axiom:

$$\lnot a \implies a$$

Intuitively, this seems like a contradiction. But all implications hold if the LHS is false. Does this mean that:

$$a$$

is a valid conclusion? Or is there a contradiction in the axiom?

-
Suppose $\neg a$. Then as $\neg a \to a$, by modus ponens, $a$ holds, a contradiction. Therefore $a$. – martini Jun 5 '12 at 14:32
The alternative wasn't $\lnot a$, but a contradiction in the axiom system. (But maybe an axiom can't contradict itself?) – Johan Jun 5 '12 at 14:34
If you take $\neg a \to a$ as an axiom, you take it as true. It is possible for an axiom to be contradictory, IIRC, but then all formulae are valid conclusions. (Your's isn't and $a$ is a valid conclusion). – martini Jun 5 '12 at 14:36

However, you can simplify the expression symbolically before. $\lnot a \implies a$ is logically equivalent to $\lnot(\lnot a)\lor a$, which is $a$. Hence your formula is just $a \implies a$, which is more obviously a tautology.
It is only "obviously" a tautology if we already know $\neg \neg a \Leftrightarrow a$. On the other hand, if we start from intuitionistic logic, then ($(\neg a \Rightarrow a) \Rightarrow a)$ for all $a$) is logically equivalent to ($\neg\neg a \Leftrightarrow a$ for all $a$). Either is a possible axiom that can be added to intuitionistic logic on order to make it classical. – Henning Makholm Jun 5 '12 at 14:55
$a \implies b$ is equivalent to $\neg a \vee b$ so $\neg x \implies x$ implies $\neg \neg x \vee x$ which, unless we are working with constructive logic, implies $x$. This means that $(\neg x \implies x) \implies x$ is an axiom. $\neg x \implies x$, however, is not. Just take $x = 0$ and see that $1 \implies 0$ is false.