There are many ways that the system of logical notation presented here might be extended. Our purpose in this section is to present one of them, many sorted logic, and to show that while this more complex notation might make logical formulas more legible to the human reader, it does not increase the expressive power of the system. We will be able to regard many sorted formulas as just being abbreviations for longer formulas in the system already presented.
Some situations naturally present themselves not as one universe, but as
two or more separate universes with various functions and relations
connecting them. For instance, in discussing the semantics of some computer
languages, one is tempted to have two
universes, the integers and the real numbers. Each universe has its own
equality and order relations and its own arithmetical operations. We
generally overload the symbols 
by using
the same symbols in both universes. The actual function represented by
a given instance of a symbol is to be determined by the type of its
arguments. This is known as polymorphism. In many computer languages
such as C++ you are permitted to overload your own function symbols.
In addition to the functions and relations within each universe there can
be functions and relations between the universes. For this example one
usually sees the function 
which maps an integer onto its
corresponding real value, and the function
mapping a real onto its nearest integer.
The logical language describing this situation would have to have two sorts of variables, real variables and integer variables. The meaning of a quantifier would be determined by the type of the variable it binds. For our example, let us follow precedent and declare that all variables whose name begins with the letters in the range h-n are integers while a-h and o-z are reals. We can write down the following true sentences:
Another example of a two sorted logic is the theory of points and sets.
Here we consider two universes, a universe of points whose only relation
is =, and a universe of subsets of the first universe, also with one
relation, =. The membership relation
denoted by the symbol 
connects these two universes. The usual
convention is that lower case variables range over points and upper case
variables range over sets. We have one important axiom for this theory,
the axiom of extensionality,
which says that two sets are equal if they
have the same elements.
Here are two more sentences in the theory of points and sets. One states that the empty set is in the set universe and the other that the point universe is a member of the set universe.
This logic of points and sets is sometimes called second order logic expressing the idea that sets have a higher order than points. If we were to include a third universe, sets of sets, the logic would have higher order. Ordinary unsorted logic is often called first order predicate calculus because one can think of its universe as consisting only of points, which are said to be first order.
We can now begin the process of incorporating many sorted logic into
our system of logic. In the first place, it is silly and old fashioned to
reserve different variables for the different types. The modern thing to do
is to allow any variable to be used
for any type but to require explicit type declarations. In logic this can
be accomplished with bounded quantifiers.
For the point, set logic for instance, we have two types, point and set,
and each quantifier must be bounded to
one of these types. The axiom of extensionality becomes
and the other two axioms become
So the task is really one of dealing with bounded quantifiers. To do
this make up one variable
relation symbols for each of the universes, say point(x) and set(X)
and use one new
universe equal to the union of the original two with the predicate point(x)
being true of just the points and set(X) being true of just the sets.
Then the bounded quantifiers can be easily eliminated with the rules
(using the notation
to mean replace A by B),
Likewise for points or any other types you might have. So for instance the above sentence about the empty set becomes
