RAA elimination and inference a theory ?!

Question

Can somebody explain the why if we eliminate RAA rule in natural deduction system on propositional logic, why

~$(p \wedge $~$p)$ is not inference from the resulting system, but ~~ $p \to p$ can deduce from this.

any idea or hint for this type of question is so appreciated.

Answer 1

We assume the usual abbreviation : $\lnot p$ for $p \to \bot$.

Here is the proof of $\lnot (p \land \lnot p)$ :

1) $p \land \lnot p$ --- assumed [a]

2) $p$ --- by $\land$-elimination

3) $\lnot p$ --- by $\land$-elimination

4) $\bot$ --- from 2) and 3) by $\to$-elimination, with the abbreviation

5) $\lnot (p \land \lnot p)$ --- from 1) and 4) by $\to$-introduction and abbreviation, discharging [a].

The proof nowhere uses RAA.

---

The RAA rule, or rule for indirect proof, can be expresses as :

$${ \Gamma,\lnot \varphi \vdash \bot \over \Gamma \vdash \varphi }$$

and is equivalent to Double Negation : $\lnot \lnot p \to p$.

---

About : $(p∧ \lnot p) \to q$, we can derive it as follows :

1) $p∧ \lnot p$ --- assumed [a]

2) $p$ --- by $\land$-elimination

3) $\lnot p$ --- by $\land$-elimination

4) $\bot$ --- from 2) and 3) by $\to$-elimination

5) $q$ --- from 4) by $\bot$-rule

6) $(p∧ \lnot p) \to q$ --- from 1) and 5) by $\to$-introduction, discharging [a].

Neither this proof needs RAA.