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$?

  • $\begingroup$ If the reason behind close vote could be explained, I can try to improve the question $\endgroup$ – Peeyush Kushwaha Jun 24 '18 at 13:41
  • $\begingroup$ 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... $\endgroup$ – Malice Vidrine Jun 26 '18 at 1:02
  • $\begingroup$ @MaliceVidrine any luck on finding that? $\endgroup$ – Peeyush Kushwaha Jun 28 '18 at 18:16

Apologies for the delay on getting back to you. The following is not a complete answer, but it got a little long for a comment.

The reference I was thinking of was in Barendregt et al.'s Lambda Calculus with Types, Ch. 5.1. The reason this doesn't fully answer your question, though, is because it already assumes that, over and above the simply typed lambda calculus, you have universal quantification and implication, with equalities as atomic formulas. Here equality (at each type) seems to be a genuine predicate rather than a rewritability relationship.

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.