How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?
The $x$ in $\forall x . P(x)$ is not an argument. It is a bound variable indicating which variable the quantifer is ranging over.
Let us compare the situation to the definite integral, for concretness just from $0$ to $1$. Here is an example:
$$\int_0^1 x^2 + 3 x \, dx$$
This is a very archaic way of writing mathematical expressions that mathematicians like to stick to. In general (and ignoring details about non-integrable functions) the definite integral is itself a function: it takes a function $f$ as an argument, such as $f(x) = x^2 + 3x$ and returns a number (the area under the curve). So we could simply write $I$ for &quot;integrate from $0$ to $1$&quot; and then the integral of $f$ is simply
$$I(f)$$
(Or if you want to keep the integration bounds visible write $I_0^1(f)$, but I won't).
The argument $f$ need not be a symbol, it can be a complex expression:
$$I(x \mapsto x^2 + 3 x)$$
Notice how &quot;$dx$&quot; above changed to &quot;$x \mapsto$&quot;. In $\lambda$-calculus notation we would write this as
$$I(\lambda x . x^2 + 3 x).$$
In archaic notation people sometimes feel uneasy about writing
$$\int_0^1 f$$
and so they end up always displaying $dx$ by writing
$$\int_0^1 f(x) \, dx$$
even though there really is no need to do so, because $\int_0^1$ is a higher-order function which maps real-valued functions to real numbers.
If you want to make traditional mathematician feel uneasy you should write
$$\int_0^1 (x \mapsto x^2 + 3 x)$$
on their whiteboards
If this much is clear, then it should be easy to see that the universal quantifier $\forall$ is like integration, except that it takes a propositional function (one mapping into truth values instead of numbers) and returns a truth value.
The archaic notation
$$\forall x . (x^2 + 3 x &gt; -3)$$
can be changed, just like for integrals, to
$$A(f).$$
Here $A$ is the universal quantifier, and $f$ its argument, which is a function mapping from a set to the truth values. An example of such a function is $f(x) = (x^2 + 3 x &gt; -3)$. And again, we can inline the complex expression to get
$$A(\lambda x . (x^2 + 3 x &gt; -3))$$
Now just replace $A$ with $\forall$ for good old times sake:
$$\forall(\lambda x . (x^2 + 3 x &gt; -3)).$$
This his how computers like it. The notation is general, so we can write just $\forall f$ instead of $\forall x . f(x)$, and it exposes $\forall$ for what it is: a higher-order function that maps propositional function to truth values.