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?

Right.

Tobias

> Thanks for the help in advance.
> 
> John
> 





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