B3. SUBSTITUTION, TYPICAL ELEMENTS, AND INSTANCES
1. Substitution
We will frequently have occasion to talk about eventualities that
exhibit the same pattern, are similar, or are tokens of the same
type. Thus, we need predicates for describing this similarity in
structure.
The first predicate we will need expresses what we get in ordinary
logics by substitution. We need to axiomatize substitution. We would
like to be able to say that if John believes he is successful and Mary
believes she is successful, then John plays the same role in his
belief as Mary plays in hers. Thus, suppose we know the following:
(believe' e1 J e3), (successful' e3 J)
(believe' e2 M e4), (successful' e4 M)
We would then like to be able to say that if you substitute M for J in
e1, you get e2. Alternatively, J plays the same role in e1 that M
plays in e2. The way we say this is
(subst J e1 M e2)
The definition of "subst" is a bit complex, but the reader should be
able to work through the axiom and see why it holds for the above
example. (Ignore the fourth line for now.)
(iff (subst x e1 y e2) (1)
(and (exists (p n)
(and (pred p e1)(pred p e2)(arity n e1)(arity n e2)
(noSubstTypelt x e1 y e2)
(forall (i)
(if (and (posInteger i)(leq i n)
(argn z1 i e1)(argn z2 i e2))
(and (iff (eventuality z1)
(eventuality z2))
(if (not (eventuality z1))
(and (if (nequal z1 x)
(equal z2 z1))
(if (equal z1 x)
(equal z2 y)))))
(if (eventuality z1)
(subst x z1 y z2)))))))))
This defines what it is for x to play the same role in e1 as y plays
in e2. Both e1 and e2 have to be eventualities; this follows from the
fact that they have predicates and arities. They have the same
predicate p and the same arity n (line 3). Then we look at all the
corresponding pairs of non-self arguments z1 and z2 of e1 and e2
(lines 5-7). z1 and z2 are either both eventualities or both not
eventualities (lines 8-9). If z1 is not an eventuality and is not the
same as x, then it remains unchanged; z2 is equal to z1 (lines 10-12).
If z1 the same as x, then z2 is y; this is where y is substituted for
x (lines 13-14). If z1 (and hence, z2) is an eventuality, then we
recurse and substitute x for y in those corresponding arguments; x
plays the same role in the argument z1 that y plays in argument z2
(lines 15-16).
Two substitutions can be done by doing one at a time.
(iff (subst2 x1 x2 e1 y1 y2 e2) (2)
(exists (e3)
(and (subst x1 e1 y1 e3)
(subst x2 e3 y2 e2))))
For example, if Mary loves John and Sue loves Bill, then we want to
say that the pair plays the same role in the first loving
event as the pair plays in the second.
(love' e1 M J), (love' e2 S B)
We express this by first substituting Sue for Mary in e1 to get e3:
(love' e3 S J)
and then substituting Bill for John in e3 to get e2. Of course, the
existence or nonexistence of e1 and/or e2 says nothing about whether
or not e3 holds.
Note that by definition (1), the expression "(subst e1 e1 e2 e2)"
means that the predications in which e1 and e2 are the self arguments
have the same predicates and the same non-self arguments. That is,
the only distinguishing features they have will be external to the
predications in which they are self arguments.
2. Typical Elements
Among the things we can think about are both specific eventualities,
like "Fido is barking", and general or abstract types of
eventualities, like "Dogs bark". We do not want to treat these as
radically different kinds of entities. We would like both, at some
level, to be treated simply as eventualities that can be the content
of thoughts.
For this it is convenient, although nonstandard, to reify the
universally quantified variable in statements about all elements of
sets. We would like to go from the standard set theoretic notation
s = { x | p(x) }
or its logical equivalent,
(forall (x) (iff (member x s)(p x)))
to a simple statement that p is true of a "typical element" of s by
reifying typical elements. We use the term "typical element",
although "reified universally quantified variable" might be a more
precise name for it (cf. McCarthy, 1977). The predication
(typelt x s)
will say that x is a typical element of the set s. The second
argument is constrained to be a set, and conversely, every set has a
typical element.
(forall (s) (iff (set s) (3)
(exists (x) (typelt x s))))
There is no assumption of uniqueness of typical elements.
The principal property of typical elements is that all properties of
typical elements are inherited by the real members of the set.
(forall (x s y e1 e2) (4)
(if (and (typelt x s)(member y s)(subst x e1 y e2)
(Rexist e1))
(Rexist e2)))
The term "typical element" has been used in previous papers (Hobbs,
1983, 1995, 1998). Some have complained that the term "typical
element" is too close to the term "prototype" and in any case suggests
defeasibility, i.e., that there may be properties of typical elements
that are not inherited by all of the real members. The reader may
overcome this feeling by thinking of "typelt" as meaning "type
element", the entity that represents the type defined by membership in
the set. We have also considered using the term "any element"
("anyelt"). However, this leads to frequent recourse to the barbarism
"the any element" or "an any element" to indicate that we are talking
about that entity rather than any real member of the set. The intent
of "typelt" is that all of its properties are inherited by all of the
real members, as indicated in Axiom (4).
One reason for distinguishing between a set and its typical element is
to capture the distinction between the two sentences
The men ran.
The men met.
In the first, each individual man runs, so the running would be
predicated of a typical element. In the second, it is the set of men
that met. Meeting is not something individual men can do by
themselves.
A related but stronger concept is represented by the predicate "dset".
This says that a set s with typical element x contains just those
elements for which some eventuality e really exists.
(dset s x e)
The "d" is for "defined"; the set s is defined by the property e. The
first argument of "dset" is a set, the second one is its typical
element, and the typical element occurs somewhere, perhaps embedded,
in the eventuality.
(forall (s x e) (5)
(if (dset s x e)
(and (set s)(typelt x s)(arg* x e))))
For example, s might be the set of things Mary believes to be red.
(dset s x e), (believe' e M e1), (red' e1 x)
If (p' e x), holds, i.e., if e is the eventuality of p being true of
x, then (dset s x e) is just a way of saying s = {x | p(x)}.
An entity is a member of a defined set if and only if the property e
holds for it. (Ignore the third line for now.)
(forall (s x e y e1) (6)
(if (and (dset s x e)(subst x e y e1)(Rexist e)
(notSubsetTypelt y s))
(iff (member y s)(Rexist e1))))
The rightward implication of the "iff" clause follows immediately from
Axioms (4) and (5). The leftward implication is new and what the
concept "dset" adds over and above "typelt".
A typical element of a set exists in the real world exactly when all
the real elements exist in the real world. For some eventuality
involving a typical element of a set to exist in the real world is
just for the corresponding eventualities involving the real elements
to exist in the real world.
Axioms (4) and (6) are useful but they bring with them some thorny
technical problems. Essentially, we have to be careful about applying
them to eventualities whose predicates are "typelt" and "member". The
reader who is willing to take these axioms on faith and believe that
in this book they will be used appropriately can skip the next
section, where these issues are discussed.
3. Handling Some Thorny Issues
As they are stated, Axioms (4) and (6) and the use of typical elements
more generally raise some difficult problems.
In Axiom (4), suppose (typelt' e x s) holds, i.e., that e is the
property of x being a typical element of s. Then it seems that each
real member of s will inherit that property and thus be a typical
element of the set as well. Applying this axiom again, that says that
anything true of any of the members would be true of all the other
members as well.
In Axiom (6), consider what happens when we let y be equal to x and e1
to e. Trivially, (subst x e x e) holds. If e is a property that
really exists, then it follows that x, a typical element of s, is a
member of s as well as all the real members. When we combine this
with the definition of cardinality in Chapter B2, we see that a set
{a, b, c}, if x is different from a, b, and c, would have at least
four members, a, b, c, and that typical element of the set.
The Law of the Excluded Middle says that a property either is true or
is not true of an entity. Suppose we have a set of pencils, some but
not all of which are red. Is a typical element red or not red? It
would seem that if typical elements are red, then all of the real
members are red, and if a typical element is not red, then none of
the real members are red.
To get around this family of problems, in Hobbs (1995) a scheme of
predicate indexing was introduced. This was fairly complicated, but
the essentials of the idea can be described without too much
difficulty. Base-level predicates, applying to real entities, were
subscripted with 0. If a predicate was applied to a typical element
of a set, it was subscripted with the name of the set and defined to
be true exactly when the base-level predicate was true of all the real
members of the set.
(forall (x s)
(if (typelt x s)
(iff (p_s x)
(forall (y) (if (member y x)(p_0 y))))))
In a sense, we are transforming the predicate "red" into the predicate
"all-red". Then if a typical member of the set is "all-red", all
the real members are "red", and conversely.
This solves the problem of the Law of the Excluded Middle. The
predicate "red" (or "red_0") is not true of typical elements, because
base-level predicates don't apply to typical elements. The predicate
"all-red" or "red_s" does apply to typical elements, and it is false,
because not all the pencils are red.
It might seem that we could take this "not all-red" property of the
typical element and pass it down to all the real members, so that they
would all be not red. But that would be a scoping error, a confusion
between "not all-red" and "all not-red". These are not equivalent.
The subscripts on the predicates can be ignored in almost all cases.
For example, consider the inference that if x believes p, then x is a
person.
(forall (x p) (if (believe x p)(person x)))
This holds true as well of typical elements. If a typical element x
of a set "believes_s" p, then that means all members of the set
believe p, so all members of the set are persons, so "person_s" is
true of the typical element. The inference holds for typical element
predicates as well as base-level predicates.
This is the normal case. We will have a predication about a typical
element involving a predicate from some non-set-theoretic content
theory, and we will want all the real members of the set to inherit
that property.
For this reason, we will reintroduce the unsubscripted predicate, now
as a cover term for all the subscripted predicates. An unsubscripted
predicate p is true of an entity exactly when some subscripted version
of that predicate is true of the entity.
(forall (x)
(iff (p x)
(exists (i) (p_i x))))
Then suppose (p x) holds. If x is an individual, that is, not a
typical element of a set, then (p_0 x) will hold. If x is a typical
element of s, then (p_s x) will hold.
This means that we will be operating at a less specific level than if
we used subscripted predicates. If we are only told "(red x)", we
don't immediately know whether "(red_0 x)" or "(red_s x)". But this
will almost never get us into trouble, and results in a much simpler
formalism.
Returning to the problem of the Law of the Excluded Middle, there are
three predicates we need to consider. The predicate "red_0" is false
of a typical element of the set of pencils because base-level
predicates are always false of typical elements. The predicate
"red_s" is false of the typical element because not all the real
members of the set are red_0. The unsubscripted predicate "red" is
false of the typical element because none of the subscripted
predicates are true of it.
Where the unsubscripted predicates do get us into trouble is with
set-theoretic predicates, because of the problems with Axioms (4) and
(6) described above. In Hobbs (1995) it is noted, as a warning for
future development, that "set-theoretic axioms have to be formulated
carefully." We are now at that point.
In this book, all but two of the predicates used will be the
unsubscripted predicates, and thus can apply to real elements and
typical elements. The two predicates are "typelt" and "member".
These predicates are closely related. The predicate "member", as we
are using it, is the base-level predicate "member_0", because that is
what we need in Chapter B2 in formulating traditional set theory. The
predication "(member_s x s)" is then true of typical elements of s
just in case every member of s is a member of s. So the predicate
"member_s" has exactly the same properties as the predicate "typelt".
They are equivalent; "typelt" is in fact just another name for
"member_s".
Since we are using the (implicitly) subscripted predicates "member"
("member_0") and "typelt" ("member_s"), we cannot allow real members
to be freely substituted for typical elements in Axiom (4), and we
have to be careful about concluding membership in Axiom (6). Failure
to do these things is what resulted in the problems. To avert these
problems and yet retain the power and utility of Axioms (4) and (6),
we have introduced a condition into the definition of substitution
("subst"), namely "(noSubstTypelt x e1 y e2)" in the fourth line of
(1). We are doing a kind of surgery on the definition of "subst" on
just those cases that cause trouble for typical elements -- when e1
itself is a typical element relation between x and s and y is a member
of s.
(forall (x e1 y e2) (7)
(iff (noSubstTypelt x e1 y e2)
(exists (s) (and (typelt' e1 x s)(member y s)))))
Now Axiom (4) will not allow us to conclude that a real member is also
a typical element, because "(subst x e1 y e2)" will not be true if e1
is the property of x being a typical element of a set of which y is a
member.
The problem with Axiom (6) is that the problematic conclusion
"(member y s)" involves the implicitly subscripted predicate
"member". We will thus run into problems whenever y is a typical
element of s or of a subset of s. All the antecedents of the
rightward implication will be satisfied, yet y, being a typical
element, will be the wrong sort of entity to have a base-level
predicate true of it. To get around this problem, we do surgery on
Axiom (6) and rule out the problematic cases with the condition
"(notSubsetTypelt y s)".
(forall (y s) (8)
(iff (notSubsetTypelt y s)
(exists (s1)(and (typelt y s1)(subset s1 s)))))
Note that the "dset" predication does not necessarily guarantee the
existence of the set; that is, there is no Axiom of Comprehension. If
e is the eventuality that x is not a member of s, then we would have
the Russell paradox: An entity y is member of the set if and only if
it is not a member of the set. Such a set s does not exist in the
real world.
4. Functional Dependencies
Every person has a mother. The usual way to express this in logic is
(forall (x)
(if (person x)
(exists (y) (mother y x))))
This is a general situation or eventuality in the world, and it can be
the content of a thought. Therefore we would like to reify it. This
means we have to reify its parts -- the x and the y. We already know
how to reify the x. It is a typical element of the set of entities
defined by the property e where (person' e x), i.e., the set of
persons. Here we discuss how to reify the y.
Not all the mothers are the same, so we can say that the mother is
"functionally dependent" on the person, with respect to the property
of being a mother. We will abbreviate this predicate to "fd". The
predication "(fd y x e)" says that y is functionally dependent on x
with respect to property e. The argument x must be a typical element
of a set, and both x and y must be involved somehow in e.
(forall (x y e) (9)
(if (fd y x e)
(and (arg* x e)(arg* y e)
(exists (s) (typelt x s)))))
In the above example, e is the eventuality such that (mother' e y x),
i.e., the property of y being the mother of x.
The principal property of "fd" is that when e holds and a real entity
instantiates x, then there is a real entity that instantiates y and
the corresponding eventuality holds.
(forall (x y) (10)
(if (and (fd y x e)(Rexist e)(typelt x s)(member x1 s))
(exists (y1 e1)
(and (subst2 x y e x1 y1 e1)(Rexist e1)))))
For example, Charles is a person, so he is a member of s. The
predication "(Rexist e)" holds becauses it really is true that every
person has a mother. Suppose Elizabeth is Charles's mother. Then
Elizabeth is y1 and e1 is the eventuality such that
"(mother' e1 Elizabeth Charles)" holds, i.e., the eventuality of
Elizabeth being Charles's mother.
The y1's constitute a set too, and thus have a typical element. It
would be pleasant if we could assume that the functionally dependent
entity y was the same as that typical element. (This was suggested in
Hobbs (1983).) But this is not possible since, in this case, it would
imply that every mother is the mother of everyone.
(mother y x) ==> (mother y1 x) for some y1, by (10)
==> (mother y1 x1) for every x1, by (6)
Corresponding to the functional dependency, there is a function
(normally called a "skolem function") that maps any element x1 of the
set s into the corresponding y1, and that function has a range. We
will define these here.
(forall (x x1 y y1 e) (11)
(iff (skfct y1 y x1 x e)
(and (fd y x e)
(exists (e1)
(and (subst2 x y e x1 y1 e1)
(if (Rexist e)(Rexist e1)))))))
The expression "(skfct y1 y x1 x e)" says that y1 is the value of the
function defined by the functional dependency "(fd y x e)" applied to
x1.
The range of the functional dependency is then the set of all values
of the skolem function.
(forall (s1 x y e) (12)
(iff (rangeFd s1 y x e)
(forall (y1)
(iff (member y1 s1)
(exists (x1) (skfct y1 y x1 x e))))))
The predicates "typelt", "dset", and "fd" are enough for reifying
universally quantified propositions. It is well-known that any
logical expression can be rewritten in "prenex" form, in which all the
universal quantifiers outscope all the existential quantifiers. All
of the existentially quantified variables will then have "fd"
relations with universally quantified variables.
With the device of skolemization, functions are introduced for every
existentially quantified variable; their arguments are all the
universally quantified variables, and their values are the
existentially quantified variables. For example, if we were to
express the statement that any point on a horizontal grid,
oriented in the cardinal directions, has a latitude, a longitude, and
an elevation, the prenex form would be
(forall (x y)
(exists (a b c)
(and (lat a x y)(long b x y)(elev c x y))))
(a is the latitude of , b is the longitude of , and c is the
elevation at .) After skolemization, this would be
(forall (x y)
(and (lat (f x y) x y)(long (g x y) x y)(elev (h x y) x y))))
Our "fd" predicate captures these functional relations f, g, and h.
But in fact we know that longitude depends only on x, latitude depends
only on y, and elevation depends on both. So rather than represent
the functional dependencies in the mechanical way skolemization does,
involving all the universally quantified variables, we would just have
the following "fd" relations:
(fd a y e1), (fd b x e2), (fd c x e3), (fd c y e3)
where e1, e2, and e3 are the lat, long, and elev relations,
respectively.
When a functionally dependent entity depends on more than one typical
element, that is, when an existentially quantified variable depends on
more than one universally quantified variable, we can instantiate the
functionally dependent entity one step at a time. In the elevation
example, we would first instantiate the x to a specific x-value x1
using Axiom (10), giving us (elev c1 x1 y). The c1 is then
functionally dependent on y, and we can use Axiom (10) again to give
us (elev c2 x1 y1). The entity c2 is now a real elevation, rather
than a functionally dependent entity.
But to get this to work, we need a rule that passes functional
dependence relations down to partial instantiations. The following
axiom does this.
(forall (c1 c x1 x y e e1) (13)
(if (and (skfct c1 c x1 x e) (fd c y e) (nequal x y)
(subst2 c1 x1 e1 c x e))
(fd c1 y e1)))
The relation "(fd c1 y e1)" is inherited from "(fd c y e)" whenever
some other universally quantified variable x induces a partial
instantiation of c.
In the elevation example, c1 will range over all the elevations for
points whose longitude is x1. The exact real elevation will depend on
the latitude y.
We will say that an entity that is a typical element of a set or
functionally dependent on a typical element of a set is "nonspecific".
(forall (x) (14)
(iff (nonspecific x)
(or (exists (s) (typelt x s))
(exists (y s) (and (typelt y s) (fd x y))))))
An entity is specific if and only if it is not nonspecific.
(forall (x) (iff (specific x) (not (nonspecific x)))) (15)
5. Instances
If x is a typical element of a set and x1 is a member of the set, we
can say that x1 is an instance of x. We would like to extend this
notion to eventualities.
First let us define the set of parameters in an abstract eventuality
e.
(forall (s e) (16)
(iff (parameters s e)
(forall (x)
(iff (member x s)
(exists (s1)
(and (arg* x e)(typelt x s1)))))))
The parameters of an abstract eventuality e are those typical elements
of sets that are somehow involved in e; "arg*" is a precise
characterization of "somehow involved in".
A partial instantiation results from instantiating some of the
parameters of the abstract eventuality either with real members of
their sets or with typical elements of subsets. We can define a
partial instance in this way.
(forall (e1 e) (17)
(iff (partialInstance e1 e)
(forall (s x)
(if (and (member x s)(parameters s e))
(exists (x1 s1)
(and (subst x e x1 e1)(typelt x s1)
(or (member x1 s1)
(exists (s2)
(and (typelt x1 s2)
(subset s2 s1))))))))))
That is, e1 is a partial instance of e exactly when for every
parameter x in e, there is a corresponding entity x1 in e1 which is
either a member of the set x ranges over or is a typical element of a
subset of that set. Note that we use the predicate "subset" rather
than "properSubset", so one limiting case of a partial instance of e
is e itself. Moreover, it admits some parameters being instantiated
while others are not.
Also, we could exercise the option of line 7 in the axiom and use only
real members, in which case we have a complete instantiation. In this
case, there are no remaining typical elements and thus no parameters.
So we can define a complete instantiation as a partial instantiation
with no remaining parameters.
(forall (e1 e) (18)
(iff (instance e1 e)
(and (partialInstance e1 e)
(forall (s1)
(if (parameters s1 e1) (null s1))))))
Equivalently, we could have used Axiom (17) without the last three
lines.
We can say that a eventuality type e1 holds for an entity y as its x
parameter if when the entity is substituted for x in the eventuality
type, the resulting instantiation really exists.
(forall (e1 y x) (19)
(iff (holdsFor e1 y x)
(exists (s e2)
(and (subst y e2 x e1)(typelt x s)(member y s)
(Rexist e2)))))
For example, if e1 is the eventuality type of a person being tall,
then e1 holds for John if John is tall, i.e., if his tallness really
exists.
Predicates Introduced in this Chapter
(subst x e1 y e2): x plays the same role in e1 that y plays
in e2.
(subst2 x1 x2 e1 y1 y2 e2): The pair plays the same role in e1
that the pair plays in e2.
(typelt x s): x is a typical element of s.
(dset s x e): s is the set with typical element x
defined by the property e.
(noSubstTypelt x e1 y e2): It is not the case that e1 is a typical
element relation between x and some set
s and y is a member of s; this blocks
using "subst" when e1 is a typical
element property.
(notSubsetTypelt y s): y is not a typical element of a subset
of s; this blocks problematic
applications of Axiom (6).
(fd y x e): y is functionally dependent on x by a
function described by e.
(skfct y1 y x1 x e): y1 is the value of the function
corresponding to the functional
dependency of y on x with respect to e
when applied to x1.
(rangeFd s y x e): s is the range of the values of the entity
y that is functionally dependent on x
with respect to e.
(nonspecific x): x is a typical element or functionally
dependent on a typical element.
(specific x): x is not nonspecific.
(parameters s e): s is the set of typical elements that
appear somewhere in e as arguments.
(partialInstance e1 e): e1 is a partial instantiation of e;
nonspecific arguments are either
instantiated or specialized.
(instance e1 e): e1 is a complete instantiation of e; all
nonspecific arguments are
instantiated.
(holdsFor e1 y x): The eventuality type e1 holds for entity
y; substituting y for a nonspecific
argument x of e1 yields an eventuality
that really exists.
References:
Hobbs, Jerry R., 1983. ``An Improper Treatment of Quantification in
Ordinary English'', {\it Proceedings of the 21st Annual Meeting,
Association for Computational Linguistics}, pp. 57-63. Cambridge,
Massachusetts, June 1983.
Hobbs, Jerry R., 1995. ``Monotone Decreasing Quantifiers in a
Scope-Free Logical Form'', in K. van Deemter and S. Peters
(Eds.), {\it Semantic Ambiguity and Underspecification}, CSLI Lecture
Notes No. 55, pp. 55-76, Stanford, California, 1995.
Hobbs, Jerry R. 1998. ``The Logical Notation: Ontological
Promiscuity.'' Chapter 2 of {\it Discourse and Inference}, available
at http://www.isi.edu/~hobbs/disinf-tc.html
McCarthy, John, 1977. ``Epistemological Problems of Artificial
Intellegence'', {\it Proceedings, International Joint
Conference on Artificial Intelligence}, pp. 1038-1044, Cambridge,
Massachusetts, August 1977.