Deriving contradiction from $a\Leftrightarrow\neg a$

Question

Recently I've been trying to prove some things by strictly following deduction rules. I've been trying to derive incononsistency from unrestricted comprehension axiom via Russell's paradox. I have reached the point where we have $a\Leftrightarrow\neg a$, where $a:=R\in R$. However, I'm not quite sure how to follow from here - to show that this is inconsistent, I need to show, for some $b$, to derive both $b$ and $\neg b$. I can guess that $b=a$ in this case. One could try to do something of sort "assume $a$ and derive $\neg a$, and vice versa", but this doesn't show both of these true - it shows that neither is true.

To specify my question: given $a\Leftrightarrow\neg a$, now to derive $a$ using formal inference rules?

Answer 1

Reductio ad absurdum gives $(a\Rightarrow \neg a)\Rightarrow \neg a$. And so forth,

$(a\Leftrightarrow \neg a)\Rightarrow (\neg a\Rightarrow a)$

$( \neg a\Rightarrow a)\Rightarrow a$, due to reductio ad absurdum.

Answer 2

Adding a bit more detail to Lehs' response...

Prove $\neg a$:

Suppose to the contrary $a$. Then we must have $\neg a$ and we obtain the contradiction $a\land \neg a$. Therefore, we have $\neg a$.

Prove $a$:

Suppose to the contrary $\neg a$. Then we must have $a$ and we obtain the contradiction $a\land \neg a$. Therefore, we have $\neg\neg a$, or $a$.

As required, we have $a \land \neg a$.

Answer 3

This answer is just to remark that deducing a contradiction from $a\leftrightarrow\lnot a$ (which is short for $(a\to\lnot a)\land(\lnot a\to a)$) can be done using constructive (or intuitionistic) logic only, that is without using the excluded middle (or equivalently $\lnot\lnot a\to a$). The excluded middle would give, without any hypothesis, $a\lor\lnot a$, and together with $a\leftrightarrow\lnot a$ this easily gives a contradiction (consider both cases). But one does not need to proceed that way, nor use a proof by contradiction. The Russell paradox is valid constructively.

Note that in constructive logic $\lnot a$ is an abbreviation for $a\to\bot$, so it is allowed to prove $\lnot a$ by assuming $a$ and deriving a contradiction; this is basically the only way to prove $\lnot a$, and not a proof by contradiction. What is not allowed is proving $a$ by assuming $\lnot a$ and deriving a contradiction; that would only prove $\lnot\lnot a$.

Assume $H_1:a\to\lnot a$ and $H_2:\lnot a\to a$. First prove $\lnot a$ as follows: [assume $a$; with $H_1$ modus ponens gives $\lnot a$ which means $a\to\bot$; now with assumption $a$ again and modus ponens one gets $\bot$ as desired]; we have proved $\lnot a$. With this result and $H_2$, modus ponens gives $a$, and now with the result $\lnot a$ again, modus ponens leads to$~\bot$. This shows that $H_1\land H_2\to\bot$