# Quantification

So far, we have only looked at ways to make statements about specific objects, like #\$FredsBike. But CycL, like first-order predicate calculus, also gives us two ways to talk about objects without being specific about the identity of the objects involved: universal quantification and existential quantification. Universal quantification corresponds to English expressions like every, all, always, everyone, and anything, while existential quantification corresponds to English expressions like someone, something, and somewhere. CycL contains one universal quantifier, #\$forAll, and many existential quantifiers, including #\$thereExists, #\$thereExistAtLeast, #\$thereExistAtMost, and #\$thereExistExactly.

### 2.6.1.  #\$forAll

The quantifier #\$forAll takes two arguments, a variable and a sentence in which the variable appears. In practice, the sentence is almost always a conditional in which the antecedent is used to restrict the scope of the variable. Here’s an example:

```     (#\$forAll ?X
(#\$implies
(#\$owns #\$Fred ?X)
(#\$objectFoundInLocation ?X #\$FredsHouse)))```

This sentence states that it is true, concerning every object in the CYC ontology, that if #\$Fred owns that object, then that object is located in #\$FredsHouse. In other words, all Fred’s stuff is in his house.

### 2.6.2.  Multiple Quantification

Sentences may contain more than one quantifier, as in the following:

```     (#\$forAll ?X
(#\$forAll ?Y
(#\$implies
(#\$and
(#\$owns #\$Fred ?X)
(#\$owns #\$Fred ?Y))
(#\$near ?X ?Y))))```

which says that any two things owned by Fred are near each other. Note that each quantifier introduces a new variable, and that each variable must have a different name.

### 2.6.3.  Unbound Variables

Normally, variables need to be introduced (“bound”) by a quantifier before they are used. Each quantifier binds exactly one variable, and every variable used should be bound by exactly one quantifier. Furthermore, a variable has no meaning outside the scope of the quantifier which binds it.

However, if a unbound variable appears in a CycL sentence, it is always assumed to be universally quantified, with the result that

```     (#\$implies
(#\$owns #\$Fred ?X)
(#\$objectFoundInLocation ?X #\$FredsHouse))```

is exactly equivalent to

```     (#\$forAll ?X
(#\$implies
(#\$owns #\$Fred ?X)
(#\$objectFoundInLocation ?X #\$FredsHouse)))```

Since the former is easier to write and read, it is almost always preferred in practice, and you will rarely see a #\$forAll while browsing the CYC KB. Note, however, that unbound variables which appear only in the consequent of a conditional, and not in the antecedent, may have drastic and undesired consequences. Take, for example, the following:

```     (#\$implies
(#\$owns #\$Fred ?WHATEBER)
(#\$objectFoundInLocation ?WHATEVER #\$FredsHouse))```

Because of the typo, the variable ?WHATEVER will range over the entire CYC ontology. In other words, the assertion above states that as long as Fred owns one thing, everything is located in #\$FredsHouse–probably not what we wanted. See the section on “don’t-care” variables for ways in these kinds of mistakes can be detected.

### 2.6.4.  #\$thereExists

The quantifier #\$thereExists takes two arguments, a variable and a sentence in which the variable appears. In practice one uses #\$thereExists only in certain ways, of which the following is a good example:

```        (#\$implies
(#\$isa ?A #\$Animal)
(#\$thereExists ?M
(#\$mother ?A ?M)))```

This assertion states that, for every animal, there exists at least one object which is that animal’s mother. The object which is the animal’s mother may be an object which is already represented by a CYC constant, or it may be a new object of which CYC has no knowledge. But unless and until it is told otherwise, CYC will assume that the object is a new one not identical with any “known” object.

### 2.6.5.  #\$thereExistExactly, #\$thereExistAtLeast, #\$thereExistAtMost

These three quantifiers are similar to #\$thereExists, but provide greater quantitative expressiveness. Each of them takes three arguments: a positive integer, a variable, and a sentence in which the variable appears. Their meaning should be fairly self-explanatory. Look at the following examples:

```        (#\$implies
(#\$isa ?P #\$Person)
(#\$thereExistExactly 2 ?LEG
(#\$and
(#\$isa ?LEG #\$Leg)
(#\$anatomicalParts ?P ?LEG))))
```
```        (#\$implies
(#\$isa ?T #\$Table)
(#\$thereExistAtLeast 3 ?LEG
(#\$and
(#\$isa ?LEG #\$Leg)
(#\$physicalParts ?T ?LEG))))
```
```        (#\$implies
(#\$isa ?P #\$UnitedStatesPerson)
(#\$thereExistAtMost 1 ?SPOUSE
(#\$spouse ?P ?SPOUSE)))```

### 2.6.6.  Well-Formedness of Quantified Sentences

As you probably by now expect, any sentence beginning with a quantifier is well-formed if and only if its arguments are of the right number, of the right types, in the right order, and its sentence argument is well-formed.

### 2.6.7.  Skolemization

People writing assertions for entry into the CYC KB use #\$thereExists quite frequently. But when you browse the KB, you rarely see #\$thereExists in an assertion. That’s because once assertions are entered into the KB, occurences of #\$thereExists are automatically converted into Skolem functions. The only exceptions are certain cases where #\$thereExists is used within an expression that is an argument to a predicate. Thus, an assertion which was entered as:

```        (#\$implies
(#\$isa ?A #\$Animal)
(#\$thereExists ?M
(#\$and (#\$mother ?A ?M)
(#\$isa ?M #\$FemaleAnimal))))```

will appear in the KB as 4 different assertions:

```        (#\$isa #\$SKF-8675309 #\$SkolemFunction)
(#\$arity #\$SKF-8675309 1)
(#\$implies
(#\$isa ?A #\$Animal)
(#\$mother ?A (#\$SKF-8675309 ?A)))
(#\$implies
(#\$isa ?A #\$Animal)
(#\$isa (#\$SKF-8675309 ?A) #\$FemaleAnimal))```

For more details, look at “An Introduction to CYC Inferencing”.