tech:logic matters

["John E. Clifford" <pcliffje@CRL.COM>]

&:
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