[Math] Lambda Calculus Proof: or false (not true) Evaluates to False, using lazy evaluation, Help!

Question

I am trying to learn lambda calculus, and I am currently tackling a few boolean logic questions. I have gotten to one that I am stuck on, and I am looking for a little help proceding. I need to prove that:

or false (not true)

evaluates to false, using lazy evaluation. I am given the following, where '\' is a lambda:

or = \v.\w.(v w v)
false = \x.\y.(y)
not = \v.\w.\x.(v x w)
true = \x.\y.(x)

So far I have gotten:

or false (not true)
= \v.\w.(v w v) false (not true)
= \w.((false(not true)) (false(not true)) w)

From here I am lost, I think my next step should be along the lines of:

\w.((\a.\b.(b)(not true)) false(not true) w)

But I feel like it is completely wrong. Is anyone able to help out? What would be the next step. How do I go about solving this problem? Since it is lazy evaluation, should I have done something more like:

\w.(false(false(not true) true w))

The above seems certainly wrong.

Please help

Thanks,

cjd

Answer 1

So I was going horribly wrong even from the beginning. I have finally figured this out. Here is the solution.

or false (not true)
= \v.\w.(v v w) false (not true)
= \.w(false false w) (not true)
= false false (not true)
= \x.\y.(y) false (not true)
= \y.(y) (not true)
= (not true)
= \v.\w.\x.(v x w) true
= \w.\x.(true x w)
= \w.\x.(\a.\b.(a) x w)
= \w.\x.(\b.(x) w)
= \w.\x.(x)
= false
or is the same as \x.\y.(y) which is equal to false.