B5. FUNCTIONS AND SEQUENCES 1. Pairs and Functions The distinguishing feature of ordered pairs, or simply "pairs", is that they have a first and a second element. (forall (p) (1) (if (pair p) (exists (x y) (and (first x p)(second y p))))) We could define pairs in the traditional way in set theoretic terms. The pair is defined as the set {x, {y}}. This is certainly a model of the axioms involving "pair", but it would be pedantic to call this the definition. Two pairs are equal exactly when their first elements are equal and their second elements are equal. (forall (p1 p2) (2) (if (or (pair p1)(pair p2)) (iff (equal p1 p2) (and (pair p1)(pair p2) (forall (x1 y1 x2 y2) (if (and (first x1 p1)(second y1 p1) (first x2 p2)(second y2 p2)) (and (equal x1 x2)(equal y1 y2)))))))) That is, if either p1 or p2 is a pair, then they are equal if and only if they are both pairs, their first elements are equal, and their second elements are equal. The first and second elements of a pair are unique. (forall (p x1 x2) (3) (if (and (pair p)(first x1 p)(first x2 p)) (equal x1 x2))) (forall (p y1 y2) (4) (if (and (pair p)(second y1 p)(second y2 p)) (equal y1 y2))) A function f from a set s1 to a set s2 is a set of pairs where each element of s1 occurs exactly once as the first element in a pair, and every element of s2 occurs as a second element of at least one pair. We will call this predicate "function0" because in Chapter B7 we will extend it to functions from scales to scales as well. (forall (f s1 s2) (5) (iff (function0 f s1 s2) (and (set s1)(set s2) (forall (p) (if (member p f) (and (pair p) (forall (x y) (if (and (first x p)(second y p)) (and (member x s1) (member y s2))))))) (forall (x) (if (member x s1) (exists (p) (and (member p f)(first x p))))) (forall (p1 p2 x) (if (and (first x p1)(first x p2) (member p1 f)(member p2 f)) (equal p1 p2))) (forall (y) (if (member y s2) (exists (p) (and (member p f)(second y p)))))))) Lines 4-10 of this definition say that a function is a set of pairs, the first elements of which come from s1 and the second elements of which come from s2. Lines 11-14 say that there is a value of the function for every element of s1. Lines 15-18 say that that value is unique. Lines 19-22 say that every element of s2 is a value of some member of s1 under the function f. We won't use these terms formally, but we can call s1 the domain of the function and s2 the range. (forall (f s1 s2) (if (function0 f s1 s2)(domain s1 f))) (6) (forall (f s1 s2) (if (function0 f s1 s2)(range s2 f))) (7) If f is a function from s1 to s2, we will say that f maps an element x of s1 into an element y of s2 when the pair is a member of f. (forall (f x y) (8) (iff (map f x y) (exists (s1 s2 p) (and (function0 f s1 s2)(member p f) (first x p)(second y p))))) That is, "(map f x y)" means "f(x)=y". As an aside, we note that when we have a Skolem function, or a functional dependency, we have a corresponding function. (forall (y1 y x1 x e s1 s2) (9) (if (and (skfct y1 y x1 x e)(typelt x s1)(rangeFd s2 y x e)) (exists (f) (and (function0 f s1 s2) (forall (p) (iff (and (pair p)(first x1 p)(second y1 p)) (member p f))))))) 2. Sequences Here we will assume we have the positive integers, as described in Chapter B9. The expression "(posInteger n)" says that n is a positive integer. The expression "(ints s n1 n2)" says that s is the set of all positive integers from n1 to n2, including n1 and n2. (forall (s n1 n2) (10) (iff (ints s n1 n2) (and (posInteger n1)(posInteger n2)(set s) (forall (n) (iff (member n s) (and (posInteger n)(leq n1 n)(leq n n2))))))) A sequence of length n is a function whose domain is the first n positive integers. (forall (s) (11) (iff (sequence s) (exists (s1 s2 n) (and (function0 s s1 s2)(ints s1 1 n)))))) We define "length" as follows: (forall (n s) (12) (if (sequence s) (iff (length n s) (exists (s1 s2) (and (function0 s s1 s2)(ints s1 1 n)))))) The nth element in a sequence is the entity in the range of the function that n is mapped into. (forall (s n y) (13) (if (sequence s) (iff (nth y n s)(map s n y)))) The first element of a sequence is the nth element where n is 1. (forall (s y) (14) (if (sequence s) (iff (first y s)(nth y 1 s)))) Note that "first" is the same predicate we used for the first element of a pair. Formally, there is no confusion because all axioms involving the predicate "first" are conditioned on its second argument being either a pair or a sequence. Intuitively, any confusion is harmless, because the set of pairs is isomorphic to the set of sequences of length two. The rest of a sequence is the sequence that remains after the first element is removed. (forall (s1 s) (15) (iff (rest s1 s) (and (sequence s)(sequence s1) (forall (i x) (iff (map s1 i x) (exists (j) (and (gt j 1)(successor j i) (map s j x)))))))) The expression "(rest s1 s)" says that s1 is the rest of s (after the first is removed). For example, the sequence viewed as a function maps 2 to b. Then the sequence maps 1 to b. The last element of a sequence is the nth element where n is the length of the sequence. (forall (s y m) (16) (if (and (sequence s)(length n s)) (iff (last y s)(nth y n s)))) An entity is in a sequence if it is the nth element of the sequence for some n. (forall (x s) (17) (iff (inSeq x s) (exists (n) (nth x n s)))) If one element's n is less than another's, it is before the other in the sequence. (forall (x y s) (18) (iff (beforeInSeq x y s) (exists (n1 n2) (and (sequence s)(nth x n1 s)(nth y n2 s) (lt n1 n2))))) We won't need infinite sequences. Predicates Introduced in this Chapter (pair p): p is an ordered pair. (first x p): x is the first element of a pair or sequence. (second y p): y is the second element of a pair. (function0 f s1 s2): f is a function from s1 to s2. (domain s1 f): s1 is the domain of function f. (range s2 f): s2 is the range of function f. (map f x y): The function f maps x to y; f(x)=y. (ints s n1 n2): s is the set of positive integers from n1 to n2, including n1 and n2. (sequence s): s is a sequence. (length n s): n is the length of the sequence s. (nth y i s): y is the ith element of sequence s. (rest s1 s): s1 is the rest of the sequence s after the first element of s. (last y s): y is the last element of sequence s. (inSeq y s): y is an element of the sequence s. (beforeInSeq x y s): x comes before y in the sequence s. In addition, the following predicates will be explicated in Chapter B9. (posInteger n): n is a positive integer. (leq n1 n2): n1 is less than or equal to n2. (successor n1 n): n1 is the successor of n; n1=n+1. (lt n1 n2): n1 is less than n2. The constant 1 will also be explicated there.