Looking for help in understanding a proof of the fixed point lemma in mathematical logic.

In the fixed point lemma on page 58 of https://www.math.ucla.edu/~dam/114L.18s/114Lnotes.pdf don't the implications in $\chi(v_1)$ and $\sigma$ need to be double implications? Is this an error in the proof?

If the proof in the above pdf is in fact correct, then I don't get the very last line of the proof asserting that you can deduce $\sigma$ from $\varphi$.

I have the same issue with the Wikipedia proof: It seems to me that $${\displaystyle {\mathcal {B}}(z):=(\forall y)[{\mathcal {G}}_{f}(z,\,y)\Rightarrow {\mathcal {F}}(y)]}$$ needs to be a double implication so that the deduction can be made from ${\mathcal {F}}(y),$

Many thanks for your help.


No, there doesn’t need to be and shouldn’t be a double implication.

Reasoning in Q, if $\sigma$ is false, that means is some number $v_3$ such that $\psi(q,q,v_3)$ holds and $\varphi(v_3)$ is false. But since $\psi$ represents a function, there is only one such $v_3$, namely $\#\sigma$, so $\varphi(\#\sigma)$ is false. The contrapositive of all of this is that $\varphi(\#\sigma)\to\sigma$.