Re: Many-sorted (or typed) logic
> >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.
Yes, of course, we can take a *particular* model of SOL and turn it into
a *particular* model of MSL. You can also turn it into a model of
standard single-sorted FOL. (Just moosh all the domains of the first-
and higher-order quantifiers into a single domain and introduce n-place
predicates into your first-order language that are assigned the former
domains of the SO quantifiers as their intepretations.) But that
doesn't tell us anything about expressive power. The expressive power
of a language is gauged not relative to a single model, but to the class
of all of its models. 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.
> >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.
Not in the standard model theory for MSL. MSL is complete, compact,
the Lowenheim-Skolem theorem holds, etc.
> 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". In that sense, MSL (with
its standard semantics, of course) is nothing but syntactic fluff --
though heuristically useful fluff, I agree, and heuristic usefulness is
certainly not something I would gainsay when we're thinking about KR
applications. Moreover, there may be computational advantages as well,
as the Cohn article you mention suggests, and that could certainly be a
further reason for using MSL in certain circumstances. But I think your
general enthusiasm here is not properly apportioned to the logical
facts.
> >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.
Not sure what is meant by "unification" here; I've ordered the
Meinke-Tucker book. But I suspect it means something like the
representation of a variety of logics in a many-sorted languages,
perhaps with appropriately adjusted model theories.
> 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;
Right, the standard semantics for MSL corresponds very naturally to
Henkin's general semantics for higher-order languages -- which, with
that semantics, are no more powerful than first-order languages.
-chris
--
Christopher Menzel # web: philebus.tamu.edu/~cmenzel
Philosophy, Texas A&M University # net: chris.menzel@tamu.edu
College Station, TX 77843-4237 # vox: (979) 845-8764