Anyone can help me with proving ~(AvB) |- ~(BvA) via natural deduction?

Question

~(AvB)  
ㅡㅡㅡㅡ
~(BvA)

I have to provide a derivation to establish validation of this argument.

First of all, can I first change ~(AvB) into ~A&~B by using the De Morgan rules?

And the second is:

~(Av~(A&B))

I have to derive that this is a contradiction.

It seems hard because the entire argument is negated. I am not sure what to assume first.

Answer 1

Fact 1. ¬(A ∨ B) |= ¬(B ∨ A)

Proof. The negated form of the conclusion hints at an obvious way of proceeding: assume (B ∨ A) with the hope of deriving a contradiction. The disjunctive form of this assumption suggests the second step (proof by case analysis): assume B, derive some sentence Γ, then assume A and derive that Γ again; then using (B ∨ A) and those two derivations conclude Γ. Here's a way of applying those techniques:

1. ¬(A ∨ B) [ Given ]
2. (B ∨ A) [ Assumption ]
3. B [ Assumption ]
4. (A ∨ B) [ ∨-introduction, 3 ]
5. ⊥ [ ⊥-introduction, 4, 1 ]
6. A [ Assumption ]
7. (A ∨ B) [ ∨-introduction, 6 ]
8. ⊥ [ ⊥-introduction, 7, 1]
9. ⊥ [ ∨-elimination, 2, 3-5, 6-8 ]
10. ¬(B ∨ A) [ ¬-introduction, 2-9 ].

Fact 2. ¬(A ∨ ¬(A ∧ B)) ≡ ⊥

Proof. The combinatorial space is bigger here, given that you haven't specified what rules you are allowed to use and whether you are to prove this semantically, proof-theoretically, etc.. I'll sketch an algebraic variant here. We want to show that ¬(A ∨ ¬(A ∧ B)) ≡ ⊥. We can proceed as follows:

1. ¬(A ∨ ¬(A ∧ B)) ≡ ⊥ [ Goal ]
2. (A ∨ ¬(A ∧ B)) ≡ ⊤
3. (A ∨ (¬A ∨ ¬B)) ≡ ⊤ [ De Morgan ]
4. (A ∨ ¬A ∨ ¬B) ≡ ⊤ [ Associativity ]
5. (⊤ ∨ ¬B) ≡ ⊤
6. ⊤ ≡ ⊤.

Another method would be to use valuations (truth-tables). We want to show that v(¬(A ∨ ¬(A ∧ B))) = 0. The useful fact is: v(¬φ) = 1 - v(φ). We proceed as follows.

1. v(¬(A ∨ ¬(A ∧ B))) = 0 [ Goal ]
2. v(A ∨ ¬(A ∧ B)) = 1
3. v(A) = 1 or v(¬(A ∧ B)) = 1
4. v(A) = 1 or v(A ∧ B) = 0
5. v(A) = 1 or (v(A) = 0 or v(B) = 0)
6. (v(A) = 1 or v(A) = 0) or v(B) = 0
7. 1 or v(B) = 0
8. 1

This is pretty much the same as the one above. You can go with the one that's closest to the system you use. I didn't justify the steps because, as has been pointed out, we don't know what rules you can use.

Answer 2

Proving that a formula φ is a contradiction amounts to derive ⊥ from it (i.e. : φ ⊢ ⊥).

---

Proof :

(i) ~(Av~(A&B)) --- premise

(ii) ~A --- assumed [1]

(iii) A&B --- assumed [2]

(iv) A --- from (iii) by &-elim

(v) ⊥ --- from (ii) and (iv) by →-elim

(vi) ~(A&B) --- from (iii) and (v) by →-intro, discharging [2]

(vii) Av~(A&B) --- from (vi) by v-intro

(viii) ⊥ --- from (i) and (vii) by →-elim

(ix) A --- from (ii) and (viii) by RAA (or Double Negation), discharging [1]

(x) Av~(A&B) --- from (ix) by v-intro

(xi) ⊥ --- from (i) and (x) by →-elim

Conclusion :

~(Av~(A&B)) ⊢ ⊥

Answer 3

First of all, can I first change ~(AvB) into ~A&~B by using the De Morgan rules?

Well sure, you could use derived rules, however the most convincing natural deduction argument for this commutivity would use the fundamental rules of inference; thus showing that commutivity follows directly from the introduction rules having left and right side versions.

After all, if you used deMorgan's, you would then commute a conjunction before using deMorgan's again.   So since you do have to justify commutation either way, then you may as well do so without using any derived rules.

  1|_ ~(A v B)         : Premise
  2|   |_ B v A         : Assumption
  3|   |   |_ B          : Assumption
  4|   |   |  A v B      : Disjunction Introduction (3, Left)
   |   |   +
  5|   |   |_ A          : Assumption
  6|   |   |  A v B      : Disjunction Introduction (5, Right)
  7|   |  A v B         : Disjunction Elimination (2,3-4,5-6)
  8|   |  #             : Negation Elimination (1,7)
  9|  ~(B v A)         : Negation Introduction (2-8)

---

And the second is:

~(Av~(A&B))

I have to derive that this is a contradiction.

It seems hard because the entire argument is negated. I am not sure what to assume first.

Use the Law of Excluded Middle, assume A or ~A must be the case. To eliminate that disjunction to something usable, you have to introduce a disjunction and a negation of a conjunction.

  0|  A v ~A              : Axiom (L.E.M.)
  1|_ ~(A v ~(A & B))     : Premise
  2|   |_ A                : Assumption
  3|   |  A v ~(A & B)     : Disjunction Introduction (2, R)
   |   +
  4|   |_ ~A               : Assumption
  5|   |   |_ A & B         : Assumption
  6|   |   |  A             : Conjunction Elimination (5, R)
  7|   |   |  #             : Negation Elimination (4,6)
  8|   |  ~(A & B)         : Negation Introduction (5-7)
  9|   |  A v ~(A & B)     : Disjunction Introduction (8, L)
 10|  A v ~(A & B)        : Disjunction Elimination (0,2-3,4-9)
 11|  #                   : Negation Elimination (1,10)

Revision: This can be pruned down a bit.

  1|_ ~(A v ~(A & B))     : Premise
  2|  |_ A & B             : Assumption
  3|  |  A                 : Conjunction Elimination (2)
  4|  |  A v ~(A & B)      : Disjunction Introduction (3)
  5|  |  #                 : Negation Elimination (4,1)
  6|  ~(A & B)            : Negation Introduction (2-5)
  7|  A v ~(A & B)        : Disjunction Introduction (6)
  8|  #                   : Negation Elimination (7,1)

Answer 4

The following show ways to prove these arguments.

The first uses De Morgan Rules (DeM), conjunction elimination (E), conjunction introduction (∧I).

The goal of the first argument is to show that two sentences commute over the disjunction connective with a negation connective over the whole disjunction. This requires breaking the sentence into each disjunct and then recombining the sentences in the different order.

The second one uses De Morgan Rules (DeM), conjunction elimination (∧E), double negative elimination (DNE), and contradiction introduction (⊥I).

---

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/