**Mail folder:**Interlingua Mail**Next message:**sowa: "Re: Standardizing FOL"**Previous message:**sowa: "Standardizing FOL"**In-reply-to:**sowa: "Standardizing FOL"**Reply:**sowa: "Re: Standardizing FOL"

Message-id: <199309211953.AA18100@dante.cs.uiuc.edu> Reply-To: cg@cs.umn.edu Date: Tue, 21 Sep 1993 14:56:47 +0000 To: cg@cs.umn.edu, interlingua@isi.edu, sowa <sowa@turing.pacss.binghamton.edu> From: phayes@cs.uiuc.edu X-Sender: phayes@dante.cs.uiuc.edu Subject: Re: Standardizing FOL Cc: phayes@cs.uiuc.edu

Hi John! >When I talk about standardizing FOL, I mean the KIF and CG coaltion, >which supports metalanguage and context mechanisms that go far beyond >plain vanilla first-order logic. I understand, but the meta-meta heirarchy you outline isnt the same one as the higher-order heirarchy (of functions of functions of..)that we were talking about. The context mechanism doesnt go far beyond first-order logic, by the way, in fact it never goes beyond first-order logic. All it amounts to, as far as I can see, is a kind of quotation; but that hardly extends the semantic base at all. (Perhaps I am missing something, however.) But at the same time KIF & CGs go >beyond it in a way that allows you to define any kind of ontology or >system of inference that you prefer. You can define varieties of >temporal logic, modal logic, intensional logic, or even fuzzy logic. Maybe, but you can't define ANY kind. For example, it doesnt have the syntactic power to enable you to define lambda-conversion. And its not clear that this notion of 'define' always captures the semantics of the logics in question. (Although Im sure that it can be proved to do so in many cases.) >I didn't have a chance to catch up with my email last week, so here >are some comments on your note of September 14th: > >> ... And I don't think we need 'full-blown' >> higher-order logic. But consider the possibility of a second-order >> logic which is full-blown in this sense but restricted in other ways; >> a linear second-order logic, say; or a second-order logic whose >> quantification over predicates is restricted by some kind of context >> mechanism but otherwise full-blown (full-blown in a box, it might >> be called airbag logic). I'm making these up as I go along, but my >> point was that we need to be experimenting, not standardising. > >Yes, that is what we are doing with KIF and CGs. What they provide >is a hierarchy of metalevels. Start with a conventional domain of >discourse D -- say a typical first-order model -- and a first-order >language L0 that talks about individuals in D. (You can assume your >favorite syntax for L, since we are standardizing the semantics >and providing two starting syntaxes -- KIF and CGs -- but you can >define your favorite linear, graphic, or whatever syntax you prefer.) > >Then we have our next language L1, which is also first-order. Its >syntax is identical to L0, except for a little more vocabulary that >lets us talk about the language L0, the domain D, and the relationship >between L0 and D. In L1, we can extend L0 by giving new definitions. >We can even define what it means for a statement in L0 to be "true" >-- i.e. we can define a Tarski-style model theory or we can define >a Hintikka-style language game for L0. Yes, but your scare quotes are quite appropriate here. Its not clear that this notion of 'true' is the one which a genuine semantic theory would provide. Suppose I have a language LP with a model theory defined on it, and suppose we can describe the syntax of LP and its model theory in L1: call this the lp-theory. Now, take a first-order model of the lp-theory: will this be suitably isomorphic to a model of LP? Will every model of LP be suitably isomorphic to a first-order model of lp-theory? Neither of these questions has an obvious answer. ........ > >As far as airbags, we got 'em. The context mechanism in CGs draws >boxes around collections of propositions (theories, if you like). >Then outside the boxes, you can talk about what's inside, what it >means, how it relates to some other box, etc. No, you don't have them. I was imagining a 'context' syntax which would allow higher-order heirarchies to exist but with a limited range. The semantic difficulty with (fullblown) higher-order logic is that once one has specified the base domain I of individuals, the higher-order domains (I->I of functions from I to I, I->(I->I), etc etc) are all fixed: they contain ALL the relevant functions. If I is countably infinite then these must be uncountably infinite, so anything like a Herbrand theorem, and hence a completeness theorem, is impossible. Henkin models allow domains in which the functional heirarchy need not contain all the functions, but only enough to guarantee that any function nameable in the vocabulary is present. This is exactly what is achieved by a suitably rich collection of comprehension axioms, or a rather smaller collection of schemata. A simple first-order model would not even have this constraint, but would let (N->N) have, say, just two elements when N is the integers. What you can make the logic talk about is one thing, but what that talk means is another. Until you provide a model theory, its not clear what these internal translations and descriptions amount to. (Now do you see why I make such a fuss about the importance of semantics? :-) > >> I guess my most recurrent worry is this. One of the reasons we feel >> 'safe' with FOL is that while acknowledging that we will need extensions >> to it, we all feel that they will indeed be extensions, ie they can >> hardly be weaker than FOL. (After all, what would you take out? 'NOT', >> say? Nah...) But maybe this intuition is mistaken. Maybe in order to >> get the comfort back we will need to sacrifice some expressive power >> of FOL for something else, and do so in a systematic way which forces >> us to alter the semantic base significantly. > >Yes. But you can use the metalanguage to limit the expressive power >of what you can say in certain boxes. Thats not clear to me. But in any case, limiting what you are able to conclude doesnt give you the semantic insight I am worried about. Heres the point: any semantics, be it fuzzy or modal or whatever, thinks about a sentence as having some kind of property - truth, for example - which inference rules preserve somehow. So sets of sentences which are semantically interesting are always ones which are closed under the application of these rules. But we seem often to be dealing with sets of sentences which don't have this recursive-closure character. So how can they be characterised semantically? (Maybe this is not true of linear logics, and I confess to not yet understanding what the semantic base of linear logic could be.) ..... >What we are trying to do with KIF and CGs is to stop doing the useless >reinventing of the wheel and to start doing some productive kinds of >experimentation. Once we have a standard defined, then we can start >building tools that people can use to start the real fun of experimenting >on the definition of new theories without the dog work of implementing >a new parser, theorem prover, graphics display, debugging package, etc. >The real work is in defining new ontologies, I largely agree, defining theories is where the real work needs to be done. My worries were inspired by the thought that maybe some of our recurrent problems in doing this well are the result of not having the proper conceptual 'tools' (not the implementational stuff you are talking about, but the languages that underlie them.) not in working two years >to build the tools before you can even begin. And the tools require >standards. If building your tools requires standardising my tools, then its too early to be standardising. But lets stop arguing about this: I agree, if we can save some wheel-reinventing, that wont be a bad thing. Lets just bear in mind that research hasnt finished in this area, and not give students the wrong impression. Best wishes Pat ---------------------------------------------------------------------------- Beckman Institute (217)244 1616 office 405 North Mathews Avenue (217)328 3947 or (415)855 9043 home Urbana, IL. 61801 (217)244 8371 fax hayes@cs.stanford.edu or Phayes@cs.uiuc.edu