Re: Many-sorted (or typed) logic
Hans Chalupsky <hans@isi.edu> writes:
> >>>>> pat hayes <phayes@ai.uwf.edu> writes:
> > Now it is not hard to tweak the syntax of the logical language to
> > allow quantifiers over properties (and relations: again I won't
> > bother with the details). You just allow variables to be put in the
> > predicate position of an expression, ie you allow things like (?P a
> > ?x) as well as (P ?x ?y), and then you allow them to be quantified.
> > Nothing to it: CYCL does it without even batting an eyelid. (KIF
> > carefully excludes this, which IMHO is a major problem for using KIF
> > in ontology specification.
>
>Just a minor addition: KIF 3.0 (not the stripped-down KIF proposed as
>an ANSI standard) DOES allow second-order quantification via the
>`holds' predicate (which is defined via the primitive `member'
>relation). For example, the Ontolingua Frame Ontology uses `holds' to
>define the transitivity property like this (all variables are
>implicitly universally quantified):
>
> (<=> (Transitive-Relation ?R)
> (and (Binary-Relation ?R)
> (=> (and (Holds ?R ?X ?Y)
> (Holds ?R ?Y ?Z))
> (Holds ?R ?X ?Z))))
>
>Since you are working on a "CYClified version of KIF", you might want to
>consider this notation, since it already has seen extensive/some :-)
>use in various communities.
Thanks for the suggestion. This use of 'holds' is a well-known way of
transcribing higher-order quantification into first-order syntax, but
in my view it is more like syntactic vinegar than syntactic sugar.
What is gained by insisting that one write
(Holds ?R ?X ?Y) instead of just plain (?R ?X ?Y)? What this does in
effect is just to relocate the relation variable from the first place
in the expression, which removes it from the restrictions placed on
that position by the first-order reasoner. It would be simpler to
just remove those restrictions from the logical language itself. This
obviates the need for this clumsy variadic pseudorelation (I say
'pseudo' because it has no first-order theory, as indeed one would
expect it not to. Its only role is to act as a kind of relational
gap-filler. What (Holds ?R ?X ?Y) actually means is something like
(<blank> ?R ?X ?Y), which is better written without the blank.) The
major problem with the use of 'holds' is that it requires the logic
to support two distinct ways of asserting a predication. As well as
being clumsy, this forces a reasoner to perform dummy inferences
which amount to translations back and forth between these equivalent
versions.
>The only restriction for ?R is that it
>has to be a bounded relation (the specification of KIF 3.0 uses the
>notion of bounded sets and objects to avoid Russel's paradox). Not
>sure how this relates to your three choices of second-order universes.
The need to avoid the Russell paradox only arises if one allows
arbitrary predications, including self-applications of predicates (?P
?P) . I am quite happy to avoid that by the same trick which Russell
used, ie a strict heirarchy of types. (All three of the alternatives
second-order universes are typed, ie there is a clear distinction
between first- and second-order entities.) The KIF strategy is
adapted from later versions of set theory, which might indeed be more
'modern' if we were here doing mathematics, but mostly we are not.
Personally, I could go to my grave happy without ever worrying about
the set of all sets that are not members of themselves.
>Pragmatically, I don't think the choice matters much, since every
>inference engine expected to deliver results during the lifetime of
>its users will need to restrict reasoning with higher-order
>constructs, which in turn might effectively implement some of the more
>restrictive choices such as your #3. For example, a pragmatically
>sensible application of the above rule would be to run it forward and
>instantiate the transitivity rule for a specific relation `foo' (but
>usually not to prove `(Transitive-Relation ?R)' by going the other
>way). Advertisement: This is what PowerLoom does.
I agree with your general point about pragmatism, though with a
couple of comments. First, to some extent this kind of pragmatic
limitation applies to all inference, first-order as well as
higher-order; neverthless it is useful to get the underlying logic as
straight as possible. Second, what is pragmatically useful depends,
in general, on what one wants to do. For example, if a query was
about the transitivity of a relation, then applying the axiom in
reverse might be a sensible tactic. (What we really need is some way
to give useful tactical advice to a reasoner, and this is still an
open problem. A priori restrictions amount to 'blanket' advice such
as: never do this, or always prefer these to those.)
>Used in this form, the higher-order construct is really just a
>convenient way to represent an axiom schema, that could (in many
>cases) be replaced by a macro mechanism outside of the language
>without losing much.
I agree it is often useful to think of higher-order constructs as
amounting to schemas, but disagree that not much is lost by putting
these outside the language. The ability to say things about relations
is extremely useful (speaking now in an very pragmatic mode) and I
only came to appreciate it fully when I got used to being able to do
it, and felt the pain of subsequently trying to do without it.
Thanks for the suggestion, in any case.
Pat Hayes
---------------------------------------------------------------------
IHMC (850)434 8903 home
40 South Alcaniz St. (850)202 4416 office
Pensacola, FL 32501 (850)202 4440 fax
phayes@ai.uwf.edu
http://www.coginst.uwf.edu/~phayes