Re: Standardizing FOL
sowa <sowa@turing.pacss.binghamton.edu>
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