Re: A proposal of "sorts"
phayes@cs.uiuc.edu
Message-id: <199312062357.AA17704@dante.cs.uiuc.edu>
X-Sender: phayes@dante.cs.uiuc.edu
Mime-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Date: Mon, 6 Dec 1993 18:00:43 +0000
To: Tomas Uribe <uribe@CS.Stanford.EDU>, Interlingua-working-group@ISI.EDU
From: phayes@cs.uiuc.edu
Subject: Re: A proposal of "sorts"
Cc: phayes@cs.uiuc.edu
Tomas-
I agree that sorts are best viewed as predicates, but have a few remarks on
your message. First, the existential case uses conjunction rather than
implication:
Add, as syntactic sugar to quantifiers, the constructions
(exists ((?x P)) <Sentence>)
and
(forall ((?x P)) <Sentence>)
as abbreviations, respectively, for
(exists (?x) (& P(?x) <Sentence>))
and
(forall (?x) (=> P(?x) <Sentence>)).
So the general construction for all quantifiers does not work.
Without this, the generalised DeMorgan rule for quantifier negation isnt
correct: but in any case, this is surely the intended meaning of the sorted
existential quantifier. Your version : (exists (?x) (=> P(?x) <Sentence>))
is true if ANYthing NOT of sort P exists.
A rather deeper issue is that proponents of sortal syntaxes are willing to
admit, under pressure, that sorts are semantically the same as unary
predicates, but they still want to distinguish these sortal predicates in
some way, for dark purposes of thier own. KIF needs to respect this, and so
needs some way in which one can assert OF a unary predicate that it is a
sortal predicate; and this seems to be an essentially second-order kind of
assertion.
If one want to keep things first-order (this paragraph will be trivially
true of Fritz Lehmann :-) one way to do it is to transform them from
predicates to individuals of category Sort, and have a relation SortOf
between things and sorts which says that thing is of that sort. The
connecting axiom is then (written in second-order, but its really no more
than a schema):
(forall(?P)(Sortal(?P) =>
(exists(?p) (Sort(?p) &
(forall (?x) (?P(?x) <=> SortOf(?x, ?p) )))))
You might want to have the first => be <=> to give a kind of extensional
identity to sorts, but this is often inappropriate. It is probably wise to
have a special sort S, the sort of sorts, such that
SortOf(?x,?y) => (SortOf(?y,?z) <=> ?z=S).
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.
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.
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