Encoding of booleans in lambda calculus

Question

The encoding of booleans in pure lambda calculus:

true := λx.λy.x

false := λx.λy.y

cond := λb.λx.λy.b x y

So if "cond" re-defined as cond := λx.x and assume "true" and "false" are keep same as before, does this result in a valid encoding of booleans?

Answer 1

Yes, you are correct. The two definitions of cond are extensionally equal. But using the short version would make the definition even more mysterious, and it is very mysterious already.

You could also use $\lambda xy.xy$ or $\lambda abcd.abcd$ and it would work the same.

Some presentations omit cond completely and just say that the boolean value is itself the test.