Re: Standardizing FOL
sowa <sowa@turing.pacss.binghamton.edu>
Reply-To: cg@cs.umn.edu
Date: Thu, 23 Sep 93 07:30:12 EDT
From: sowa <sowa@turing.pacss.binghamton.edu>
Message-id: <9309231130.AA13137@turing.pacss.binghamton.edu>
To: cg@cs.umn.edu, interlingua@isi.edu, phayes@cs.uiuc.edu,
sowa@turing.pacss.binghamton.edu
Subject: Re: Standardizing FOL
Pat,
> But be careful: a sort heirarchy is not a type heirarchy, ie ,
> a higher-order heirarchy.
No, of course not. But see my comment about Goedel below.
> It lets you make assertions of the same syntactic form, but they
> *aren't* saying the same things, as you correctly observe! In
> contrast, there are some second-order theories whose
> intended models are genuinely second-order, but which are in
> fact decideable. So this is a delicate area.
Yes, I agree.
> COLORED Petri nets? Well, every man to his taste, as I am
> sure you agree.
"Color" is just his name for "type" or "sort". Some people call
them "flavors". I suppose you could also call them "smells".
Every man to his own sensory modality.
> This is the kind of thing that McCarthy and Guha and others are
> developing at Stanford and MCC. But you can't do what they are doing
> just with quotation. If I simply quote (the text of) a theory, all I
> have is a string of symbols. To do the reasoning necessary, one needs
> to be able to say things like true-in(p,c) where both this and
> p are wffs of the logic. This is a genuine extension to
> the logic and it requires a delicate hand to get its semantics right.
> Its not just a relation between a string and something.
Yes, of course! We are not disagreeing at all. The only claim
I am making is that we provide the basic mechanism with which people
with delicate hands can draw masterpieces and clumsy people will
make a mess. The best analogy is to an operating system with
hierarchies of virtual machines. Inside any VM, you can build another
hierarchy of VM's or you can get yourself hung up in an infinite loop.
But the overall operating system keeps on running, and your local
problem doesn't affect anyone else.
> Notice I said DEFINE, not program. I dare say you can hack it up: after all,
> FOL can be regarded as a programming language.
Hackers and masters use the same tools. You can hack up or
"define" lambda conversion or anything else you like.
> NO! Use of natural language is almost never a use of FOL or any other
> formalism. If it were this trivial to transcribe NL into FOL then AI work
> in NL understanding would have been finished years ago. (Theres a deeper
> reason why not, which is that natural languages are different in kind
> from formal logics. I don't expect to able to convince you of that here
> if you don't believe it, so just go with the complexity argument.)
Of course, we have no disagreement on this point. To be explicit,
let me take Goedel's famous paper as an example. It is written in
a natural language -- German. Goedel uses German as a metalanguage
to define a bunch of recursive functions, most of which are primitive
recursive. The critical one Beweisbar [provable] is recursive, but
not primitive recursive. That collection of recursive functions on
the integers itself forms a metalanguage, and what G. is effectively
saying with that metalanguage are the axioms and proof procedures
of higher-order logic.
You could translate Goedel's definitions into KIF or CGs -- certainly
not automatically, I never made such an outlandish claim. Stefan
Bauer-Mengelberg, a former colleague of mine, did an excellent job
of translating it from German to English, and other people who tried
have not done as well. But once you have done that translation to
FOL, you are using pure FOL as a metalanguage in the same way that
Goedel used German as a metalanguage. Then the recursive functions
that G. defined become another metalanguage in which you can define
the axioms for any HOL theory that you like.
Whether you say that Goedel "hacked it up" or created a masterpiece
is irrelevant. The point is that it can be done.
> No. You miss the point. Even if you can describe the inference rules, etc.,
> that you need - and its not obvious to me that you always can, by the way -
> that doesnt specify the semantics. And it was the semantics I was worrying
> about.
Of course! We are not disagreeing at all. I am like an operating system
developer. My responsibility is limited to providing you with a context
mechanism in which you can do anything you like without disturbing other
people who are working in other contexts. The semantics of what you
define or "hack up" is your responsibility, not mine.
> Then this is just a programming language, not a Krep language, standardised
> or otherwise.If all the Krep aspects of the standard are not going to be
> used by me as Krep, then they just get in the way. Why should I not just
> use PROLOG or LISP? (Or C++, which is rapidly becoming a de facto standard
> anyway.)
Finally, we are getting to the point. All we are doing with KIF and
CGs is giving you a version of sorted FOL with metalevels that you can
use as a programming language. The argument for FOL is that it is
much simpler and better defined than Prolog, Lisp, C++, SQL, or any
others we could name, it is at least as powerful if not more so than
any of them, and it has been a de facto standard for over a century.
> ... but you also imply confidently and authoritatively - as you
> did in this very message - that they make masses of fundamental research
> unnecessary. Contexts? We got 'em! Different semantic bases? We can hack
> up anything! For years Ive been pointing out that some new representational
> idea is just another notation for FOL. But thats not because I think FOL is
> the answer to everything. On the contrary, I want us to go beyond it, and I
> shoot lame horses. Nonmonotonic reasoning genuinely goes beyond FOL, for
> example. The message that started this sequence merely expressed a concern
> that the way in which we need to go beyond it might, just might, involve
> a fundamentally different way of thinking about semantics. So we
> shouldn't stop thinking about semantics.
Again, I don't believe that we have any fundamental disagreement on
this point. I am not saying that we are making "masses of fundamental
research unnecessary". What I am saying is that we are providing the
mechanisms that enable you to do that research without spending two
years building tools before you can get started. Again, look at the
example of operating systems: giving people hierarchies of virtual
machines doesn't stop research -- it gives researchers the tools to
build totally new kinds of systems of their own. And it also gives
application developers tools that they can use to build end user
packages for people who don't care at all about what's under the covers.
Your point that building tools may not be so easy is certainly well
taken. A lot of creative thinking will be necessary to design tools
that are easy to use, efficient, flexible, robust, industrial-strength,
etc. And it won't be done all at once. But the important thing is to
have standards so that you can upgrade from one tool to the next one
without making your previous knowledge bases obsolete.
John