Formulate boolean logic in lambda calculus

Question

I want to formulate the boolean operator $\Leftrightarrow$ in lambda calculus. I know that the negation is formulated as $\lambda x.x F T$ and the conjugation is formulated as $\lambda x y.x y F$ as well as that $\mathtt{true} = \lambda x y.x$ and $\mathtt{false} = \lambda x y.y$. But how can I now get from there to a formulation for the equivalence?

Answer 1

One way is to combine what you already have. Since $\Leftrightarrow$ is (can be) defined as $p \Leftrightarrow q = (p \Rightarrow q) \land (q\Rightarrow p)$ and $p \Rightarrow q = \lnot p \lor q$ and $p \lor q = \lnot (\lnot p \land \lnot q)$ you could just compose what you already have.

Now assuming your definitions of $\mathtt{true}$ and $\mathtt{false}$ there is a much simpler term. Namely $\Leftrightarrow$ can be defined as $$ \lambda x y. x\, y\, (y\,\mathtt{false}\,\mathtt{true})$$ or using the definition of $\lnot$ simply as

$$ \lambda x y. x\, y\, (\lnot y)$$

To see why this is so consider the cases.

If $p = \mathtt{true}$ then $p \Leftrightarrow q$ is true if $q$ is true and false if $q$ is false. Therefore if $p = \mathtt{true}$, $p \Leftrightarrow q = q$.

If $p = \mathtt{false}$ then $p \Leftrightarrow q$ is true if $q$ is false and false if $q$ is true. Therefore $if p =\mathtt{false}$, $p \Leftrightarrow q = \lnot q$.

Since $\mathtt{true}$ is the first projection and $\mathtt{false}$ is the second projection booleans act as an "if" expression, hence you can read $\lambda x y.x\,y\,(\lnot y)$ as $\lambda x y . \mathbf{if}\, x\, \mathbf{then}\, y\, \mathbf{else}\, (\lnot y)$ which should now make clear where the expression came from.