New chapter in my struggle with Lambda Calculus (previous chapters here and here, with my great thanks to those users who wrote enlightening answers). My problem is now to establish the following result in Example 2.13(ii) from "Introduction to Lambda Calculus":
$$\exists G \ \forall X, \ GX = GG $$
without setting $G \equiv \mathbf{Y} ( \lambda gx.gg)$. Here there is my attempt:
Proof: Let $G \equiv FF$ with $F\equiv \lambda fx.ffff$.
Thus, from Compatibility Rule 1 we have that $FF = (\lambda fx.ffff)F$, from which $FF = \lambda x.FFFF$.
Again, apply Compatibility Rule 1 to have $FFx = (\lambda x.FFFF)x$, from which we have $FFx = FFFF$. Finally, by definition of $G$, we have $Gx = GG$ and, since $x$ is arbitrary, $GX = GG$. $\square$
I wouldn't call this elegant, but I am wondering if it is actually correct. Also, if it is, are there more elegant solutions to the problem that do not use $\mathbf{Y}$?
Any feedback as always will be greatly appreciated.
Thank you for your time.
Your proof is correct, except for a small detail. You defined $F \equiv \lambda fx.ffff$, which means that $F$ is nothing but a shorthand for $\lambda fx.ffff$. Hence $FF \equiv (\lambda fx.ffff)F$, which means that $FF$ is nothing but a shorthand for $(\lambda fx.ffff)F$ (and for $(\lambda fx.ffff)(\lambda fx.ffff)$ and $F(\lambda fx.ffff)$ as well), i.e. they are syntactically the same object. In particular, this implies that $FF = (\lambda fx.ffff)F$ by the first equality rule (Def. 2.7 in your notes), and not by the first compatibility rule.
Concerning a simpler solution of the problem that does not use $\bf Y$, you can repeat your proof by setting $F \equiv \lambda fx.ff$ and $G \equiv FF$. Then, \begin{align} G &\equiv FF = \lambda x.FF \equiv \lambda x.G \\ GG &\equiv (\lambda x.G)G = G = (\lambda x. G)X \equiv GX. \end{align}