Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Encoding quantifiers

Email Gateway (Aug 19 2022 at 09:52):

From: John Munroe <munddr@gmail.com>
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

Email Gateway (Aug 19 2022 at 09:52):

From: Tobias Nipkow <nipkow@in.tum.de>
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

Last updated: Apr 26 2024 at 04:17 UTC