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.