B9. ARITHMETIC 1. Integers In a practical reasoning system, one would not try to solve arithmetic problems by automatic theorem-proving from basic axioms. One would simply use the procedural attachment capabilities of the theorem-prover and utilize the computer's much more efficient arithmetic operations. Nevertheless, just for conceptual completeness, we will axiomatize basic arithmetic here, following the standard Peano axiomatization, in terms of a "successor" predicate. For consistency, we will treat arithmetic operations via predicates rather than via functions and use prefix notation rather than the conventional infix notation. However, the integers will be constants, the only constants we will use in this book. We could treat them as properties true only of unique individuals, but that would be altogether too pedantic. Zero is a nonnegative integer. (nonNegInteger 0) (1) Every nonnegative integer has a successor which is also a nonnegative integer. (forall (n) (2) (if (nonNegInteger n) (exists (n1) (and (nonNegInteger n1)(successor n1 n))))) The arguments of "successor" are nonnegative integers. (forall (n1 n) (3) (if (successor n1 n)(and (nonNegInteger n1)(nonNegInteger n)))) Besides zero, the only other specific numbers we will need are one, two, and ten. However, to define ten, we need to define three through nine. (and (successor 1 0)(successor 2 1)(successor 3 2) (4) (successor 4 3)(successor 5 4)(successor 6 5) (successor 7 6)(successor 8 7)(successor 9 8) (successor 10 9)) A positive integer is any nonnegative integer except zero. (forall (n) (5) (iff (posInteger n)(and (nonNegInteger n)(nequal n 0)))) No nonnegative integer has zero as its successor. (not (exists (n) (and (nonNegInteger n)(successor 0 n)))) (6) Successors are unique. (forall (n n1 n2) (7) (if (and (successor n1 n)(successor n2 n)) (equal n1 n2))) We will define addition recursively in terms of the "successor" relation. The predication "(sum n1 n2 n3)" means that n1 is the sum of n2 and n3. The sum of a number n and zero is n. (forall (n) (sum n n 0)) (8) The recursive step is as follows: (forall (n n1 n2 n3 n4) (9) (if (and (successor n3 n2)(sum n4 n1 n2)) (iff (sum n n1 n3)(successor n n4)))) The more conventional and more succinct way of saying this is "n1+S(n2) = S(n1+n2)". We won't constrain the arguments of "sum" to be nonnegative integers since we can extend "sum" to other kinds of numbers. But we can say that the nonnegative integers are closed under addition. (forall (n1 n2 n3) (10) (if (and (nonNegInteger n2)(nonNegInteger n3)(sum n1 n2 n3)) (nonNegInteger n1))) Addition is associative. (forall (n n1 n2 n3 n4 n5) (11) (if (and (sum n4 n2 n3)(sum n5 n1 n2)) (iff (sum n n1 n4)(sum n n5 n3)))) In more conventional notation, "n1+(n2+n3) = (n1+n2)+n3". Addition is commutative. (forall (n n1 n2) (12) (iff (sum n n1 n2)(sum n n2 n1))) More conventionally, "n1+n2 = n2+n1". We will not need multiplication in other chapters, but we need to introduce it here because we will need it in defining proportions and half orders of magnitude. Multiplication is defined in a manner similar to addition. The predication "(product n1 n2 n3)" means that n1 is the product of n2 and n3. The product of a number n and zero is zero. (forall (n) (product 0 n 0)) (13) The recursive step is as follows: (forall (n n1 n2 n3 n4) (14) (if (and (successor n3 n2)(product n4 n1 n2)) (iff (product n n1 n3)(sum n n4 n1)))) The more conventional way of saying this is "n1*S(n2) = (n1*n2)+n1". The nonnegative integers are closed under multiplication. (forall (n1 n2 n3) (15) (if (and (nonNegInteger n2)(nonNegInteger n3) (product n1 n2 n3)) (nonNegInteger n1))) We will not place constraints on the arguments of "product" because we want to extend it to rational numbers as well. One is the identity under multiplication. This follows from (13) and (14). (forall (n) (product n n 1)) (16) Multiplication is associative. (forall (n n1 n2 n3 n4 n5) (17) (if (and (product n4 n2 n3)(product n5 n1 n2)) (iff (product n n1 n4)(product n n5 n3)))) In more conventional notation, "n1*(n2*n3) = (n1*n2)*n3". Multiplication is commutative. (forall (n n1 n2) (18) (iff (product n n1 n2)(product n n2 n1))) Or, "n1*n2 = n2*n1". Multiplication and addition are related by the distributive law. (forall (n n1 n2 n3 n4 n5 n6) (19) (if (and (sum n4 n2 n3)(product n5 n1 n2)(product n6 n1 n3)) (iff (product n n1 n4)(sum n n5 n6)))) More conventionally, "n1*(n2+n3) = n1*n2 + n1*n3". A "less than" relation can be defined for nonnegative integers as follows: (forall (n1 n2) (20) (if (and (nonNegInteger n1)(nonNegInteger n2)) (iff (lt n1 n2) (exists (n3)(and (posInteger n3)(sum n2 n1 n3)))))) That is, n1 is less than n2 if and only if there is some positive integer n3 such that n2 is the sum n1 and n3. We condition this on n1 and n2 being nonnegative integers because we will extend it to rational numbers as well. The relations "leq", "gt", and "geq" can be defined in the obvious ways. (forall (n1 n2)(iff (leq n1 n2)(or (lt n1 n2)(equal n1 n2)))) (21) (forall (n1 n2)(iff (gt n1 n2)(lt n2 n1))) (22) (forall (n1 n2)(iff (geq n1 n2)(or (gt n1 n2)(equal n1 n2)))) (23) 2. Rational Numbers Fractions will be characterized by a nonnegative integer (the numerator) and a positive integer (the denominator). The predication "(fraction f a b)" says that f is the fraction a/b. Such fractions exists. (forall (a b) (24) (if (and (nonNegInteger a)(posInteger b)) (exists (f) (fraction f a b)))) Two fractions are equal under the usual conditions. (forall (f1 f2 a1 a2 b1 b2 c1 c2) (25) (if (and (fraction f1 a1 b1)(fraction f2 a2 b2) (product c1 a1 b2)(product c2 a2 b1)) (iff (equal f1 f2)(equal c1 c2)))) That is, a1/b1 = a2/b2 exactly when a1*b2 = a2*b1. The nonnegative integers can be embedded in the set of rational numbers. (forall (n) (if (nonNegInteger n)(fraction n n 1))) (26) That is, n = n/1. The "lt" relation can be extended to rational numbers. (forall (f1 f2 a1 a2 b1 b2 c1 c2) (27) (if (and (fraction f1 a1 b1)(fraction f2 a2 b2) (product c1 a1 b2)(product c2 a2 b1)) (iff (lt f1 f2)(lt c1 c2)))) That is, a1/b1 < a2/b2 exactly when a1*b2 < a2*b1. This also extends the other ordering relations, "leq", "gt", and "geq". We won't need to add two fractions. The product of two fractions is defined as follows: (forall (f f1 f2 a1 a2 b1 b2 c1 c2) (28) (if (and (fraction f1 a1 b1)(fraction f2 a2 b2) (product c1 a1 a2)(product c2 b1 b2)) (iff (product f f1 f2)(fraction f c1 c2)))) That is, if f1 = a1/b1 and f2 = a2/b2, then f1*f2 = (a1*a2)/(b1*b2). This definition works as well if the numerators and denominators are fractions as well as if they are integers. Thus, "product" can take fractions for any of its arguments. We will say that a fraction is a number, and that "product" requires a number and a nonzero number for its numerator and denominator. (forall (f a b)(if (fraction f a b)(number f))) (29) (forall (f a b) (30) (if (fraction f a b)(and (number a)(number b)(nequal b 0)))) All of this leaves open the possibility of defining the product of numbers other than the nonnegative rational numbers we have defined. But we will not need irrational or negative numbers in this book. 3. Measures and Proportions Sets of rational numbers, and hence sets of nonnegative integers, are very important examples of scales. We will focus on sets in which 0 is the smallest element. If e is the "lt" relation between x and y and s1 is a set of numbers containing 0 but no smaller number, then there is a nonnegative numeric scale s with s1 as its set and e as its partial ordering. (forall (s1 e x y) (31) (if (and (lt' e x y) (forall (n)(if (member n s1) (and (geq n 0)(number n)))) (member 0 s1)) (exists (s) (and (scaleDefinedBy s s1 e)(nonNegNumericScale s))))) Conversely, a nonnegative numeric scale has the "lt" relation for its ordering and a set of numbers, including zero, as its set. (forall (s) (32) (if (nonNegNumericScale s) (exists (s1 e x y) (and (lt' e x y) (forall (n)(if (member n s1) (and (geq n 0)(number n)))) (member 0 s1) (scaleDefinedBy s s1 e))))) It follows that a nonnegative numeric scale is a scale. A measure is a monotone increasing function from a scale into a nonnegative numeric scale in which the bottom of the domain scale, if there is one, maps into zero. (forall (m s1) (33) (iff (measure m s1) (exists (s2) (and (scale s1)(nonNegNumericScale s2) (functionInto m s1 s2) (monotoneIncreasing m) (forall (x)(if (bottom x s1)(map m x 0))))))) For example, if s1 is the scale whose set is a set of sets including the null set and whose partial ordering is "subset", then cardinality is a measure. (forall (e x y s1 s m n u) (34) (if (and (forall (z)(if (member z s1)(set z))) (exists (w)(and (member w s1)(null w))) (subset' e x y) (scaleDefinedBy s s1 e) (card' m n u)) (measure m s))) Line 2 says that s1 is a set of sets. Line 3 says that the null set w is one of those sets. Line 4 defines e as the subset relation. Line 5 says s is the scale defined by s1 and e. Line 6 defines m as the cardinality relation. Under these conditions, m is a measure on s. Suppose we have two points x and y on a scale s1 which has a measure. Then the proportion of x to y is the fraction whose numerator and denominator are the numbers the measure maps x and y into, respectively. (forall (f x y m s1) (35) (if (and (measure m s1)(inScale x s1)(inScale y s1)) (iff (proportion f x y m) (exists (n1 n2) (and (map m x n1)(map m y n2) (fraction f n1 n2))))) In more conventional notation, if m is a measure function mapping s1 into a nonnegative numeric scale, then the proportion f of x to y is given by "f = m(x)/m(y)". The constraints on the arguments of "proportion" are as follows: (forall (f x y m) (36) (if (proportion f x y m) (exists (s1) (and (measure m s1)(inScale x s1)(inScale y s1))))) The identity function is the function that maps every entity into itself. (forall (f s) (37) (iff (identityFunction f s) (and (function f s s) (forall (x)(if (member x s)(map f x x)))))) The identity function on a nonnegative numeric scale is a measure. (forall (f s) (38) (if (and (nonNegNumericScale s)(identityFunction f s)) (measure f s))) Thus, we can talk about the proportion of one point on a numeric scale to another, via the identity measure. Frequently, when an entity is measured on a numeric scale, we say that that entity is "at" that point on the scale. For example, we might say The temperature is at 90 now, but its going to fall this evening. When two scales are disjoint, we can define the "measure" relation as an "at" relation, thereby tapping into the rich vocabulary language has for talking about changes in such relations, such as the word "fall". If an entity is mapped into a point by a measure, it is "at" that point. (forall (m s1 x y) (39) (if (and (measure m s1)(function m s1 s2)(disjoint s1 s2) (map m x y)) (at x y s2))) The scale s2 is a possible ground by virtue of the fact that all its elements are numbers. 4. Half Orders of Magnitude In Hobbs (2000) and Hobbs and Kreinovich (2001) it was argued that a measurements in terms of half orders of magnitude consitituted a very important coarse-grained qualitative mode of judgment in commonsense reasoning. Increasing or decreasing the linear size of something by a factor of around three changes the way we interact with it. A box 4 inches square can be carried in one hand. If it is one foot square, we will carry it with two hands. If it is three feet square, we will get help in carrying it. We approach meetings differently if we know they will last 20 minutes, one hour, or three hours. The most common American coins and bills come in half orders of magnitude -- $0.01, $0.05, $0.10, $0.25, $1.00, $5.00, $10.00, and $20.00. The words "about", "approximately", and "nearly", when applied to quantitative measures, typically have some half order of magnitude as their implied precision, and add a fuzz around the judgment the width of that half order of magnitude. The word "several" usually indicates a half order of magnitude; we could state this succinctly as "Several squared equals ten." While we rarely know the precise measure of something on a scale, we often can say what half order of magnitude it is. In this book we will need only a predicate saying when two entities are the same half order of magnitude. This is straightforward to define. The proportion of the smaller to the larger is less than the square root of 10. Since we lack irrational numbers, we will square the proportion. (forall (x y s1 m) (40) (if (and (leqs x y s1)(measure m s1)) (iff (sameHOM x y s1 m) (exists (f f2) (and (proportion f y x m)(product f2 f f) (leq f2 10)))))) (forall (x y s1 m) (41) (if (and (gts x y s1)(measure m s1)) (iff (sameHOM x y s1 m)(sameHOM y x s1 m)))) The constraints on the arguments of "sameHOM" are as follows: (forall (x y s1 m) (42) (if (sameHOM x y s1 m) (and (inScale x s1)(inScale y s1)(measure m s1)))) Constants and Predicates Introduced in this Chapter The constants introduced were the integers 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, and 10. The predicates introduced were as follows: (nonNegInteger n): n is a nonnegative integer. (successor n1 n): n1 is the successor of n; n1 = n+1. (posInteger n): n is a positive integer. (sum n1 n2 n3): n1 is the sum of n2 and n3; n1 = n2+n3. (product n1 n2 n3): n1 is the product of n2 and n3; n1 = n2*n3. (lt n1 n2): n1 is less than n2; n1 < n2. (leq n1 n2): n1 is less than or equal to n2. (gt n1 n2): n1 is greater than n2. (geq n1 n2): n1 is greater than or equal to n2. (fraction f a b): f is the fraction whose numerator is a and whose denominator is b; f = a/b. (nonNegNumericScale s): s is a scale whose elements are nonnegative numbers, including 0, and whose partial ordering is "lt". (measure m s): m is a monotone increasing mapping from a scale s into a nonnegative numeric scale, mapping the bottom of s into 0. (proportion f x y m): f is the proportion or ratio of m(x) to m(y), where m is a measure on the scale containing x and y. (identityFunction f s): f is the function that maps every element of s into itself. (sameHOM x y s1 m): Two elements x and y of a scale s1 are of the same half order of magnitude under measure m. References: Hobbs, Jerry R., 2000. ``Half Orders of Magnitude'', KR-2000 Workshop on Semantic Approximation, Granularity, and Vagueness, Breckenridge, Colorado, April 2000; possibly to appear in Christopher Habel, ed. Resolution and Granularity. Hobbs, Jerry R. and Vladik Kreinovich, 2001. ``Optimal Choice of Granularity in Commonsense Estimation: Why Half Orders of Magnitude'', Proceedings, Joint 9th IFSA World Congress and 20th NAFIPS International Conference, Vacouver, British Columbia, pp. 1343-1348, July 2001.