In classical boolean algebra syntax,
p NAND q = NOT(p AND q)
In lambda calculus, we have
\begin{align*}
true &:= \lambda xy. \,x \\
nand &:= \lambda uvxy. \, u \, (v \, y \, x) \, x
\end{align*}
The logical operator "not" is beta equivalent to "nand true".
We know that
" and p q = nand true (nand p q)"
This definition of "and" is good, but it is unwieldy. Because the definition of "and" becomes
$$and := \lambda pq. \,\text{nand true (nand p q)}$$
However, I also tried "nand true nand" as a definition for "and" but if failed because it is beta equivalent to "nand".
The question is, using a combination of " nand" and "true", is it possible to define a lambda term that behaves like "and".
obtuse abyss
tall auroraBOT