How to prove ¬¬(A ∨ B) leads to ¬¬(B ∨ A)?

Question

Using laws of natural deduction, how can one prove that the single premise ¬¬(A ∨ B) leads to ¬¬(B ∨ A)?

I have tried solving the problem for some time but to no avail.

Answer 1

Proof in Natural Deduction, avoiding Double negation-elimination (thus, the derivation is intuitionistically valid) :

1) ¬¬(A ∨ B) -- premise

2) ¬(B ∨ A) --- assumed [a]

3) A ∨ B --- assumed [b]

4) A --- assumed [b1] for ∨-elimination

5) B ∨ A --- from 3) by ∨-introduction

6) B --- assumed [b2] for ∨-elimination

7) B ∨ A --- from 5) by ∨-introduction

8) B ∨ A --- from 3), 4)-5) and 6)-7) by ∨-elimination, discharging assumptions [b1] and [b2]

9) ⊥ --- from 2) and 8) by ¬-elimination

10) ¬(A ∨ B) --- from 3) and 9) by ¬-introduction, discharging [b]

11) ⊥ --- from 1) and 10) by ¬-elimination

12) ¬¬(B ∨ A) --- from 2) and 11) by ¬-introduction, discharging [a].

Answer 2

The following proof used negation introduction (¬I) by assuming the negation of the conclusion represented as having one less negation connective.

To break the terms into simpler sentences, I used the DeMorgan Rule (DeM) to express the negation of a disjunction as a conjunction of negated sentences and then conjunction elimination (∧E) broke that into the component sentences. I recombined those sentences in the desired order using conjunction introduction (∧I).

Using the DeMorgan Rule again introduced a contradiction (⊥I) with the premise on line 1 which allowed me to introduce a negation (¬I) on line 9.

For more detailed information on these rules see forall x: Calgary Remix.

---

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/