# Does there exist a way, within Lambda Calculus, to discover if two free variables are the same?

Using Church's $$\lambda x.(\lambda y.y))$$ as false and $$\lambda x.(\lambda y.x))$$ as true, and given two free variables $$g$$ and $$h$$:

Could there exist a function $$eq?$$ such that $$(eq?\ g\ h)$$ is false, and $$(eq?\ g\ g)$$ is true?

I typically would show my work here, but as of right now, I honestly have nothing except a hunch that it's categorically impossible.

• What do you mean by the truth value of an expression like $(eq?\ g\ h)$ when $g,h$ are free? I don't believe that's well-defined. The natural definition would be to say that it reduces to true; but that doesn't make sense for an expression with free variables. – D.W. Mar 27 at 2:21
• @D.W. I want to determine whether two free variables are literally the same variable or not. In Scheme, I can write (eq? 'A 'A) and it returns #t, whereas (eq? 'A 'B) returns #f. ('A and 'B are atoms, not strings, meaning that they behave like $\lambda$-calculus free variables.) I'm open to any edits or suggestions that would make that clearer. – Ben I. Mar 27 at 2:24