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.

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.

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 ?

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.