How to understand quantifier without predication “ ∀(λφ. (φ x m→ φ y))”?

Question

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent example here https://www.isa-afp.org/entries/GoedelGod.html (as encoded for Isabelle/HOL).

This embedding has embedding for Leibniz equality for individuals:

abbreviation mLeibeq :: "μ ⇒ μ ⇒ σ" (infixr "mL=" 90) where "x mL= y ≡ ∀(λφ. (φ x m→ φ y))"

and this type of euqality is used for the first axiom already:

A1a: "[∀(λΦ. P (λx. m¬ (Φ x)) m→ m¬ (P Φ))]"

which can be written without lambdas as:

A1a: ∀φ[P(¬φ)↔¬P(φ)]

My question is - how to understand the expression ∀(λφ. (φ x m→ φ y)), because usually we have ∀x.P(x)? I.e. universal quantifier expects the argument (x) and the predicate (P(x)), but this expression contains noone know what? is entire (λφ. (φ x m→ φ y)) and argument x or Predicate P(x)? What can be omitted here, what is the convention used here?

Answer 1

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 "integrate from $0$ to $1$" 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 "$dx$" above changed to "$x \mapsto$". 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 > -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 > -3)$. And again, we can inline the complex expression to get $$A(\lambda x . (x^2 + 3 x > -3))$$ Now just replace $A$ with $\forall$ for good old times sake: $$\forall(\lambda x . (x^2 + 3 x > -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.