Re: Standardizing FOLphayes@cs.uiuc.edu
Date: Tue, 21 Sep 1993 14:56:47 +0000
To: email@example.com, firstname.lastname@example.org,
Subject: Re: Standardizing FOL
>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
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
not in working two years
>to build the tools before you can even begin. And the tools require
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.
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
email@example.com or Phayes@cs.uiuc.edu