Show that there does not exist $F$ such that $F(MN) = M$ for all $M$ and $N$.

Question

This is for Exercise 2.4.6 of Barengredt's "Lambda Calculus - It's Syntax and Semantics" and the exact statement from the book is to "Show that $\neg \ \exists \ F \ \forall \ MN \ F(MN) = M$".

My solution is as follows, and I was wondering if there is anything wrong with it:

Assume that there were to exist such an $F$. Then, let $G \equiv \lambda x . F(xI)$. So, for any $N$, we have that \begin{align} GN = F(NI) = N \tag{1} \end{align}

But by $\beta$-conversion, $G$ can be re-written as $G \equiv \lambda x.F(xI) = \lambda x.F((\lambda y. yI) x)$. Now, by the Fixed Point Theorem, there is some $X$ that is the fixed point of $\lambda y. yI$, and so $$ GX = F ((\lambda y.yI) X) = FX $$ Now, apply $F$ to both sides: \begin{align} G = F(GX) = F(FX) = F\tag{2} \end{align}

This means that for any $N$, \begin{align*} N \stackrel{(1)}{=} GN = G(IN) \stackrel{(2)}{=} F(IN) = I \end{align*} Now this shows that $F(MN)\ \# \ M$.

(The $I$ above is just the identity function).

Answer 1

This seems fine enough, but it is excessively complicated. $\beta$-equivalence is a congruence so if $X=_\beta Y$ then $FX=_\beta FY$. It's pretty obvious that the hypothetical $F$ violates this congruence. You can quickly produce a counterexample by finding $M$, $M'$, $N$, and $N'$ such that $MN=_\beta M'N'$ but $M\neq_\beta M'$. In your proof this happens when you show $G=F$, though you then need to show that $G$ can't be $F$. You could choose much more mundane and straightforward examples, e.g. $M=\lambda x.I$, $M'=I$, and $N=N'=I$. You'd then have $MN=_\beta I=_\beta M'N'$ but $M\neq_\beta M'$.

Even if we start off the way you do, we immediately have $G=\lambda x.x$ right from the first step. Then once you do the $\beta$-expansion, you immediately get $G=\lambda x.\lambda y.yI$ which is clearly not the identity function. This is another clear example of this hypothesized term violating the congruence. There's no need to talk about the Fixed Point Theorem. You seem to be avoiding applying the hypothesized equivalence under a lambda, but unless there's some implicit convention that $M$ and $N$ have to be closed terms, there's no reason for that.