natural deduction problem using the connective not

Question

I am having problems understanding how the connective not works in natural deduction. We were given the below example but I cannot workout how the lecturer got the values in table. If someone could explain how the result was derived I would really appreciate it.

   ¬¬p |- p

1     ¬¬p            ass 0
2     ¬p |- ¬p ∧ ¬¬p
2.1   ¬p             ass 2
2.2   ¬p ∧ ¬¬p       ∧-I 2.1, 1
3     p              ¬-E 2

Answer 1

As in your previous post, line 2) states that the following lines 2.1-2,2 are a sub-proof of:

$\lnot p \vdash \lnot p \land \lnot \lnot p$.

The sub-proof is:

2.1) $\lnot p$ --- assumed

2.2) $\lnot p \land \lnot \lnot p$ --- from 1) and 2.1) by $\land$-introduction.

Now, we have a contradiction (often symbolized with: $\bot$) that has been derived from 1) $\lnot \lnot p$ and 2) $\lnot p$.

But now we are in trouble ...

The $\lnot$-E rule allow us to derive a formula whatever from a contradiction; see Jan von Plato, Elements of Logical Reasoning (2013), page 48.

But in this way, we cannot discharge the assumption 2) $\lnot p$.

In order to discharge it, we have to use Double Negation [see von Plato, page 81], but this is exactly what we are trying to prove.