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

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?

Posted on Categories proxies