# Natural Deduction problem

• May 5th 2012, 02:04 AM
Alexya
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.
• May 5th 2012, 01:48 PM
emakarov
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.
• May 6th 2012, 12:36 AM
Alexya
Re: Natural Deduction problem
Quote:

Originally Posted by emakarov
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 ?
• May 6th 2012, 05:14 AM
emakarov
Re: Natural Deduction problem
Quote:

Originally Posted by Alexya
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.