From LOJBAN%CUVMB.BITNET@UBVM.CC.BUFFALO.EDU Wed Jan 10 14:25:42 1996
Received: from wnt.dc.lsoft.com (wnt.dc.lsoft.com [205.186.43.7]) by locke.ccil.org (8.6.9/8.6.10) with ESMTP id OAA11910 for <cowan@LOCKE.CCIL.ORG>; Wed, 10 Jan 1996 14:25:40 -0500
Message-Id: <199601101925.OAA11910@locke.ccil.org>
Received: from PEACH.EASE.LSOFT.COM (205.186.43.4) by wnt.dc.lsoft.com (LSMTP for Windows NT v1.0a) with SMTP id 81F392D0 ; Wed, 10 Jan 1996 13:56:58 -0500
Date:         Wed, 10 Jan 1996 10:42:31 -0800
Reply-To: "John E. Clifford" <pcliffje@CRL.COM>
Sender: Lojban list <LOJBAN@CUVMB.BITNET>
From: "John E. Clifford" <pcliffje@CRL.COM>
Subject:      tech:logic matters
X-To:         lojban list <lojban@cuvmb.cc.columbia.edu>
To: John Cowan <cowan@LOCKE.CCIL.ORG>
Status: OR
X-Mozilla-Status: 0001
Content-Length:  1671


&:
I have thought that {ro da poi kea broda cu brode} and {ro broda cu
brode} both give "Ax: broda(x) -> brode(x)" - with neither entailing
"Ex broda(x)". I assumed that it is in emulation of nat lang syntax
rather than predicate logic that these forms are used in preference to a
form with logical connectives (ganai...gi).
pc:
Well, _ro broda cu brode_ is both natural language and traditional
logic (and more advanced modern logic) form for a quantifier which
regularly in both those areas has existential import (implies there are
brodas) but is generally agreed not to be existentially importing in
Lojban. _ro da poi broda cu brode_  was devised to give a form with
exstential import and fits nicely into the pattern of restricting the
possibilities of what the sumti modified by _poi_ can be used for.
However, its official status is now in some doubt and at least xorxes
regularly asserted that it had no existential import.  In any case,
Ex:Fx => Gx does not imply ExFx (nor ExGx).

&:
It would be helpful if you would indicate what logical form corresponds
to {ro da poi kea broda} and {ro broda}.
pc:
Like so much of logical form representation, that for restricted (or
binary) quantifiers is not standardized.  The basic idea is apparent in
(Ax: x broda)x, a quantifier on x, restricted for values to brodas, and
what I take _ro da poi broda_ to represent.  In lambda terms it is
(roughly) \F(0=/= {y:y broda}c {z:Fz}), a quantifier = 2nd order
predicate.  I do not know what is the current state of _ro broda_ (nor,
for sure, that of _ro da poi broda_), but suspect it is \F(Ax:x broda =>
Fx), the modern universal.
pc>|83