[FOM] A question about the history of a notation

[Roger Bishop Jones]

Correcting my own posts again!

On Thursday 02 January 2003  1:24 pm, Roger Bishop Jones wrote:

> 2. in languages such as HOL (a mechanised derivative of Church's STT)
> "E!" is used and is both a quantifier and a predicate.
> In HOL:
>
> 	(E! x. p x) = ($E!) (lambda x. p x)
>
> (where the $ is used to override the syntactic status of E! as
> a variable binder and allow it to be used as a predicate).
>
> So distinguishing between the predicate and the quantifier
> in the way you suggest doesn't make sense in general.

This is OK in spirit, but I don't think "E!" is the name of the unique
existence predicate/quantifier in HOL.
Maybe its "?!", but I forget since don't use Cambridge HOL now,
I mostly use ProofPower which uses backwards E subscript 1,
(also for a unique existence predicate and quantifier).

Roger Jones