Tree Tutorial 6: Functional Terms and First Order Theories

Logical System


The word 'terms' in logic means 'names' and thus far we have met two kinds of terms: constants (or proper names), and variables.

These are not the only names there are. In English consider 'the father of Betty' -- now, this is not a statement, it does not say something true or false, rather it is a construction which names an individual. It takes Betty and what we might call the 'father of' function and uses the two of those to name an individual. Similarly in mathematics, the expression 7 + 2 does not assert something true or false, rather it is a construction which names a number (which also happens to have the name 9).

The logic we are studying, so called 'First order logic', can accommodate these fancy terms, and it does so by means of 'functional terms'.

Here is a characterization of our syntax for functional terms

  • any constant is a functional term.
  • any lower case letter followed by ( followed by any number of functional terms, separated by commas, followed by ) is a functional term.
  • and these are all the functional terms there are.

For example, a, b, c, f(a), g(b), g(a,c), h(g(c),b), aFunctionalTerm(withAnArgument) ... are all functional terms.

To symbolize, say,

'The father of Betty is kind'

we choose, say, f(x) to represent the 'father of x' function, b to represent Betty, and Kx to represent the predicate 'x is kind' and the whole lot becomes:


[We could also have symbolized this Kind(fatherOf(betty)). This same process is extended to arguments. So the argument

Everything is kind.
Betty's father is kind.

could be

∀xK(x) ∴ K(f(b))

And, of course, this is valid and closing a tree for it is simple.

Functional terms often appear in identities. For example

Allison’s brother’s wife’s sister is her very best friend.

might be symbolized


where a=Allison, b(x)= is the brother of x, s(x)= is the sister of x, w(x)= is the wife of x, f(x)= is the very best friend of x,

Functional terms have an 'arity', which, roughly, is the number of arguments they apply to. Remember with predicates you can have one place predicates like F(x), and two place predicates, or relations, like T(x,y) (and three place...). So too with functional terms. The 'father of' function is of arity one-- it expects one term as an argument. In mathematics there are plenty of functions of higher arity. For example, the plus function usually expects two arguments, so 'plus x y' might be represented p(x,y).

Actually, there is another small issue that comes up here. The way we write functional terms is to write the function first, followed by the arguments. In math, a fair few functions are 'infix', that is to say they are written between their arguments instead of before them-- mathematicians generally write (1 + 2) not +(1,2).

[For your information, our tree rules are configured to do minimal formal arithmetic and it is familiar with the following conventions:-

It knows about + ('plus') and . (times) and ' (successor of), and 0,1, 2. + and . are infix and successor is postfix (it comes after its argument) and 0,1, 2 are just the constants 0, 1, 2. 'successor of' just means the number plus one (so the successor of 3 is 4 etc.) It can read an expression like the following K((0+0')) and what this says is that '0 plus the successor of 0 has the property K'.

None of these extended capabilities are of immediate interest to us.]

Using functional terms in trees does not require any additional rules. When there are functional terms in trees, the most likely tree rules to be in use are Identity (to substitute one term for another), and occasionally functional terms are used as instantiations of the Universal quantifier.

Functional terms also often appear in so-called 'First Order Theories', which are areas of mathematics that have been characterized or axiomatized using ordinary predicate logic with functional terms. We will briefly consider three examples: groups, arithmetic, and set theory.