1. ## 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.

2. ## 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.

3. ## Re: Natural Deduction problem

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 ?

4. ## Re: Natural Deduction problem

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.