Functions Expressing generality
One of the most important properties that a relation R may have is that of being many-one. This means that for any object x from the domain of discourse there is at most one thing y such that Rxy. A many-one relation is sometimes also said to be functional. If R is both many-one and connected, then for any x there is exactly one y such that Rxy, which is to say that there exists such a thing as the R-relative of x.
First order logic already has the resources to represent the logic of relations, and we can in principle sprinkle extra assertions about their functionality over arguments as needed, but this is cumbersome and tends to obscure rather than clarify the reasoning. Rather than write complicated and tedious quantified formulae everywhere, we shall follow standard practice and introduce function symbols into our formal language, and refer to the associated many-one relations as functions. A k-ary relation which is many-one with respect to its last argument place (that is, for any x1,...,xk−1 there exists at most one y such that Rx1,...,xk−1,y) is a k−1-ary function, taking k−1 things as its arguments and delivering (at most) one thing as its value for those arguments. If for all arguments there is exactly one value, then the function is said to be total; otherwise (if it may have no value for certain arguments) it is partial.
Examples of unary (or monadic) functions: 'the father of...' in the domain of people; 'the successor of...' in the domain of whole numbers. Examples of binary (dyadic) functions: the standard operators of basic arithmetic, 'plus', 'minus', 'times', etc. In mathematics, of course, functions are everywhere. If you have used Logic for Fun to formalise problems in first order logic, you will know that functions are everywhere else as well. It is therefore very important that our logical system should have the resources to handle them properly.
We shall use lower-case letters, usually f, g, etc., as function symbols in our formal language. Following the same conventions as Logic for Fun, we shall write the arguments as a comma-separated list enclosed in parentheses, after the function symbol. Of course, where a binary function symbol like '+' is more familiar in infix position (between its arguments) we shall allow ourselves the freedom to write it in the usual way. That is, we prefer to write 'a + b' rather than '+(a,b)', though if you feel that the latter looks "more logical" or something, you are free to write it that way!
Having function symbols in the language, we have to complicate the syntax a little. A referring expression will now be called a term. Names can be re-cast as 0-ary function symbols, since they do what function symbols do (refer to an object) but they do it without needing to be supplied with arguments. The set of terms may therefore be defined as the smallest set such that each term in it is an n-ary function symbol (for some n, zero or more) applied to n terms. The definition is not circular, since the inner terms (the ones to which the function symbol is applied) have to be provably terms by means of the definition, so they have to be shorter and simpler. Eventually, all terms have to start from function symbols without arguments, otherwise known as names. To illustrate, if a is a name (nullary function symbol), f a unary function symbol and g a binary one, then the following are terms:
a
f(a)
g(a, f(a)))
Our notion of substitution of variables for names (and names for variables) in formulae also has to be extended to allow substitution for terms, and substitution of one term for another. The rules ALLE and SOMEI have to be amended slightly to allow for terms of arbitrary complexity in place of just names. Thus ALLE, for instance, allows the inference from ALLv A to Atvwhere the latter is the result of substituting the term t for the variable v. This makes sense: if A is true of everything then it is true in particular of whatever the term t picks out, however complex t may be. The rules ALLI and SOMEE, however, require arbitrary names in their premises, and the role of these names cannot in general be played by compound terms.
The rules =I and =E governing the identity predicate (see below) also apply to general terms, not just to names. SP {ALLx (Fx IMP Ff(x)) ⊢ ALLx (Fx IMP Ff(f(x)))} PL {1} {1} {ALLx (Fx IMP Ff(x))} {A} PL {2} {2} {Fa} {A} PL {1} {3} {Fa IMP Ff(a)} {1 ALLE} PL {1,2} {4} {Ff(a)} {2, 3 IMPE} PL {1} {5} {Ff(a) IMP Ff(f(a))} {1 ALLE} PL {1,2} {6} {Ff(f(a))} {4, 5 IMPE} PL {1} {7} {Fa IMP Ff(f(a))} {6 [2] IMPI} PL {1} {8} {ALLx (Fx IMP Ff(f(x)))} {7 ALLI} EP|
|
fProof shows the amended rules in use. Notice that at line (5) we use ALLE substituting the compound term f(a) for the variable in line (1), but that the last line requires the term in line (7) to be a name rather than a compound.
Note that terms may substitute for subterms deep inside other terms. Substitution into terms is especially important in the case of equational reasoning (using the rule =E, to be introduced below) which allows substitution of equals for equals in arbitrary contexts. This form of reasoning is used everywhere in elementary mathematics to transform terms by rewriting them according to equations.
With function symbols in our language, we are able to formulate a great many interesting first order theories including arithmetic. Since numerals (0 , 1 , 2 ... ) are just names, while 'successor', 'plus' and 'times' are straightforward function symbols of one, two and two arguments respectively, the first order theory of arithmetic is reasonably simple to set up. Historically, the development of symbolic logic from the mid-19th century on was partly driven by the need to provide rigorous foundations for mathematics, so it is very important that the language of logic should be sufficient to express such concepts.