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 '15 at 15:34
  • 1
    Double negation-elimination, folowed by Disjunction-elimination, followed by Double negation-introduction. – Mauro ALLEGRANZA Oct 14 '15 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 '15 at 20:47
  • 1
    By the way, this is a theorem in intuitionistic logic. You don't need double negation elimination. – Pseudonym Oct 15 '15 at 0:21

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/

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.