[isabelle] Encoding quantifiers


Does anyone know where I can find how the existential quantifier is
encoded using quantifier constants and lambda terms? I see

Ex_def:       "Ex(P)     == !Q. (!x. P x --> Q) --> Q"

in HOL.thy. Is "Ex" here same as "\exists" and "!" same as "\forall"?
"!" is a binder for "All", which is the constant for universal
quantifier, right?

Thanks for the help in advance.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.