Re: SUO: Comments on Whitten's Starter Ontology
Before I get into the details of replying to Chris Menzel's
comments on the starter Structural Ontology, I would
like to publically acknowledge all the work and thought
that he has put into reviewing this document.
I appreciate his careful attention and feel that he is
providing a valuable service to the SUO study group
as well. I applaud his dedication and skill.
David (whitten@lynx.eaze.net) (713) 791-1414 ext 6116
>The scope of your starter ontology is impressive, indeed,
> somewhat overwhelming.
I would hope that the scope is what is necessary
to provide a structural ontology for the SUO effort.
The SUO itself, as I understand it, has a much larger
scope commensurate with its aims.
> I have interleaved comments with quoted text below.
> But in general, I am seriously concerned with
> several issues:
>1. The general point. I am not sure what you are doing.
> It looks to me that you are building a single first-order
> theory that is trying perform at least three functions:
> (a) Defining the syntax of SUO-KIF (or some language
> or other); here I reference your point about needing
> more of your "rules" of KIF, as well as all of the
> syntactic stuff like "length", "valence", etc.
> (b) Defining the semantics of KIF. Here I reference the
> NAME-OF relation as well as your axioms for a lot
> of traditional semantic categories like relation.
> (c) Axiomatizing some of the central categories of an SUO, e.g.,
> CLASS, INDIVIDUAL, and NUMBER.
>
> Thus, I think you are ignoring certain traditional, well
> understood divisions of labor.
This is very encouraging to me, and in fact one of the aspects
that I believe makes this SUO effort attainable. We have a
large number of people from diverse backgrounds willing to
work together to create a well-rounded, carefully considered
standard upper ontology. It is heartening to know that
there is a traditional, well understood division of labor
for this kind of work.
Most of my background is in linguistics and computer science
with my knowledge of logic primarily from self study.
I do know a bit about denotational semantics of programming
languages
In the process of expressing this Starter Structural Ontology,
I attempted to use the KIF syntax. From my reading of the
document at: http://ltsc.ieee.org/suo/suo-kif.html,
I see a description of the semantics of the KIF language.
I also see a BNF-like grammar specifying the syntax of
sentences.
As you can see, the semantics description in the KIF document
is in English, not in KIF, or any other formal notation.
One of my hopes in creating this ontology is to make explicit
in KIF what the semantics of KIF should be for the SUO.
I did not include very much of this, as this is the beginning
of my effort. It may be that my preference for self describing
systems is logically untenable. I am not as gifted a logician
as others on this list, and am willing to be taught.
I do not see the axioms for LENGTH and VALENCE as defining
the syntax of KIF, but in specifying restrictions on expressions
in KIF. I agree that they are 'syntactic' restrictions, in that
they specify meta assertions which are necessary for all
assertions that exist in a knowledge base.
> 2. General conflation of object language and metalanguage.
> This is sort of a corollary to the first point, but is in my
> opinion particularly critical to note explicitly.
> Syntactic and semantic definitions traditionally go into
> a metalanguage. Putting them into the object language
> along side a lot of straight ontological content is just a
> potential source of both conceptual confusion and,
> worse, logical incoherence. This raises the third point.
It is true that the object language and metalanguage are
conflated in my presentation. I hoped that presentation
of this ontology would show the need that the SUO
group has for well defined boundaries between the
object language and the metalanguage, as well as the
metametalanguage, etc.
It is possible that, just as the LENGTH and VALENCE
relations are not strictly necessary, as Adam Pease has
pointed out, the identification of what makes up a
statement in the object language and what makes up
a statement in the meta language may not be necessary.
This automatic identification could follow a procedure
such as : 1) identify the object or meta level that each object
referenced in the sentence is introduced into the logical
system. 2) if any variables are used that are instances
of an object referenced, then the sentence that uses
them is of one higher meta level than the object referenced.
3) identify the entire sentence with the meta level
one higher than the highest level of any meta levels identified
by 1) or 2).
Even with this automatic identification process in place,
I would prefer that we identify what language a given
statement is intended to be a part of. It seems clearer
and of at least as much utility as any other structural
relation in the ontology.
I also think we need to be clear on three other methods
that seem to be used by logicians, which I do not
see reflected in the SUO-KIF document. These are
the use of "schema", "abbreviations" and
"definitions of terms".
For the logicians among us, I'm sure these methods
are comfortable and powerful tools.
I personally don't see anything in the document for
SUO-KIF that states that they are allowed in a knowledge
base. The closest meaning I have come up with is
that schema may be interpreted as sentences in a metalevel
language that represent a possibly infinite number
of sentences in the 'object' language below.
Abbreviations and definitions appear to be similar to
macro substitution in a programming language,
and seem to be a metalevel language sentence that
is a 'short-hand form' for some object level language
sentence.
Perhaps someone can point out in the document
http://logic.stanford.edu/kif/dpans.html or
http://ltsc.ieee.org/suo/suo-kif.html where these
methods are supported ?
> 3. Questionable and insufficient axiomatizations. Many of
> the notions you introduce are not adequately axiomatized.
> ASSERTION is a good example. You say that this is the
> class of all assertions expressing a sentence, but about all
> we get for axioms is that assertion is a class and its instances
> are individuals. But that doesn't distinguish assertions from
> any other class of individuals.
Absolutely true. I am open to including any axioms in the
starter structural ontology that you may suggest. I wanted
to include what I knew. This seems to have some
overlap with the discussion on a separate thread of ambiguous
versus indefinite.
If you might give me some advice, I ran into a problem with
KIF syntax in that the 'obvious' characterization of
stating that all sentences are instances of ASSERTION,
looks like a statement that the results of a function
are elements of the class ASSERTION.
(forall (?REL ?X)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?X INDIVIDUAL)
(INSTANCE-OF (?REL ?X) ASSERTION)
)
)
Using two statements didn't seem adequate either :
(forall (?REL ?X)
(=>
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?X INDIVIDUAL)
(and
(= ?ASRT (?REL ?X))
(INSTANCE-OF ?ASRT ASSERTION)
)
)
)
Aside from the issue of the syntax looking
like I'm looking at the function result is the
separate issue that these statements could be
interpreted as saying only statements that are known
to be true are instances of the class ASSERTION.
> Thus, none of the *intended* content of this term
> is captured in the axioms.
> Axioms for CLASS and NUMBER are similarly
> inadequate, and potentially inconsistent -- notably, you
> explicitly introduce a class of all classes and assert its
> self-membership. (Such axioms belong in separate ontologies
> anyway, IMO).
I agree that the Axioms for NUMBER are inadequate.
I waited a month or more for someone else to volunteer
axioms suitable for inclusion. I don't believe those I included
are wrong, however. As someone else pointed out, the
ontology currently only uses numbers as identifiers for
positions in an assertion. As presented in version two,
I only use the NUM-SUCC and NUM-< relations
to define the VALENCE and LENGTH relations.
The formalization I provided, to my knowledge only
defines the integers from zero through ten.
And only defines them sufficiently for the axioms
that they are used in. If I had used a class
ORDERED-POSITION, rather than NUMBER,
I would have had the same axioms.
I do not believe I intended to state that
the class of classes was a subclass of CLASS.
I stated:
R072: (INSTANCE-OF CLASS CLASS)
The meaning I intended is that the object whose
name is "CLASS" is a member of the class of
those objects which are treated as classes by
other axioms. I realized this was self referential.
I certainly did not intend that it was problematic logically.
Another way of stating this, that any assertion
that requires in argument position N, an object
that is a class, shoul glad. Its hard to determine the
right way to deliver ideas to such a
varied group as ours.
> > (NTH-DOMAIN ?REL ?POS ?TYPE)
> > - the argument in position ?POS
> > of relation ?REL is a member
> > of class ?TYPE.
> Note this needs to be cashed as discussed
> earlier, or else you are proposing quantifying
> over relations and numbers, which requires a
> *lot* of work, and a lot of expressive power.
I don't think we want to quantify over all
numbers. In fact, there has been some
discussion on a separate thread that I have
gone far beyond what anyone needs in going
up to 9-ary relations.
> > ?POS=0 is used for the return type
> > of functional relations.
>
> If by a functional relation you are really talking
> about a *relation*, then its "value" should be
> its second argument place, and hence ?POS=2
> should be the position of its "return type",
> shouldn't it? Typically, a functional relation
> is just a relation R such that Rxy & Rxz => x=z.
I believe this was added by Adam to avoid the
creation of a separate relation such as
(RESULT-DOMAIN ?REL ?TYPE)
- the relation ?REL may be used as a function
symbol in KIF expressions and the result is
a member of class ?TYPE.
I did not use functions in this version of
the starter structural ontology, and in fact,
have a separate thread discussing how we
want to deal with functions. I also
brought up functions for states of matter
previously.
> > (VALENCE ?REL ?COUNT)
> > - the COUNT of arguments that the
> > relation ?REL can take is the number ?COUNT
> > Note: an assertion is not stated when a
> > relation can take an arbitrary NUMBER of arguments
> I am concerned that metalanguage and
> object language notions are getting
> mixed together here.
> > (LENGTH ?ASRT ?COUNT)
> > - the count of arguments that are present
> > in the assertion ?ASRT is the number ?COUNT.
> > ?COUNT=0 is used for an assertion with
> > only the relation present.
> Ditto, only more so.
Both of these relations, in my mind, are statements
in some meta level of the logic system as they are
stating restrictions on sentences on a lower level.
Since we don't have a clear idea what our various
meta levels are for SUO, I have not included those
notations with these statements.
> We now appear to be taking *assertions* to be
> first-class objects as well. You say below that
> an assertion is "the class of all assertions
> expressing a sentence." But what sort of
> thing is that?
Actually I intended to state that the class
namsed on the structures in this
ontology, not to some inherent
number-ness qualities.
> >COUNT
> > - class of numeric individuals
> > expressing a quantity.
> Don't you just mean numbers here?
I have COUNT and POSITION as
separate classes because I used them
differently. I wasn't comfortable with
the idea that the 'length' of a sentence
was a POSITION, when I knew it
was a count of how many individuals were
arguments in the sentence.
Perhaps I should rename NUMBER as NUMERAL
use NUMERAL instead of POSITION,
and use NUMBER for where I used COUNT.
Then use some relation to generalize
an ordered class, and make NUMERAL and NUMBER
subclasses of that ordered class ?
This seems to be a general principle. the
same objects (0,1,2...10) are used as a POSITION
and as a COUNT, but their meaning is subtly
different.
> > ASSERTION
> > - class of all assertions
> > expressing a sentence
> Again, how does an assertion differ
> from a sentence, and what is it
> for an assertion to express a sentence?
As you and Adam have argued, this
class should be renamed SENTENCE.
> Rules:
> R001:
> (forall (?ANY)
> (= ?ANY ?ANY))
>
> > R002:
> > (forall (?ANY)
> > (not (\= ?ANY ?ANY)))
> I think it is preferable just to define \= as (not (= ... ))
We should state this in the KIF document.
I don't know of any problems with this.
However, my suggestion that \= become a
variable valence relation might affect this.
The meaning I hoped we would add
was that if (\= 1 2 3 4) is true,
then I know
(and (not (= 1 2))
(not (= 1 3))
(not (= 1 4))
(not (= 2 3))
(not (= 2 4))
(not (= 3 4)))
if you have no problem with this being
the same as (not (= 1 2 3 4)) from a logical
perspective, I don't either.
> R003:
> (forall (?X ?Y)
> (not (and
> (= ?ANY ?ANY)
> (\= ?X ?Y))))
I cannot parse this. Can you say it in English?
This was a tired-o. ( was tired when I typed it)
I intended to say two variables can't be equal
and not equal at the same time.
> > ;;Leibnitz's Rule
> > R004:
> > (forall (?X ?Y ?REL ?POS)
> > (=>
> > (= ?X ?Y)
> > (and
> > (NTH-ARGUMENT ?ASRT 0 ?REL)
> > (NTH-ARGUMENT ?ASRT ?POS ?X)
> > (NTH-ARGUMENT ?ASRT ?POS ?Y))))
> I don't think you want a conjunction in the consequent here.
> Essentially, I think you are trying to say that if ?X and ?Y are
> identical, then IF you have some *true* atomic sentence, you can
> replace occurrences of ?X with occurrences of ?Y in the sentence and
> the result will be true as well.
Actually, if I recall correctly, I was trying to say that
this replacement would be valid for any sentence.
I was not thinking of the truth value of the sentences.
My intent for this ontology was only to deal with the structure
of the ontology and leave semantics for later.
As a point of query though, why would I not want a conjunction there?
The axiom:
R004:
(forall (?X ?Y ?SENT ?REL ?POS)
(=>
(INSTANCE-OF ?SENT SENTENCE)
(INSTANCE-OF ?REL RELATION)
(INSTANCE-OF ?X INDIVIDUAL)
(INSTANCE-OF ?Y INDIVIDUAL)
(INSTANCE-OF ?POS POSITION)
(=>
(= ?X ?Y)
(and
(NTH-ARGUMENT ?SENT 0 ?REL)
(NTH-ARGUMENT ?SENT ?POS ?X)
(NTH-ARGUMENT ?SENT ?POS ?Y)
)
)
)
)
is how I would have stated this axiom if I had reviewed it a day
later (it was one of the last axioms I included in the ontology)
But I'm not sure that it is general enough, none-the-less.
I think the dependency you see on only true sentences is tied
up in the axioms of NTH-ARGUMENT, which I didn't intend.
> Aside from the fact that this is not general enough, this rule
> highlights my concerns about serious confusions of object language and
> metalanguage in this document. Thus usual way of expressing this law
> (it's not what is usually called Leibniz' Law) in a first-order
> language is by means of a schema using the notion of substitution: for
> any sentence A (of SUO-KIF), the following is an axiom:
> (forall (?x ?y)
> (=> (= ?x ?y)
> (=> A A'))),
> where A' is the result of replacing every free occurrence of x' in A
> with an occurrence of y'. You are pushing everything into the
> object language, and the result seems quite messy.
I easily could have misunderstood what a colleague referred
to as Liebniz's Law. but your restating of my desired statement
indeed captures what I recall I was wanting to say.
Of course, to do so, you have used a schema, which we don't
have SUO-KIF. Could that be stated as an axiom in the metalanguage?
> > R004: ;; Everything is an instance of "TOP"
> > (forall (?ANY)
> > (INSTANCE-OF ?ANY TOP))
> >
> > R005: ;; There exists something
> > (exists (?ONE)
> > (INSTANCE-OF ?ONE TOP))
> This follows from R004 and the theorem of first-order logic that
> something exists. By the way, are the axioms of first-order logic
> supposed to be among your rules or not? You have identity axioms, but
> none for boolean connectives and quantifiers, nor do you state any
> inference rules.
I would think that a reflective system would have
as axioms (on some meta language level) all axioms
of the logic that it is intending to implement.
I only began with identity axioms because they
were easy. My concern is that all of the first-order
logic axioms may be viewed as tautologies to a system
that already has them built-in. My understanding of
the goal behind the lattice of logical theories is that
in some logical theories of the lattice they are
tautologies, but in others, they may need to be explicit.
> > R006: ;;Every class is a subclass of "TOP".
> > (forall (?TYPE)
> > (=>
> > (INSTANCE-OF ?TYPE CLASS)
> > (SUBCLASS-OF ?TYPE TOP)))
> >
> > ...
> > ;(NTH-DOMAIN ?REL ?POS ?TYPE)
> > ; - the argument in position ?POS
> > ; of relation ?REL is a member of class ?TYPE.
> > ; ?POS=0 is used for the return type
> > ; of functional relations.
> >
> > ;; define signature of "NTH-DOMAIN" relation
> Note that on the suggestion that nth-domain statements be treated as
> abbreviations, "nth-domain" is not a genuine predicate, and hence
> needs no signature.
I'm not sure how to answer this, since I haven't heard your
opinion on whether abbreviations, schema, and definitions
can be treated as metalevel language sentences.
Since I'm hoping the SUO is self reflective, I'm assuming
I will still need to define the signature of all relations,
regardless of the metalevel on which they are defined.
> > ;(NTH-ARGUMENT-NAME ?R ?P ?S)
> > ; - the documented preferred name of the variable
> > ; in position ?P used in expressing assertions
> > ; with relation ?R expressed as a string ?S.
>
> I'm sure you don't really mean to be talking about names for
> variables, but rather for values of variables. But at any rate,
> again, this seems to be pushing all sorts of metalinguistic stuff into
> the object language. It just doesn't belong there.
Actually, this relation is solely for documentation, so I am
indeed intending that it is specifying a string used for representation
of the variable used by relation when a sentence is in some 'text form'.
> > ;(NAME-OF ?INS ?NAME)
> > ; - A name of the individual ?INS as a string ?NAME
> > ; ?NAME cannot be the empty string.
> > ; two assertions in the same context cannot
> > ; have the same string as a name.
> More of the same, only now you are introducing explicit semantic
> relations into the picture. Very dicey stuff. Moreover, you are
> building all sorts of semantics into your predicates that are not
> propertly axiomatized. What is a context, for example? This is a
> large and complicated topic in AI.
I actually used "context" when I intended to use "knowledge
base" as defined the SUO-KIF document.
I didn't intend to be bringing in semantic relations. I was intending
to be relating the internal form of an instance with a string that
would be suitable to represent it in a 'text form'.
If I had not released this ontology when I did, there would have
been some axiom saying that when the individual was a sentence,
that the variable names would have matched one of values stated
for the NTH-ARGUMENT-NAME string. But I'm sure that would have
been tricky to express.
> > R039: two individuals can't have the same name
> > (forall (?INS-1 ?INS-2 ?STR)
> > (not
> > (and
> > (\= ?INS-1 ?INS-2)
> > (NAME-OF ?INS-1 STR)
> > (NAME-OF ?INS-2 STR)
> > )
> > )
> > )
> Certainly a strong rule -- but again, one that belongs in a
> metalanguage.
And in fact, one that I think of as belonging on a metalevel.
> >;ASSERTION
> >; - class of all assertions
> >; expressing a sentence
> >R040: (INSTANCE-OF ASSERTION CLASS)
> >R041: (SUBCLASS-OF ASSERTION INDIVIDUAL)
> The notion of "expressing a sentence" is not axiomatized.
I agree this is a (too) weak axiomatization for ASSERTION
(or even for SENTENCE).
> > ;(NTH-SUBCLASS ?REL ?POS ?TYPE)
> > ; - the argument in position ?POS
> > ; of relation ?REL is a subclass of class ?TYPE.
> > ; ?POS=0 is used for the return type
> > ; of functional relations
> Problems like those that arose for nth-domain will arise here.
Agreed, and should be handled in the same way.
> > R072: ;; "CLASS" is an instance of CLASS
> > (INSTANCE-OF CLASS CLASS)
>It does indeed appear that you are treating all classes as
>individuals. And now you have the universal class and are claiming
>that it is an instance of itself. These are dangerous waters. There
>are serious issues that must be addressed with your class and number
>axioms. Notably, there are already well-known axiomatizations of
>number. You are reinventing the wheel here.
I welcome any pointers or contributions you or others may
make to increase the robustness of this ontology.
> > ;(LENGTH ?ASRT ?COUNT)
> > ; - the count of arguments that are present
> > ; in the assertion ?ASRT is the number ?COUNT.
> > ; ?COUNT=0 is used for an assertion with
> > ; only the relation present.
> I have trouble understanding the motivations for all of these
> syntactic analysis predicates, except insofar as they serve your
> method of putting everything in the object language.
The intent was to provide a 'first line of defense' on
what are well formed formulas in the knowledge base.
By axiomatizing the rules we would use on recognising
the structures of an ontology as an ontology, I see
we can work out what we want for a standard SUO
object language and metalanguage, as well as using
the tools we are developing for ontology analysis.
David (whitten@lynx.eaze.net) (713) 791-1414 ext 6116