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?