Re: Many-sorted (or typed) logic
Chris,
The purely syntactic mapping of MSL into FOL does nothing
to change the semantics. Mike and I adopted that mapping
for the KIF and CG standards, since it was the simplest
and quickest way to support identical semantics for CG,
typed (or sorted) KIF, and plain vanilla untyped KIF.
But one can (and Solomon Feferman did) develop a model theory
directly for MSL, which shows that MSL is a nontrivial extension
of FOL that has many advantages over simple FOL. Following
is another quotation from Maria M's summary:
In 1967, Feferman pointed out that, concerning Craig's
interpolation lemma, the many-sorted language is better
because an improved version of it can be formulated and
proved on the premise of many-sortedness...
H. D. Ebbinghaus (quoted by Maria M.) says
It is especially with interpolation that many-sortedness
pays. As seen in Feferman (1974), the many-sorted version
of the interpolation theorem together with its possible
refinements is a powerful tool even for one-sorted model
theory, offering for instance elegant proofs of various
preservation theorems.
Maria M. also quotes a result by Hook (1985), who showed that
a many-sorted theory could be interpretable in terms of another
many-sorted theory without their one-sorted translations being
interpretable in one another. This property can be useful in
proving relative consistency of theories:
Even if another consistency proof is known, the proof using
interpretations has the advantage of being finitary and
purely syntactic.
>.... For example, for a language to have the power to
>express the notion "finite" is for there to be a sentence of the
>language that is true in all and only the finite models of the language.
>There is such a sentence in (true) second-order logic because the
>n-place second-order quantifiers of a second-order language are
>guaranteed by its model theory to range over the entire power set of nth
>cartesian product of the individuals of any model. The standard model
>theory for many-sorted languages does not impose any analogous
>restrictions on the ranges of the sorted quantifiers; the expressive
>power of these languages is equivalent to single-sorted first-order
>languages.
Standard MSL (not the syntactic translation of MSL to FOL)
has the correct properties: the quantifiers range over
every element of the sort declared for the corresponding
variables. Maria M. gives two different translations of
SOL into MSL. In the first (and simpler of the two), she
maps the second-order type into the second sort. This gives
an identical semantics, with the corresponding lack of
compactness and ability to define finiteness. In the second
mapping of SOL to MSL, she uses Henkin's general models.
You can do either or both in MSL, if you like.
>> 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.
>
>Not if by "power" you mean "expressive power".
The above remark has nothing to do with MSL vs. FOL. Going
to the metalevel gives you an enormous increase in expressive
power, with or without distinguising your sorts. You can,
for example, define truth and model theory for a language L0
with a pure FOL metalanguage L1. You can also define
provability at the metalevel and use it to define modal
operators (as in Dunn's semantics) at the object level.
Robert Kowalski has been using metalevel techniques in
logic programming since his 1979 book. It can do wonders
(independent of what version of negation you use).
John