Type Labels, Sorts, and Order Sorted Logic [Gentzen Syntax]

Topic
Logical System

8/30/09

Prerequisities

You need to know predicate logic to be able to understand this. Checking through Easy Deriver or Deriver would put would put you about where you need to be.

Skills to be acquired in this section:

To become familiar with type labeled and sorted logic.

Reading

[scan only]

K.H.Blasius et al. eds.[1990] Sorts and Types in Artificial Intelligence
Maria Manzano [1996] Extensions of First-Order Logic
John Sowa [2000] Knowledge Representation

G. Kriesel and J.L. Krivine [1971] Elements of Mathematical Logic
Hao Wang [1952]  'Logic of many-sorted theories', Journal of Symbolic Logic 17, 2 pp105-116

Introduction:

We know from Completeness, Compactness, the Lowenheim Skolem Theorem, and the Lindstrom Theorems [P. Lindstrom, On extensions of elementary logic, Theoria  35 (1969)  1-11. ] that First Order Predicate Calculus (FOPC) is pretty well where we want to be. [The first three theorems establish good properties for FOPC, and then Lindstrom shows that no stronger theory than, or extension to, FOPC has these good properties-- so FOPC is the strongest good logic.]

That FOPC is good does not mean that there are not advantages to dressing it up in certain ways to make it more amenable to humans, perhaps by adding what the computer scientists call 'syntactic sugar'.

One obvious opportunity concerns domains, ie what the variables range over. In FOPC we have the notion of an 'individual constant' and an 'individual variable' and the variables range over 'everything'. But this is a little at stress with how we think about many subject areas and how we reason much of the time. Beginning students are regularly baffled by universal statements like  'All men are mortal' , in particular what the 'all' ranges over and how the statement is to be symbolized. We, and the beginners, think that the universal statement is about men; then we learn that actually it is about everything, and, in particular, it should be rendered 'whatever x you choose, if x is a man, etc.'. Then, once we start deriving with our symbolized statements we make heavy weather of such inferences as ascending a hierarchy (such as 'All men are mortal', 'All mortal men are eventually die' therefore 'All men eventually die') or flat inferences on a common domain (such as 'All men are mortal', 'All men are kind' therefore 'All men are mortal and kind'). What slows us is dealing with the 'if-clause' all the time ('if x is a man').

Then, independently of this, many subject matters seem to have separate domains. For example, the tableaux or trees, dealt with elsewhere, are part of graph theory, and in the graphs of graph theory there are nodes, one domain, and there are links, a second domain. FOPC can deal with graph theory, using statements like 'if x is a node, etc. ' or 'if x is a link, etc.' but this is not the most natural. And this phenomenon is common place:-

  • in geometry, there are points and lines;
  • in an employment workplace there are people and there are their salaries ie different kinds of things.
  • in database design, there regularly is analysis in terms of entitites and their relationships, and this leads to different domains; for example, a simple database for a library will have the domain of patrons (borrowers/users ie people) and the second domain of books.
  • everywhere in computer science; for example, in any modern typed programming language there might be 'booleans'. 'integers', 'strings' etc., all of these are different domains.

There are two common approaches here: type labels or sorted logic. [The word 'types' gets used in different areas in logic-- here it is being used to identify what is known in computer science as 'data types'.]