12/13/09
Sorted Logic
(Many) sorted logic, with sorts or sort labels, is very similar in concept and execution to the types and type labels just discussed (in fact, many texts use the two terms interchangeably). There is, though, a conceptual difference. It is that whereas both ordinary logic and logic with type labels use one (homogenous) domain or universe, sorted logic uses a (usually stratified, heterogenous) domain which consists of two or more sub-domains.
An example will help.
Say we had a library with people borrowing books. The people are one type or sort of thing. And the books are another. In ordinary first order logic, the universe would consist of 'everything' and we would write such formulas as
Baw to mean 'Arthur borrowed Wuthering Heights'
Of course, Arthur is a person, and Wuthering Heights a book, but we probably would not bother about this, or if we did, we might write
Pa∧Bw∧Baw to mean 'Arthur is a person and Wuthering Heights a book and Arthur borrowed Wuthering Heights'
We would probably be more careful if quantifiers were involved, perhaps writing
(∃x)(Px∧Bw∧Bxw) to mean 'somebody has borrowed the book Wuthering Heights'
We could use type labels if we wished to type this
(∃x:p)(Bw∧Bxw)
with the variable 'x' still ranging over the entire universe.
With sorts, we say that actually the universe consists of two separate universes: a universe of people and a universe of books. And, back in the formal language, each universe has its own set of variables that range over it, so people has its variables and books its own variables. We need to denote these somehow, one way would be to superscript them. In our plain vanilla first order logic, our variables are such terms as
w,x,y,z
we could introduce some new variables
wp,xp,yp,zp
which would range only over the people universe and
wb,xb,yb,zb
which are different variables which range over only the book universe. Then the earlier formula would become
(∃xp)(Bw∧Bxpw)
The same treatment could be given to the constants. The constant for Arthur, a, is a constant that can range over people (and only over people) so we could write it ap, similarly for w, which ranges over books, so a new version for it might be wb. So we could end up with
(∃xp)(Bwb∧Bxpwb)
Mathematics seems to be full of sorts. For example, a mathematician will tell you that a vector space is a structure consisting of a set of scalars S and an entirely separate set of vectors V, some special elements which are scalars, another special element which is a vector, operations among scalars, operations among vectors, and some operations across both ie
a vector space = {S, V, etc.}
If we were looking for a 'natural' logic for this, there would have to be the temptation to have two domains (scalars, and vectors) and suitable constants and functions.
Signatures
Thus far, with syntax, we have allowed in special variables wp,xp,yp,zp and special constants ap,bp,cp. But actually this needs to be carried through for all the predicates and functions. For example, we have used Bxy to mean '(person) x borrowed the (book) y'. So, really, Bxy, conceptually or notationally, needs to be Bpbxy to mean that the predicate Bxy has a type or signature that requires that its first argument is a person and its second argument is a book. Then
Bpbaptb
is a perfectly good formula which might mean 'The (person) Arthur borrowed the (book) Tale of Two Cities'
On the other hand a string of symbols like
Bpbtbap
is not permitted or ill-typed or not well formed or is nonsense because the predicate 'borrowed' requires a person as its first argument and a book as its second, but this seems to have a book as its first argument and a person as its second. It is trying to say that Tale of Two Cities borrowed Arthur.
This typing can or perhaps should be carried out through all the syntax. A problem is that the formulas look very messy and proofs become obscure merely because of the notation. A somewhat more relaxed alternative is just to not write out the signatures explicitly all the time, but to understand they are there is the background. [There are results from elsewhere that have some bearing here. There is the Hindley-Milner type inference algorithm, which can determine and check types automatically. There are ways of checking the types even if we do not always write them out.]
Notation for signatures
Within the software here it is not easy to do signatures. The reason is a practical one that the character encoding for the web pages (Unicode) does not support real subscripts and superscripts for letters. So we could not superscript the variables even if we wanted to. But there is a way to simulate it. Unicode does support subscript numerals, and so does our software.
So, for example, instead of using special variables wp,xp,yp,zp , wb,xb,yb,zb , and special constants ap,bp, etc. We can give the number 1 to the first sort, and 2 to the second sort, and so on. Then use subscript one, two, etc. to indicate the sorts. So, for example,
B12x1t2
is a well formed and properly signed or typed formula. It uses the predicate B12 which requires two arguments, the first of sort 1, which it has x1, (which happens to be a variable) and the second of sort 2, which it has t2 (which happens to be a constant).
Translating in and out of types and sorts
We saw with the types that all that was needed to go into and out of types was for there to be a monadic predicate for each type. So, for example, if we wanted a type 'p' for 'people' we just needed a monadic predicate, say 'Px', for 'x is a person' and then 'All people die' is symbolized
(∀x)(Px⊃Dx)
and then into types by
(∀x:p)(Dx)
(and similarly for the existential quantifier). The types don't really add anything extra to the logic by way of what can be proved-- they just clarify and simplify for certain kinds of applications.
Sorts can be treated in much the same way. All that is needed to go into and out of sorts is for there to be a monadic predicate for each sort. So, for example, if we wanted a sort for person we just needed a monadic predicate, say 'Px', for 'x is a person' and then 'All people die' is symbolized
(∀x)(Px⊃Dx)
and then into sorts by
(∀xp)(Dxp)
(and similarly for the existential quantifier). This addresses the syntax.
If we wanted to have just two sorts, people and books, we could say that, or simulate that, with the formulas
(∀x)(Px∨Bx), ~(∃x)(Px∧Bx)
which say 'Everything is a person or a book' and, further, ' nothing is both a person and a book'.
The semantics, when going into or out of a sorted logic, recognizes differences between sorted and unsorted logic. If the logic is sorted to start with, it will have several separate universes (eg people and books), to get a single universe, these universes are just 'unioned' together; so, for example, with the mathematical vector space
a vector space = {{S union V}, etc.}
Going the other way the single universe is divided up into separate strata according to the kind of the items (eg whether they are people or books, or scalars or vectors). And the sorted constants (functions, predicates) are just brought in or left out as required-- the difference they make is with the semantics-- they have to be interpreted appropriately. There are details here, but the principles are clear, simple, and straightforward.
What can be proved in sorted logic versus what can be proved in ordinary predicate logic
The sorts don't really add anything extra to the logic by way of what can be proved-- they just clarify and simplify for certain kinds of applications. Anything provable in sorted logic can be proved in ordinary predicate calculus.
The reverse is usually not true, though.
In ordinary logic you can prove, say, 'If A then A' for any well-formed formula A. So you can prove the formal counterpart of 'If Tale of Two Cities borrowed Arthur then Tale of Two Cities borrowed Arthur'. But, in our sorted logic for libraries, illustrated above, you cannot even say 'Tale of Two Cities borrowed Arthur' because it is nonsense.
But, anything that is provable in ordinary logic, which makes sense in the sorted logic, is provable in the sorted logic.
Why use sorts?
Sorts can be more natural in certain settings. If sorts are not used, there has to be an 'extra' monadic predicate to do the work that the sort would do. In the earlier library example, there was talk of a sort for people and a sort for books-- in the unsorted case, that would require an extra predicate for people and another for books (not much perhaps). But in computer science there might be a specification for a programming language that wants to use signed and unsigned integers, reals, booleans, characters, strings, etc and wants to make such statements as 'adding a real to a real gives a real'. If such a specification is done in an unsorted logic, the monadic predicates (for 'real', 'integer', etc.) will clutter up the statements. Sorts would be much clearer here.
Sorts also make certain proofs more natural or elegant. The example often given is that of Craig's Interpolation Lemma (not explained here); advanced logicians argue that sorts make its proof easier.
There is also the question of whether sorts might help you to make sensible statements. Earlier we wrote
Baw to mean 'Arthur borrowed Wuthering Heights'
In ordinary (unsorted) logic Bwa is a perfectly good statement ie
Bwa to mean 'Wuthering Heights borrowed Arthur'
now, the view could be taken that this is just false, alternatively the view could be taken that it is a nonsense since books cannot borrow people. Sorts allow the codification of the second view. If the borrowing predicate Bxy has a sort restriction on it that requires its first argument to be a person and the second a book, the formula Bwbap would be nonsense.
Here is a more striking example that is common in the texts. Consider people and numbers. In ordinary logic
Julius Caesar is a prime number.
is a perfectly good statement. That means that it is either true or false. Of course it is not true. It is false. But that means that its negation is true. So
It is not the case that Julius Caesar is a prime number.
is true. All this is a bit odd.
In a suitable sorted logic
Julius Caesar is a prime number.
just would not make sense, and neither would
It is not the case that Julius Caesar is a prime number.
Order sorted logic
Another consideration is whether the sorts need to be disjoint ie the sub-universes have no members in common (they usually are disjoint eg nothing is both a person and a book).
Earlier, types proved to be useful with classification, for example
but stratifying the universe here does not seem wise (do we want to have a sub-universe of fish, and of mammals, or vertebrates, or what?). What seems natural with classification is to have one domain, period, and then for some items in that domain to have type 'fish' and some type 'mammal' etc. That is, type labels seem useful, but not conceiving those type labels as indicating disjoint sorts of the universe by stratifying the universe.
But there is a way to accommodate this. It is to not require that the sorts be disjoint. Sorts can overlap or be subsorts of other sorts.
That possibility is order sorted logic.