Message-Id: <199402151920.AA02609@eli.CS.YALE.EDU>
Date:         Tue, 15 Feb 1994 18:30:00 GMT
Reply-To: i.alexander.bra0125@oasis.icl.co.uk
Sender: Lojban list <LOJBAN%CUVMB.bitnet@YaleVM.YCC.YALE.EDU>
From: i.alexander.bra0125@OASIS.ICL.CO.UK
Subject:      Re: TECH: Quantifiers (was: cukta)
To: Erik Rauch <rauch>
Status: RO

la kau,n. tu'a mi spuda di'e
> > ... but there is no place in such a description where a prenex could have
> > occurred.  If it had been {ro da poi [de zo'u:]  da klama de}, fair enough,
> > but it appears from this that {ro klama be de} refers to all goers to one
> > specific place, since {de} is quantified *outside* the description, in
> > whatever bridi it occupies.

> Yes, it is.  However, "ro klama" means "ro lo klama", which can be transformed
> WLG into "ro DA poi klama", where DA is an otherwise-unique member of the
> da-series.  The quantification of this "DA" precedes that of "de", so the
> fully explicit prenex-normal-form is:

>         ro DA [su'o] DE zo'u co'e DA poi klama de

> where the "co'e" represents the whole selbri in which this description is
> embedded.  Every quantified expression in Lojban can be transformed into
> a form in which the quantifier is attached to a variable.  Therefore,
> even though "de" is quantified outside the description, so is the implicit
> "ro DA", and the "ro DA" is outside the "de".

I'm not sure how this works, given that {DA} is restricted (by the {poi}
clause) *after* the prenex.  Doesn't this select a subset of the {DA}
introduced by the prenex?  Or does the restriction apply throughout?
My instinct is that you need to be able to subselect, but I can't quite
wrap my brain round a selection which depends on the value of {de}, which
was quantified after {DA}, and hence potentially depends on {DA} - a sort of
mutual recursion.  (I suspect that this is a mirage, but it's still confusing.)

    For any given {DA}, we can choose a {de}, such that some predicate
    holds for those {DA}s which {klama de}.

.oiro'e

I've already given the expansion I was originally assuming, with {de}
quantified inside the (virtual) restriction, and this looks to me like
a different claim.

mu'o mi'e .i,n.