# How do you prove B v A |- A v B?

I am having trouble with how to use the assumption, which I feel that I will need for this proof.

If any one can demonstrate or give hints for this proof, I would greatly appreciate it.

• @MolsStillHere: Please identify what proof system you are using, and what version of the axiom schema and rules of inference you have available – Graham Kemp Oct 24 '18 at 0:45

Let's discuss the intuitive meaning of B∨A. It means either B or A.

If that is the case then, writing any disjunct first or last should not truth functionally matter.

Now, let's go to the truth table:

```B A  (B∨A) (A∨B)
T T      T     T
T F      T     T
F T      T     T
F F      F     F
```

As you can see the corresponding truth values are identical and therefore, (A∨B)≡(B∨A).

• I made an edit which you may roll back or continue editing. I hope I got the formatting as you intended it. Welcome to this SE! – Frank Hubeny Oct 20 '18 at 21:11
• @FrankHubeny Thank you for the edit, That is precisely how I wanted it. – Bertrand Wittgenstein's Ghost Oct 20 '18 at 22:31

Here is a proof using Klement's proof checker and rules provided in forall x. These may or may not be adequate, but they offer one way to go about proving this. The premise or assumption is in line 1 and the conclusion or goal is in line 6. The proof checker starts off by writing the assumption for me. You would simply state it on line 1 if you are not using a proof checker. In the reference section is the link to the proof checker that I am using. You may use as well for future exercises as a way to check if your proofs are correct.

Since the premise is a disjunction (an "or" proposition), I need to consider two cases. The first case, "B", I considered in lines 2 and 3. The second case, "A", I considered in lines 4 and 5. I need to get the same result in both cases to invoke the disjunction elimination (∨E) rule, which I did on line 6. Note that I had to use the disjunction introduction (∨I) rule on lines 3 and 5. Since it did not matter which order I used I used the order I needed for the goal.

You may be required to use other rules or other names for the rules than the ones I used.

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/

• Hey Frank, unfortunately, I dont think I am allowed to use two subproofs in a row. Is there another way to go about proving this? – MoIsStillHere Oct 22 '18 at 5:12
• @MoIsStillHere This would be a Fitch-style proof checker. You may be asked to do this in a different way. What text are you using? Perhaps you can quote an example of how disjunction elimination or doing each case in an "or" statement is used. That is the pattern you would need to follow. – Frank Hubeny Oct 22 '18 at 10:22
• For instance, some authors require conditional introductions to follow the subproofs, and disjunction elimination then takes the form B v A, B -> (A v B), A -> (A v B) |- A v B – Graham Kemp Oct 23 '18 at 23:41
• @GrahamKemp True. The OP may have to modify the answer to fit what they are required to do. – Frank Hubeny Oct 24 '18 at 0:32