Re: [isabelle] Encoding quantifiers
Am 09/01/2013 06:13, schrieb John Munroe:
> 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