User:Jochen Burghardt/sandbox5

Many-sorted logic

Mathematical logic, in general, is concernd with "calculating" with propositions rather than with numbers. As a simple example, applying the negation operator to the proposition "Every human owns some animal" yields "Some human does not own any animal".

While unsorted first-order logic allows quantifiers, like "every", ""some", and "any", to range only over the whole domain of discourse, many-sorted logic allows quantification over appropriately defined subdomains.

Therefore, both example propositions are admitted only in a many-sorted logic defining both "human" and "animal" as an own subdomain each; in unsorted logic, e.g. the first proposition would have to be rephrased as "Everything which is a human owns something which is an animal".

While in the many-sorted version, both "human" and "animal" are sorts, i.e. designate subdomains, in the unsorted version both are predicates.

To check the truth of the sorted version, it is sufficient to consider every human, checking if (s)he owns an animal.

To check the truth of the unsorted version, it is necessary to consider everything at all, checking if it is not a human or if it owns an animal.

The difference becomes more clear when using common formal notation to express the first proposition: "∀x:human. ∃y:animal. owns(x,y)" in the many-sorted version vs. "∀x. human(x) ⇒ ∃y. animal(y) ∧ owns(x,y)".

Many-sorted logic can reflect formally our intention not to handle the universe as a homogeneous collection of objects, but to partition it in a way that is similar to types in typeful programming. Both functional and assertive "parts of speech" in the language of the logic reflect this typeful partitioning of the universe, even on the syntax level: substitution and argument passing can be done only accordingly, respecting the "sorts".

There are more ways to formalize the intention mentioned above; a many-sorted logic is any package of information which fulfills it. In most cases, the following are given:

• a set of sorts, S
• an appropriate generalization of the notion of signature to be able to handle the additional information that comes with the sorts.

The domain of discourse of any structure of that signature is then fragmented into disjoint subsets, one for every sort.

Motivation

In (first-order) mathematical logic, as in natural language, propositions can be built from terms (object names, like "Kermit", or "17") and predicates (property names, like "is green", or "is prime"). In an unsorted logic, an elementary proposition can be built by applying an arbitrary predicate to an arbitrary term, so that "Kermit is green" and "17 is prime" are admitted propositions, but "Kermit is prime" and "17 is green" are, too. A main aim of many-sorted logic is to forbid the latter two nonsensical compositions. To this end, distinct sorts of objects are introduced, and each predicate is restricted to an appropriate sort. In the example, two sorts "physical object" and "number" could be defined, "Kermit" and "17" could be assigned to the first and second sort, respectively, and the predicate "is green" and "is prime" could be restricted to accept only terms from the first and the second sort, respectively. This way, the nonsensical compositions can be forbidden as syntactic incorrect.

Similarly to a predicate, a function can be restricted to a sort, too; e.g. "center of gravity of" and "square root of" can be applied in a sensible way only to a "physical object" and a "number", respectively.

As another example, when reasoning about biological creatures, it is useful to distinguish two sorts: plant and animal. While a function mother: animal → animal makes sense, a similar function mother: plant → plant usually does not. Many-sorted logic allows one to have terms like mother(Lassie), but to discard terms like mother(my_favorite_oak) as syntactically ill-formed.