[CL] CG: Update to Annex B
John F. Sowa
sowa at bestweb.net
Tue Nov 1 22:12:37 CST 2005
A few comments:
JS>> That implies that even quantifiers may be moved around
PH> ? Moved where? Presumably you can't move a universal
> 'through' an existential, right?
Yes. In core CGIF, there are only existentials.
In extended CGIF, a universal quantifier is defined,
and it takes precedence over all existentials in the
same context (which in CG terminology means any
collection of nodes contained within "[" and "]").
That means that when CGIF is translated to CL, all
universals within a context are moved to the front,
next come all existentials, and any nested contexts
(which may have more quantifiers) are moved to the end.
Re quantifiers: If you're specifying relations
among sets and sequences,, both the E! and E!!
relational operators (which Whitehead defined
in the Principia) really come in handy.
Kleene replaced the E! operator by the exactly one
quantifier, but he did not adopt E!! -- which is
the one that should really be called the "unique"
quantifier. For example,
Every person has exactly one (E!) mother.
Every person has a unique (E!!) social security number.
However, I wouldn't dare ask for them in the core.
More information about the CL