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:
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?