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.

  • What exactly have you tried; where are you stuck?
    – user2953
    Oct 14, 2015 at 15:34
  • 1
    Double negation-elimination, folowed by Disjunction-elimination, followed by Double negation-introduction. Oct 14, 2015 at 16:05
  • 2
    (A or B) is the same as (B or A). After that, it doesn't matter what operations you apply to the result.
    – gnasher729
    Oct 14, 2015 at 20:47
  • 1
    By the way, this is a theorem in intuitionistic logic. You don't need double negation elimination.
    – Pseudonym
    Oct 15, 2015 at 0:21

2 Answers 2


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.

enter image description here


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/

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .