[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: TECH: Quantifiers (was: cukta)
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.