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?
