I'm trying to define a function that simulates equality between booleans.
To achieve equality operator, I can use the negation operator together with the xor operator, since for two boolean variables $p,q$, it holds that:
$\neg(p\oplus q)=T$ iff $p$ and $q$ have the same value.
If I simplify the above, I get:
$(p\vee\neg q)\wedge(\neg p\vee q)$
Which is the function I want to define.
So first let me start with the definitions, because I'll use them in this post:
$T=\lambda xy.x$
$F=\lambda xy.y$
$\bigvee_{or}=\lambda xy.xTy$
$\bigwedge_{and}=\lambda xy.xyF$
$\neg_{negaion}=\lambda x.xFT$
Now, thanks to @dtldarek I was able to define $(\neg p\vee q)$: $$\overbrace{\lambda st. \underbrace{(\lambda x.xFT)s}_\text{negates first arg}Tt}^{\text{represents }\neg p\vee q}=_{\beta}\lambda st.sFTTt$$
and in the same way, I defined $(\neg p\vee q)$:
$$\overbrace{\lambda mn. mT\underbrace{\Big((\lambda x.xFT)n\Big)}_\text{negates second arg}}^{\text{represents } p\vee \neg q}=_{\beta}\lambda mn.mT(nFT)$$
Which works, I tried it...
Now, applying $\bigwedge_{and}$ operator on these two above functions, I'd expect to get a function that takes two arguments and return $T$ if they are equal and $F$ otherwise, but:
$\big(\lambda xy.xyF\big)\big(\lambda st.sFTTt\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}\big(\lambda y.(\lambda st.sFTTt)yF\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}\big(\lambda y.(\lambda t.yFTTt)F\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}\big(\lambda y.yFTTF\big)\big(\lambda mn.mt(nFT)\big)=_{\beta}(\lambda mn.mt(nFT))FTTF$
There's no need to go further to see that I got an erroneous result, since this last application produces an expression rather than what I need which is a function that gets two arguments...
What did I do wrong?
