Re: [isabelle] Encoding quantifiers

Am 09/01/2013 06:13, schrieb John Munroe:
> Hi,
> 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.
> John

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