Thread: 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.

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.

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 ?

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.