Correction to a proposal of "sorts"

• Mail folder: Interlingua Mail
• Next message: phayes@cs.uiuc.edu: "Re: A proposal of "sorts""
• Previous message: Tom Gruber: "what is the "all" in KIF's forall ?"

Date: Tue, 7 Dec 93 00:18:27 -0800
From: Tomas Uribe <uribe@CS.Stanford.EDU>
Message-id: <9312070818.AA06709@Xenon.Stanford.EDU>
To: Interlingua-working-group@ISI.EDU, uribe@CS.Stanford.EDU
Subject: Correction to a proposal of "sorts"

As Pat Hayes was quick to point out, the restricted existential
quantifier is obviously meant to be translated into a *conjunction*
and not an implication (I only had the universal case in mind originally)
---my apologies about that!

A sentence of the form (exists (x) (=> P(x) <sentence>)) is trivially
true if P is not true of everything; one really wants an "and" instead of
the "=>". So, the syntactic sugar is really meant to work as follows:

=-=-=-=-=-==-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

Add, as syntactic sugar to quantifiers, the constructions
        (exists ((?x P)) <Sentence>)
and
        (forall ((?x P)) <Sentence>)
as abbreviations for
        (exists (?x) (and P(?x) <Sentence>))
                      ^^^
and
        (forall (?x) (=> P(?x) <Sentence>))
respectively. In general,
        (exists ((?x1 P1) .. (?xN PN)) <Sentence>)
abbreviates
        (exists (?x1 ...?xn) (and (and P1(?x1) ... PN(?xN)) <Sentence>))
                              ^^^
and
        (forall ((?x1 P1) .. (?xN PN)) <Sentence>)
abbreviates
        (forall (?x1 ...?xn) (=> (and P1(?x1) ... PN(?xN)) <Sentence>))

=-=-=-=-=-==-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=

- Tomas E. Uribe				uribe@CS.Stanford.EDU