[CL] Modules in CL and CGIF

[John F. Sowa]

Pat,

For me, restricted quantifiers are the normal case, and
unrestricted quantifiers are only used in mathematics,
where the subject matter is limited to just one type
of entities.  If you specify the domain to be integers,
you won't expect quantifiers to range over cats and dogs.

 > ... for some people, the idea that when they write
 > (and publish) axioms, it is they who get to say what is
 > in their intended universe of discourse, has an enormous
 > significance.

If they want to limit the domain of quantification, they
sould do so explicitly by using restricted quantifiers.
In CG terms, tha means put a type label on the left side
of the concept node.  That's normal CG practice.

 > In particular, the (to me, unimportant) fact that simply
 > by using a predicate name in a 'wild west syntax' logic
 > (or, by using it as a property name in RDF), one was
 > thereby committed to allowing this thing to be an individual
 > in ones universe of discourse, was considered by some folk
 > to be simply outrageous.

I'd say it was their own fault.  If you let quantifiers
range over anything conceivable, you can't complain if
somebody conceives of something you hadn't intended.

 > In particular, the (to me, unimportant) fact that simply
 > by using a predicate name in a 'wild west syntax' logic
 > (or, by using it as a property name in RDF), one was
 > thereby committed to allowing this thing to be an individual
 > in ones universe of discourse, was considered by some folk
 > to be simply outrageous.

In the following example, I would say that anybody who wants
to limit domain should add the quantifier restriction.
For example,

    (forall ((x Integer) (y Integer))...

This seems so obvious that I don't see why anybody should
complain about getting into trouble with things like the
following:

 > The key example, by the way, is what has come to be
 > called a 'Horrocks sentence', which restricts the
 > universe to a single entity. This is consistent
 > in GOFOL:
 >
 > (forall (x y)(= x y))
 > (P a)
 > (not (Q a))
 >
 > i.e. there is one thing, P is true of it and Q is not.
 > However, this is not consistent in any CL dialect
 > (such as CLIF) which is not segregated, since the
 > property names themselves denote, and the second and
 > third sentences establish that (not (= P Q)). Note that
 > equating a with, say, P, is legal: but that does not
 > suffice to equate P with Q. You can get it down to two
 > things in the universe, but not to one.

I would tell anybody who wants to restrict the domain
of quantification to use restricted quantifiers.  That's
what I recommend for CGs.  The main purpose for untyped
quantifiers (core CGIF) is to map to CL.

John