Now, given an arbitrary formula <math>\mathcal{F}(y)</math> with one
free variable <math>y</math>, define the formula
<math>\mathcal{B}(z)</math> as:
:<math>\mathcal{B}(z) := (\forall y) [\mathcal{G}_f(z,\,y)\Rightarrow
\mathcal{F}(y)]</math>I think it’s saying that if you have some formula F, you can define B(z) as a formula stating that (here i need to shift the sense of function and expression to the more formal sense of formula in the logic
