Re: Many-sorted (or typed) logic
On Fri, Jul 21, 2000 at 10:26:16PM -0500, John F. Sowa wrote:
> But one can (and Solomon Feferman did) develop a model theory
> directly for MSL, which shows that MSL is a nontrivial extension
> of FOL ...
Right. This is exactly what I was arguing you would have to provide for
MSL in order for it to sustain the claims you were making about its
virtues. That was my only point, and you seemed to be denying it in
your last post -- though perhaps I misunderstood you. I don't know
Feferman's semantics for MSL, but am anxious to learn about it.
> >> 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 have spoken a number of times about "going to the metalevel." I'm
not sure what you mean by this. Do you just mean reasoning in the
metalanguage of a given language? Or are you talking about bringing
self-referential mechanisms into the object language itself? (KIF
currently seems to use "meta..." in this way.) Or do you mean some
third thing?
> You can, for example, define truth and model theory for a language L0
> with a pure FOL metalanguage L1.
Looks like you are just talking about what we do in our ordinary
"Tarskian" metatheory for FOL. So I guess by "going to the metalevel"
you mean the first of the two meanings above. Not that this sort of
"going to the metalevel" isn't a very cool thing, but it's not exactly
news.
Regards,
-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