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