Derivation (¬¬A → A) → (¬¬B → B) → ¬¬(A ∧ B) → A ∧ B.

Question

I am struggling trying to make a derivation of this principle of indirect proof. Starting with the needed assumptions:

u: ¬¬A → A
v:¬¬B → B
w: ¬¬(A ∧ B)

I thought that in order to prove A ∧ B I will need to prove A and B separately first and then just use the introduction rule for ∧. But I did not find a proper way. Can anyone help me please with that? Is the choice of assupmtions unique?
Thanks in advance

Answer 1

Hint

We have to write the derivation:

$(¬¬A→A),(¬¬B→B),¬¬(A∧B) ⊢ A∧B$.

The conclusion will follow with three applications of $(\to \text {Intro})$ (called $\to^+$: page 10).

1. $(¬¬A→A)$ --- premise
2. $(¬¬B→B)$ --- premise
3. $¬¬(A∧B)$ --- premise
4. $¬A$ --- assumption [a]
5. $A∧B$ --- assumption [b]
6. $A$ --- from 5) by $(\land \text {Elim})$ [$\land^-$]
7. $\bot$ --- contradiction: from 4) and 6) [by def of negation, page 7 and $\to^-$]
8. $\lnot (A∧B)$ --- from 5) and 7) by $\to^+$ and def, discharging assumption [b]
9. $\bot$ --- contradiction: from 3) and 8)
10. $\lnot \lnot A$ --- from 4) and 9) by $\to^+$ and def, discharging assumption [a]

11. $A$ --- from 1) and 10) by $\to^-$.

Now repeat the same derivation with assumption $\lnot B$ in line 4) and you will have $B$.

Then:

$A \land B$ --- from the above by $\land^+$.