1. Not finding help here? Sign up for a free 30min tutor trial with Chegg Tutors
    Dismiss Notice
Dismiss Notice
Join Physics Forums Today!
The friendliest, high quality science and math community on the planet! Everyone who loves science is here!

Natural Deduction - AvB |- BvA

  1. Jan 4, 2009 #1
    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
     
  2. jcsd
Know someone interested in this topic? Share this thread via Reddit, Google+, Twitter, or Facebook

Can you help with the solution or looking for help too?