Many-sorted logic More about first order logic


Page under construction: do not trust!

As will have become apparent from the formalisation exercises in Logic for Fun, it is important for knowledge representation purposes to have notation for quantifying over things of different sorts. Using a many-sorted version of first order logic instead of the standard single-sorted one not only makes facts and situations easier to represent and the resulting formulae easier to read, but also helps direct the search for proofs by blocking substitutions (of terms for variables) that are not going to be helpful.

There is no difficulty in principle in accommodating multiple sorts in our interpretation of logic. Each sort has its own domain over which variables of that sort are to range. Sometimes, as in Logic for Fun, sorts are required to be disjoint (not overlapping); more elaborate systems allow things to be instances of more than one sort, so that the sorts form a lattice with possibly complex inclusion and exclusion relationships. In a single-sorted logic, function symbols and predicate symbols need only be described in terms of their arity (number of argument places). In the many-sorted case, however, they have different types depending on the sorts of their arguments and, in the case of function symbols, on the sort of their value. Logic for Fun goes one step further, making 'bool' just another (small) domain consisting of the two truth values, so that it does away with predicate symbols altogether in favour of function symbols whose value type happens to be 'bool'.

Extending the natural deduction calculus to deal with sorts is also not difficult, but complicates the notation somewhat, so we shall not pursue it very far here. Briefly, the predicate symbols, and function symbols if those are present, must have their types somehow declared before the proof, as in Logic for Fun, and then each quantifier ALLv or SOMEv should be elaborated to specify the sort over which the variable v is to range, giving something like ALL(v: s) or SOME(v: s), where s is the name of a sort. The sorts of variables and names, must match the declared types of the predicates applied to them, as in the syntax of Logic for Fun. Also as in Logic for Fun, the sort specifications of variables may sometimes be omitted in practice, where the information is deducible from their positions in formulae. Apart from the additional notational details, the inference rules do not need to be altered, though the need to check types everywhere makes the calculus rather cumbersome to operate—at least, for human beings.

: What a many-sorted proof might look like.
Here s and t are sorts. Each variable has its sort specified in the quantifier, and the sort of each name is noted when it is introduced. This version of first order logic is hardly convenient for human reasoners!

It is worth noting one or two important differences between quantifying over sorts and the use of restricted quantifiers as above. One is that any predicate, expressed using any combination of connectives and quantifiers, may be used as the "sort indicator" of a restricted quantifier, whereas true sorted quantifiers are limited to ranging over pre-defined and named sorts. Another is that the domain of any sort is required to be non-empty: in the jargon of logic, sortal quantifiers have existential import. The effect of this is secured in deductions by insisting that there be names of every sort. By contrast, restricted quantifiers, of course, may be vacuous—it is true in the real world that all unicorns have wings, since all Fs are Gs if there are no Fs, and this may be said using a restricted quantifier; but in the real world unicorns are not a sort, so this truth cannot be expressed directly by means of many-sorted logic.