**Mail folder:**Interlingua Mail**Next message:**Fritz Lehmann: "Higher-order KIF & CGs"**Previous message:**phayes@cs.uiuc.edu: "Re: Standardizing FOL"**In-reply-to:**phayes@cs.uiuc.edu: "Re: Standardizing FOL"

Reply-To: cg@cs.umn.edu Date: Mon, 27 Sep 93 01:29:10 EDT From: sowa <sowa@turing.pacss.binghamton.edu> Message-id: <9309270529.AA19020@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, Some comments on your last, final word: > A semantics isnt (usually) the kind of thing that fits inside a computer: > that's a category mistake, like asking the weight of the letter 'J'. A > semantics is an account of how expressions inside computers might relate to > ways the world might be. Giving a semantics for a logic isnt a process of > programming. Its a process of explaining rigorously (mathematically, if you > like) what the expressions of the logic are supposed to mean. KIF and/or > CG's won't provide me with tools for doing this, and my doing it couldnt > *possibly* have anything other than intellectual effects on anyone else. If > I make a mess of my semantics, nobody but me will ever know unless I try to > publish it. Offering to provide a standard shell to develop semantics > within, like an operating system for software, seems crazy. I know you > aren't, so we must not be understanding one another. Yes, of course. We both agree on that point completely. But there is a difference between giving a semantics for a language and giving a semantics for a metalanguage. The model theory for the KIF and CG framework is purely first-order. The domain of discourse for the multiple levels of metalanguages is some basic domain of individuals and relations that you start with. Then the domain of discourse for the higher levels is the union of the basic domain plus the linguistic expressions plus the metalinguistic expressions plus the metametameta... But every level is purely first order. Therefore, we have a very classical, very simple model theory. Now let's consider McCarthy and Guha's contexts. I am certainly not claiming that we are in any way duplicating their work or making it unnecessary. All I am saying is that the CG contexts as mapped into the KIF quotes provide a facility in which the McCarthy and Guha axioms can be written. They can write their import and export axioms in the metalanguage facilities of KIF and CGs. Our work by no means makes their axioms redundant. On the contrary, we are depending on people like them to write such axioms in order to make our contexts usable. But the semantics of their axioms are not our responsibility. They have to ensure that their axioms are meaningful and consistent for some subject that they are trying to express. The analogy to an operating system was intended to suggest that a knowledge base constructed on top of KIF and CGs (or for that matter on top of Cyc, which is already implemented) would resemble a hierarchy of virtual machines in which what is expressed in one context would be isolated from other contexts -- except for explicit import and export operations that are stated at the metalevel outside of the contexts. Each metalevel, of course, is itself within some context. All we are claiming is that the framework is consistent, not that the axioms stated within any framework are guaranteed to be consistent. > PS I didnt mean 'hack' to connote bad or careless programming: in the > culture I grew up in, hackers were regarded with awe. I meant only to > distinguish programming or describing a syntactic form (maybe in a > metalanguage) and defining a concept in a logical language. A definition > would, for example, enable you to draw conclusions from assertions using > that syntax. KIF and CGs are logical languages. Every axiom stated in them has implications that are precisely defined by the semantics. But all we are claiming is that we take responsibility for the framework, not for any axioms that anyone might choose to express in the framework. > The reason you can't define lambda-conversion in FOL is that its definition > essentially involves a schema which is not equivalent to any finite set of > first-order expressions (in contrast, for example, with the schema for > equality). True. But the schema for language Li can be stated in language Li+1. Each language and metalanguage is finite, but it can be used to state axioms that can be used to generate an indefinite number of instantiations at the level below. We have several different hierarchies in KIF and CGs: the hierarchy of types (or sorts, or colors, or flavors, ...); the hierarchy of nested contexts; and the hierarchy of metalevels. These hierarchies are largely independent, although the hierarchy of metalevels requires the hierarchies of contexts: each metalanguage statement talks about what is inside some CG context or KIF quoted expression. This provides an extremely powerful system, although from a model- theoretic point of view, the entire framework is first order. John