# 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
*x*_{1},...,*x*_{k−1}
there exists at most one *y* such that
*R**x*_{1},...,*x*_{k−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*)))

*g*(*a*, *f*(*a*))),*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
ALL*v* *A* to
*A*^{t}_{v}where
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.

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.