Re: A proposal of "sorts"
phayes@cs.uiuc.edu
Message-id: <199312071927.AA20886@dante.cs.uiuc.edu>
X-Sender: phayes@dante.cs.uiuc.edu
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Tue, 7 Dec 1993 13:30:48 +0000
To: Tomas Uribe <uribe@CS.Stanford.EDU>
From: phayes@cs.uiuc.edu
Subject: Re: A proposal of "sorts"
Cc: Interlingua-working-group@ISI.EDU, phayes@cs.uiuc.edu
>>> It is probably wise to
>>> have a special sort S, the sort of sorts, such that
>>> SortOf(?x,?y) => (SortOf(?y,?z) <=> ?z=S).
>
>Hmm, this does not allow for sorts to belong to any sort other than S;
Thats part of the idea. If we want to allow sort overloading then the
weaker version would be right. I guess this is probably best, on
reflection.
>why not just have instead
> SortOf(?x,?y) => (SortOf(?y,S)) ?
OK.
>>> Another advantage of this way of saying things is that it makes it
>>> (relatively) easy to describe different sort theories, ie the properties of
>>> different sorts...er, different kinds of sort.
>
>O.K., this is nice, but perhaps one could do something like this using
>the meta-reasoning capabilities that are already in KIF, and get away
>with writing "(sort (quote P))"? This would all just be a syntactic
>distinction anyway...
Different sort theories make really different assumptions about possible
relations between sorts, eg look at some of the things you cited in your
original message on this stuff. I don't think metareasoning would really
capture it properly. Someone might want to say that every sort has a
super-sort which contains it, someone else might want to deny this: these
are claims about the universe.
>
>>> An issue that arises in either case is how the sortal quantifiers are to be
>>> understood when a predicate is used which is not a sort. I can think of
>>> several answers: (1) all unary predicates are sorts, ie denying the
>>> validity of the distinction (2) a sortal quantifier is only well-formed if
>>> the predicate used is a sort (3) sorted assertions made with non-sorts are
>>> trivial, ie universal assertions are true and existentials are false.
>>> Answer 2 means that making an assertion using a unary predicate as a sort
>>> (or an individual as a sort in my transcription into first-order) asserts
>>> that the predicate (or individual) is in fact a sort, so it contradicts a
>>> denial of that status. I like answer 2 best, but can see the sense of all
>>> of them, and there amy be others. But we need to get clear about this,
>>> anyway.
>
>Well, my proposal was to have the "sortal" quantifiers just be syntactic
>sugar, i.e. (1);
But the sortal-ites will want to make these distinctions and give them
significance.
>my problem with (2) is that we would have to decide on
>what a "sort" actually is.
Why? All we need to say is that making sortal assertions also makes claims
about the sortal nature of the unary predicates (or individuals) mentioned.
That can also be syntactic sugar, and if one thinks that sorts really are
just unary predicates, they can simply assert that ALL unary prediacates
(or individuals, etc.) are sortal, thereby robbing the idea of any
significance while maintaining consistency.
>Perhaps an ontology for sorts along the lines
>you suggest above could be written for those people who really want to
>reason about such things, as distinct from unary predicates---or we could
>just have them write their own. :-)
Exactly. All I am proposing is giving them the logical handles to enable
them to do so.
Pat Hayes
----------------------------------------------------------------------------
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
hayes@cs.stanford.edu or Phayes@cs.uiuc.edu