Many-sorted (or typed) logic
Chris,
I'm sending this note from my other account because I'm again having
problems with my west.poly.edu account. I may have to switch to this
one permanently. Following are some comments about your recent note
and a bit more about many-sorted (or typed) logic.
John
PS: I noticed that Amazon.com is offering a second-hand copy
of the Meinke-Tucker book for $25. But they don't seem to have
new copies of either that book or the book by Maria Manzano.
The technology of printing books on demand is necessary
for keeping technical books in print. (Note that the laws
that govern this use of "necessary" are the economics of the
book publishing industry. For brevity, it is convenient to
leave the laws unspecified, but they're always there if you
look for them.)
>Ok, that's what I suspected you meant. But note that to retain the
>expressive power of SOL in the many-sorted language, as you suggested
>could be done, you have to build the semantic constraints on the
>interpretation of the higher-order quantifiers of SOL -- in particular,
>that they range over full power sets -- into the semantics of the sorted
>quantifiers of MSL; in which case you have simply created a notational
>variant of SOL, which I'm not sure is interesting for purposes of formal
>ontology.
There is no change to the semantics of MSL. The normal MSL semantics is
to restrict the range of the quantifiers to the specified sorts. If one
of the sorts is a power set, then the quantifier will happily range over
that sort. There is, of course, a change in the syntax used to write
the KR application. If you want f to be a quantified function variable,
you would have to write apply(f,x) instead of f(x). But that kind of
change is familiar to LISPers.
>And, of course, you lose completeness, compactness, etc --
>not that this is necessarily a disaster. (Indeed, as I recall, Fritz
>seems to think it is a positive virtue! ;-)
I don't consider it a virtue, but that comes with the territory.
If you want identical semantics, you get identical virtues and vices.
But as I have said, I believe that you get enormous power from the
multiple metalevels, which can handle a large number of valuable KR
techniques while retaining an FOL structure. In fact, many people who
use the term "HOL" are actually using metalevel quantification over
the syntactic constructs of the object language. (In fact, I think
that is what Cyc does.)
>Well, in this case, certainly "type" is appropriate, as the standard
>type hierarchy is an iterated powerset construction. But the fact that
>this is a special case is just why I'd want to avoid "type" for the more
>general "sort".
Following is a quotation from Maria M's introduction (p. 9 of the
Meinke-Tucker book):
Many-sorted logic is not only a natural logic for reasoning about more
than one type of object with an efficient proof theory, but also a
unifying logic for many other logics, even some non-classical logics
such as modal logic or dynamic logic.
The following list includes some of the logics that, in principle,
seem to be unifiable using many-sorted logic:
1. higher-order logics (type theory and second-order logic);
2. infinitary logic;
3. non-classical logics (modal, temporal, multivalued); and
4. logics of programs (dynamic logic, Floyd-Hoare logics).
Therefore, the study of many-sorted logic and its model theory gives
us a clue to the behavior of some other logics that can be translated
into many-sorted logic and also allows us an easy comparison among
different logics. We will see later two examples of a unified
treatment using many-sorted logic:
1. second-order logic with the general semantics invented by Henkin;
2. propositional dynamic logic.
In that same book, Tony Cohn has an interesting article about the
computational advantages of MSL for theorem proving. It is especially
valuable when there are large numbers of sorts organized in a lattice,
which is what we are assuming for the ontology.
John