[FOM] A question about the history of a notation

[Roger Bishop Jones]

On Wednesday 01 January 2003  2:00 pm, Neil Tennant wrote:
> Can any fom-er throw some light on the history of a certain notation?
>
> I'll use 'E' for the existential quantifier.
>
> The notation that interests me is 'E!' often pronouned as 'E shriek'.
> The earliest use that I know of is in Russell, where it is used in
> contexts such as
>
> 	E! iota x F(x)
>
> which means "The F exists", or
>
> 	E! alpha
>
> which means "(The set) alpha is non-empty".
>
> (See his 'On Denoting', in ed. Marsh, Logic and Knowledge, at p.93 and
> p.91 respectively.)
>
> It is clear that, for Russell, 'E!' is a predicate, in that it is
> completed by a name (or, more generally, a singular term) to form a
> sentence. Note that in the context 'E! iota x F(x)', it is 'iota', not
> 'E!', which binds the variable x. The expression 'iota x F(x)' is (of the
> category of) a singular term.

The paper you are quoting from is not "On denoting",
which makes no use of these symbols, but "Mathematical Logic
as based on the Theory of Types".

You have conflated two different notations used in that paper
and in Principia Mathematica.
A rotated E followed by ! is indeed used as if it were a predicate,
but this has nothing to do with uniqueness and little to do
with existence, since it predicates (as you say) non-emptyness.

Russell also uses the notation "E!" literally, without rotating the E
which he defines only (so far as I can see) when applied to a
definite description.
This is the one which is close to unique existential quantification,
but surely an important purpose of Russell's theory of descriptions
is to avoid the difficulties which arise if existence is treated as a
predicate.
His definition makes no sense if E! is applied to arbitrary objects
and it must surely be regarded not as a predicate but as an 
"incomplete symbol", which has no meaning in itself.

> But there is a modern usage according to which 'E!' is a quantifier, and
> directly binds variabls; more specifically, it is the uniqueness
> quantifier. On this reading,
>
> 	E! x F(x)
>
> means "There is exactly one x such that F(x)". So here 'E!' is completed
> by a predicate to form a sentence, as indicated by the variable-binding.
>
> What I would like to know is the provenance of this modern usage. 

I don't think I can say much about the provenance, but I observe that:

1. the use of "!" is prefered over "subscript 1" in mechanised proof systems 
simply because it is an ascii character.

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.

Roger Jones