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.