2013
Type labels are one way to approach what seem to be different domains in use in the same reasoning. What we are going to do here is to tag the variables with a type to indicate that they are subject to a particular monadic (one-place) predicate applying to what they pick out. An example will help, say 'All men die' is symbolized
(∀x)(Mx⊃Dx)
and our domain of reasoning (our interest, our ontology) has a lot to do with men (eg All man this, Some men that, etc.); we will let the monadic predicate Mx (x is a man) become a type tag on a quantified variable, thus
(∀x:m)(Dx)
The notation (∀x:m) is read 'Whatever x you choose of type m' . For our software system, we need here some convenient correspondence between the monadic predicates and the type labels. We have as monadic predicates Aa, Bx, Cx.... Zx ie we use the upper case letters A through Z. For types, we will just use the lower case letters a through z, and let the upper case predicate correspond to the lower case version of the same letter. So, as examples of this notation, here are some equivalences between the short form and the long form
(∀x:m)Dx≡(∀x)(Mx⊃Dx)
(∀x:a)Dx≡(∀x)(Ax⊃Dx)
(∀x:b)Dx≡(∀x)(Bx⊃Dx)
Our software supports this notation, and, with linear derivations, the abbreviation and expansion are carried out by rewrite rules. (See the Help Video below).
This then allows us to write inferences like 'Socrates is a man, all men are wise, therefore, Socrates is wise' as follows:
Ms, (∀x:m)Wx∴Ws
Our trees or tableaux support type labels directly. Here are trees for the above inferences.
Much the same can be done with existentially quantified formulas. For example, say 'Some men die' is symbolized
(∃x)(Mx∧Dx)
and our domain of reasoning (our interest, our ontology) has a lot to do with men (eg All man this, Some men that, etc.); we will let the monadic predicate Mx (x is a man) become a type tag on a quantified variable, thus
(∃x:m)(Dx)
The notation (∃x:m) is read 'There is an x of type m such that ...' . =
(∃x:m)Dx≡(∃x)(Mx∧Dx)
(∃x:a)Dx≡(∃x)(Ax∧Dx)
(∃x:b)Dx≡(∃x)(Bx∧Dx)
Our software also supports this notation, the abbreviation and expansion are carried out by rewrite rules.
and in Trees
So, conceptually at least, a database for a library might contain statements like
(∀x:p)(∀y:b)Bxy 'Any patron is permitted to borrow any book.'