Natural Deduction - AvB |- BvA

[temp_tsun]

Introduction

Hello, I have some problems proving the following problem: "AvB |- BvA". I would like to prove this by using natural deduction only. (I know it is possible proving it using truth tables).

Syntaxis

To avoid confusion I will use the following syntaxis to show my problem.
- Capital letters are used for variables.
- Instead of the mathematically symbols like "v" which means OR, I will use OR (all capital to substitute the mathematical symbols (few examples: (A AND B), (NOT(A))).
- I use something that I would like to call a diagram proof and hopefully you can explain how to do it using my familiar proof technique. I will demonstrate some below.
- I use |- to represent the mathematical symbol. It means: "When a conclusion C is derived from a set of assumptions {A1, A2, A3, ... , An} we write {A1, A2, A3, ... , An} |- C".
- When discharging a assumption I prefer to use [A] arround the proposition.


Diagrams

Note: I will use dots to represent spacings.
Note: I will use as much brackets as I can to make everything clear.

{A AND B} |- (B AND A)

(A.AND.B)...(A.AND.B.)...(Assumption)
----------...---------
...B......A... (by AND elimination)
--------------------------
....B.AND.A.....(by AND introduction)

(please also add the rules used when explaining to me)

Problem Statement

Prove using natural deduction: (A OR B) |- (B OR A)

The attempt at a solution

Using proof by contradiction:
..............[NOT(B.OR.A)]...(Assumption)
............-------------------
AvB...[NOT(A)]....(Assumption)...NOT(B).AND.NOT(A).(Rewrite)
-----------------.........--------------------
.B.............NOT(B).....(AND elimination)
-------------------------------------------------------------------
.......(B.AND.NOT(B)).........(AND introduction)
--------------------------------------------------------------------
.......FALSE..........
--------------------------------------------------------------------
.........(B OR A).......(Proof by contradiction)

Is this correct? Because I've the feeling I'm missing something.

Questions

A few questions about natural deduction itself.
- Can I use every assumption as long I discharge them later in the proof? (except for those that are already given in the excersize?

Thanks for explaining everything.

Greetings TKM

 

[KataKoniK]

Dear TKM,

Thank you for your forum post. It's great to see that you are trying to prove the statement (A OR B) |- (B OR A) using natural deduction.

Your attempt at a solution is a good start, but there are a few things that need to be clarified. First, in natural deduction, we usually use the symbol "⊢" to represent the turnstile, instead of "⊣". This symbol is used to indicate that we are proving a statement from a set of assumptions. So, in this case, we would write (A OR B) ⊢ (B OR A).

Next, when using proof by contradiction, you need to start by assuming the opposite of what you are trying to prove. In this case, you want to prove (B OR A), so you need to assume NOT(B OR A). Also, when discharging an assumption, you should use a line above the proposition, not brackets around it. So, your proof should look like this:

(A OR B) ⊢ (B OR A)
Assume NOT(B OR A)
... AvB ... (Assumption)
... NOT(A) ... (Assumption)
... B ... (by OR elimination)
... A ... (by OR elimination)
... (B AND A) ... (by AND introduction)
... (B OR A) ... (by OR introduction)

This is a valid proof using natural deduction. However, there are a few things that can be improved. First, when using the AND introduction rule, you need to have both propositions on separate lines, not on the same line as you have written. So, it should look like this:

(A OR B) ⊢ (B OR A)
Assume NOT(B OR A)
... AvB ... (Assumption)
... NOT(A) ... (Assumption)
... B ... (by OR elimination)
... A ... (by OR elimination)
... B ... (by AND introduction)
... A ... (by AND introduction)
... (B OR A) ... (by OR introduction)

Also, instead of using the AND elimination rule, you can use the OR introduction rule again to prove (B OR A). So, the proof would look like this:

(A OR B) ⊢ (B OR A)
Assume NOT(B OR A)
... AvB ... (Assumption)
... NOT(A) ... (Assumption)
... B ... (by OR elimination)
... A ...

 

[Mene]

Hello TKM,

Thank you for sharing your attempt at a solution and your questions about natural deduction. I will try my best to address them and provide a response to your content.

Firstly, your diagram proof is a valid way to represent your proof, but I will also provide a more traditional natural deduction proof below for clarity.

Proof:

1. (A OR B) ...........................Assumption
2. [A] .................................Assumption
3. A ....................................And Elimination (2)
4. B OR A ..............................Or Introduction (3)
5. .................................Assumption
6. B ....................................And Elimination (5)
7. B OR A ..............................Or Introduction (6)
8. (B OR A) ............................Or Elimination (1, 2-4, 5-7)

Explanation:

1. We start with the assumption (A OR B), which is given in the problem statement.
2. We discharge the assumption (A) and use it to derive A.
3. Using the And Elimination rule, we can extract A from (A AND B).
4. Using the Or Introduction rule, we can introduce B OR A from A.
5. We then discharge the assumption (B) and use it to derive B.
6. Again, using the And Elimination rule, we extract B from (A AND B).
7. Using the Or Introduction rule, we introduce B OR A from B.
8. Finally, using the Or Elimination rule, we can derive (B OR A) from (A OR B), (2-4), and (5-7).

To answer your question about using every assumption, the answer is yes and no. You can use any assumption as long as it is consistent with the given statements and can be discharged later in the proof. However, there may be some assumptions that are not necessary or helpful in deriving the conclusion, so it is important to carefully consider which assumptions to use.

I hope this helps to clarify things for you. Good luck with your further studies in natural deduction!