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.
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].
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.
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/