In an indirect proof, is it possible to reject the assumption based on contradiction of a premise?

Question

If we have a premise, $x \in A$, is the following a correct use of RAA?

Suppose $x \in A$:

Assume P:

...

Derive $x \notin A$

Therefore not P.

Can we correctly reject P if we find a contraction against the premise when assuming P?

Answer 1

This is a proof that $x\in A \implies \neg P$. It can be simplified, since everything between "Assume $P$" and "Derive $x\not\in A$" is just a proof that $P\implies x\not\in A$, from which by contrapositive we get $x\in A \implies \neg P$, which was to be demonstrated.

You can't in general conclude from this that $P$ is always false, of course.

Answer 2

Yes. Deriving a contradiction from the assumption of $P$ is a proof for $\neg P$.

Although apparently similar, this is not actually Reduction ad Absurdum.

This is the Rule of Negation Introduction.   Unlike RAA this is an intuitionistically valid rule of inference. $$\dfrac{\Sigma,P\vdash \bot }{\Sigma\vdash \neg P}{\sf\small\neg I}$$

---

RAA consists of Negation Introduction and Double Negation Elimination. The later rule is not considered valid under an intuitionistic proof system.$$\dfrac{\dfrac{\Sigma, \neg P\vdash \bot}{\Sigma\vdash\neg\neg P}{\small\neg\sf I}}{\Sigma\vdash P}{\small\neg\neg\sf E}$$