# Is it possible to express syntactic equality function in lambda calculus?

Let's denote truth and false by two suitable constants $T, F$ where $T \not=_\beta F$ where $\equiv$ is syntactic identity.

Could I define a $\lambda$-term $E$ such that for $\lambda$-terms $X$ and $Y$ in $\beta\eta$-nf, where $X \not\equiv Y$

$E X X =_\beta T$ and $E X Y =_\beta F$?

• If the reason behind close vote could be explained, I can try to improve the question – Peeyush Kushwaha Jun 24 '18 at 13:41
• I suspect the answer is "no", since if I recall you can use such an $E$ to get a higher order logic in conjunction with the other gear of lambda calculus. Let me see if I can find a reference to confirm this memory... – Malice Vidrine Jun 26 '18 at 1:02
• @MaliceVidrine any luck on finding that? – Peeyush Kushwaha Jun 28 '18 at 18:16

With such a logic the addition of an identity operation (there a term $\delta_{A,B}$ with signature $A\times A\times B\times B\to B$) gives a system proof theoretically much stronger than the one without it. The reason being in essence that you can form terms like $\delta(\delta a_0a_1)(\delta a_2a_3)$ that tell you the identity of two identities, and other higher order fanciness. I am unfamiliar with the methods of figuring out relative strength of these sorts of systems, so I have little helpful to add beyond the above remarks. Still, the above chapter may be a good place to start.