Results 1 to 4 of 4
Like Tree1Thanks
  • 1 Post By emakarov

Math Help - Natural Deduction problem

  1. #1
    Newbie
    Joined
    Apr 2012
    From
    Taiwan
    Posts
    6

    Natural Deduction problem

    Define ⌈T⌉ = λx.λy.x and ⌈F⌉ = λx.λy.y .
    Furthermore,let ⌈if t then u else v =tuv.
    Show if T then u else v= u and ⌈if F then u else v = v.
    (the proof sustem is Natural Deduction)
    _________________________________________

    I don't know how to start the proof.
    Any help will be appreciated.
    Follow Math Help Forum on Facebook and Google+

  2. #2
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780

    Re: Natural Deduction problem

    We have beta-reduction (λx. M)N = M[N/x] where M[N/x] is M with N substituted for x. Then

    ⌈if T then u else v⌉ = Tuv (by definition of "if")
    = (λxλy. x)uv (by definition of T)
    = ((λy. x)[u/x])v
    = (λy. u)v
    = u

    "if F then u else v" is considered similarly.
    Thanks from Alexya
    Follow Math Help Forum on Facebook and Google+

  3. #3
    Newbie
    Joined
    Apr 2012
    From
    Taiwan
    Posts
    6

    Re: Natural Deduction problem

    Quote Originally Posted by emakarov View Post
    We have beta-reduction (λx. M)N = M[N/x] where M[N/x] is M with N substituted for x. Then

    ⌈if T then u else v⌉ = Tuv (by definition of "if")
    = (λxλy. x)uv (by definition of T)
    = ((λy. x)[u/x])v
    = (λy. u)v
    = u

    "if F then u else v" is considered similarly.
    Thanks!
    But I still stuck at one question: why (λy. u)v= u ?
    Follow Math Help Forum on Facebook and Google+

  4. #4
    MHF Contributor
    Joined
    Oct 2009
    Posts
    5,545
    Thanks
    780

    Re: Natural Deduction problem

    Quote Originally Posted by Alexya View Post
    But I still stuck at one question: why (λy. u)v= u ?
    Because y is not free in u, so when v is substituted for y in u, the result is still u. This happens, for example, when u is a variable distinct from y or when u is a closed term.
    Follow Math Help Forum on Facebook and Google+

Similar Math Help Forum Discussions

  1. natural deduction
    Posted in the Discrete Math Forum
    Replies: 3
    Last Post: December 12th 2011, 08:31 AM
  2. Natural Deduction
    Posted in the Discrete Math Forum
    Replies: 9
    Last Post: June 9th 2011, 03:15 AM
  3. Could use some help with a Natural Deduction proof
    Posted in the Discrete Math Forum
    Replies: 2
    Last Post: May 4th 2010, 05:58 AM
  4. natural deduction
    Posted in the Discrete Math Forum
    Replies: 5
    Last Post: April 24th 2010, 11:47 AM
  5. Help with Logic (Natural Deduction)
    Posted in the Discrete Math Forum
    Replies: 7
    Last Post: January 12th 2010, 02:07 PM

Search Tags


/mathhelpforum @mathhelpforum