how to define lambda calculus encoding for boolean implication(⇒). (Recall that in boolean logic, x ⇒ y iff ¬x ∨ y.) You may use true, false and cond by name in your definitions if you want.
true := λx. λy. x
false := λx. λy. y
cond := λb. λx. λy. b x y
I currently have got "not" := λx.x false true
"or" := λx.λy.x true y
What should I do next ?
Let me go through how you might come up with the formula for or, and then let you do something similar for impl.
The key observation here is: if $x$ is true, then $x \vee y$ is always true. Whereas if $x$ is false, then $x \vee y$ is equal to $y$. Therefore, $x \vee y = cond ~ x ~ true ~ y.$ In other words, $$\vee = \lambda x . \lambda y . (\mathbf{if}~ x~ \mathbf{then}~ true ~ \mathbf{else}~ y) = \lambda x . \lambda y . cond ~ x ~ true ~ y = \lambda x . \lambda y . x ~ true ~ y.$$ (And if you like, you can then make this a bit shorter using the $\eta$ rule: it is equivalent to $\lambda x . x ~ true$.)
Now, for impl, we can start off with a similar analysis: if $x$ is true, then $x \rightarrow y$ is equal to $y$; whereas if $x$ is false, then $x \rightarrow y$ is always true. I'll leave it to you to take the construction of impl as a lambda expression from here.
