An explanation for Barendregt use of Y combinator in an equation

Question

I am going through the following lecture notes on lambda calculus by Barendregt and Barendsen :

http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf

Here at page 12 , after introducing fixed point theorem a small exercise which is an attempt to prove the following has been posted : $ \exists G \forall X $ $GX =SGX $.

It first proceeds to the implication

$Gx$ = $SGx$

which implies : $G$ = $ \lambda x .SGx $

which implies : $G $ = $ (\lambda gx.Sgx)G$

and then it concludes that :

$G$ = $Y$ $( \lambda g x.Sgx)$ where $Y $ is the fixed point combinator .

I am unable to figure out how was G found out to be $Y$ $( \lambda g x.Sgx)$ in the last step ? How was this conclusion reached up to ?

• Yuval Filmus: Y satisfies the equation $Y f = f (Y f)$ for all $f,ドル and so $g=Yf$ solves $g = fg$ for all $f$.
• Agnivesh Singh: @YuvalFilmus : And f here would be $( \lambda gx.Sgx) $ ?
• Yuval Filmus: Right, pattern matching would suggest that.
• chi: The direction of implication is wrong: taking $G=YF$ implies $G=FG,ドル not the other way around. So, taking $G=Y\ldots$ is only one way to solve the requirement on $G$ (other solutions exist), but that's enough for the goal. All your uses of "implies" should instead be "is implied by".
• Agnivesh Singh: @Chi : Yes , sorry for my mistake

Answer 1

The Y combinator satisfies the equation $Y f = f(Y f)$. Hence $g = Yf$ solves the equation $g = f g$. In your case, the function $f$ is $\lambda g x.Sgx$.

Answer 2

$$ \begin{align} & G=Y(\lambda gx.Sgx) & (*)\\ & G=(\lambda gx.Sgx) Y (\lambda gx.Sgx) & \text{(by FPT (ii))} \\ & G=(\lambda gx.Sgx)G & \text{(by *)} \end{align} $$ Therefore $G=Y(\lambda gx.Sgx) \implies G=(\lambda gx.Sgx)G$