Example of a theoryNext Things Next

Here is another example – not a problem this time, but a small theory about animal husbandry and the properties of ruminants:

Mary had a little lamb
Its fleece was white as snow
And everywhere that Mary went
The lamb was sure to go.

The sorts include enumerations of the relevant colours and sizes of animals, and also non-enumerated sorts such as people and timesteps. The relationships between all of these are what the problem is about.

The vocabulary needed to express this series of propositions about Mary is worth a second look. “Mary” is of course the name of a person, so Mary is forced to be of that sort: she cannot, for instance, be an animal or a colour. The ownership relation between persons and animals is symbolised by the word “had”. This is a binary predicate, so we can write “Mary had x” or “had(Mary,x)” as we please. Stature and colour are properties of animals only, but location needs to be assigned to people as well as to their animals. Consequently, we need two “location” functions, one for each of the two argument types. We make location of persons surjective, although this is not stated in the rhyme, to ensure that the places listed are all places where Mary went – or at least places where somebody went!

On solving, we find that the solutions are much as might be expected. The first models the solver comes across are those in which there is one person (person zero) called Mary and one animal (animal zero) which is a little lamb owned by Mary. However, some of the solutions have unexpected features. For instance, there are solutions in which the lamb is green – but it is still just as white as snow because snow is purple! Well, we didn’t tell the solver what colour snow normally is, so we get what we asked for!

Logic is like that – what you (literally) say is (exactly) what you get.