Le mercredi 28 mai 2014 05:42:53 UTC+9, Martin Bays a écrit :
* Monday, 2014-05-26 at 23:12 -0700 - guskant <gusni...@gmail.com>:
> Le mardi 27 mai 2014 11:53:50 UTC+9, Martin Bays a écrit :
> > * Monday, 2014-05-26 at 08:01 -0700 - guskant <gusni...@gmail.com<_javascript_:>>:
> > > Le lundi 26 mai 2014 04:49:09 UTC+9, Martin Bays a écrit :
> > > > * Monday, 2014-05-19 at 06:04 -0700 - guskant <gusni...@gmail.com<_javascript_:>>:
> > > > > Le mardi 8 avril 2014 10:09:19 UTC+9, guskant a écrit :
> > > >
> > http://www.lojban.org/tiki/gadri%3A+an+unofficial+commentary+from+a+logical+point+of+view&no_bl=y
> > > >
> > > > Saying that {zo'e} and {lo broda} introduce "constants" isn't really
> > > > enough to explain how they work, because of cases where a description
> > > > includes a bound variable, e.g.
> > > > {ro da poi verba cu prami lo rirni be da} .
> > > Generally, all {zo'e} in a statement that contains one or more bound
> > > variable(s), no matter if they are explicit or not, must be Skolem
> > > functions. If they were not, the official interpretation (CLL 7.7) of
> > > implicit {zo'e} should have been modified.
> > >
> > > For example, we may freely say:
> > >
> > > S1- {ro mlatu cu jbena}.
> > >
> > > According to CLL 7.7, it has the same meaning as
> > >
> > > S2- {ro mlatu cu jbena zo'e zo'e zo'e}.
> > >
> > > S3- {roda zo'u ganai da mlatu gi da jbena zo'e zo'e zo'e},
> > > that is
> > > Ax ~M(x) v J(x,f(x),g(x),h(x)),
> > >
> > > S3 is a Skolemized form of a statement
> > >
> > > S4- {roda su'oidexipa su'oidexire su'oidexici zo'u
> > > ganai da mlatu gi da jbena dexipa dexire dexici},
> > > that is
> > > Ax EY1 EY2 EY3 ~M(x) v J(x,Y1,Y2,Y3),
> > > where Y1 Y2 Y3 are plural variables bound by existential quantifiers E.
> >
> > I don't know of any clear problem with this solution - which, when
> > applied to {lo}, corresponds to CLL-{lo} (modulo the difference between
> > su'o and su'oi). But as I understand it, xorlo solves the problem rather
> > differently - by having the {zo'e}s there refer to generics, constant
> > with respect to {da}.
>
> The interpretation of {zo'e} as Skolem function rather reinforces xorlo,
> and makes clear that the CLL-interpretation of gadri is problematic.
>
> Skolem functions f(x),g(x),h(x) of S3 are constants for every referent in
> the domain of Ax, because they depend on no variable except x. It does not
> contradict xorlo. On the other hand, any sumti of CLL-lo are bound by any
> singular quantifier, and cannot express Skolemized form.
Although I don't actually consider myself qualified to pronounce on what
xorlo is, my understanding is that the intention and common
understanding of xorlo have {lo} and {zo'e} constant in the sense of
being outside the scope of any quantifier, except when absolutely forced
to be inside. So e.g. in {ro da broda lo brode}, the (plural) referent
of {lo brode} is constant with respect to {da} under xorlo, whereas it
is not in CLL-lojban.
Regarding {zo'e} as the outmost constant in a prenex of a statement is a special case of {zo'e} as Skolem functions. As for the example
{ro da broda lo brode},
that is
Ax B(x,f(x)),
it says nothing about whether {lo brode} as a Skolem function f(x) is constant for all x or not. That is to say, xorlo allows both interpretations "EYAx B(x,Y)" and "AxEY B(x,Y)" as a statement before Skolemization, while CLL-lo restricts the interpretation to "AxEy B(x,y)" (small y is a singular variable). If xorlo did not allow this interpretation, CLL 7.7 must have been abandoned. As long as both xorlo and CLL 7.7 are kept true, a constant {zo'e} is not always out of bound variables.
> If a statement includes no universal quantifier after transformed into
> prenex normal form, the statement can be Skolemized into a statement in
> which all Skolem functions are Skolem constants. xorlo can precisely
> express these constants. CLL-lo cannot.
>
> xorlo can make explicit the difference of meaning between S3 and S6.1 for
> any sumti in a simple way like S6. CLL-lo restricts the outer quantifier
> according to sumti, and makes it difficult to express the difference of
> meaning between S3 and S6.1.
> > > S6- {cy zo'u ro mlatu cu jbena fo cy},
> > > S6.1- Ax ~M(x) v J(x,f(x),g(x),h),
You're right, the semantics you're suggesting aren't really CLL-lo. But
they share the scope-sensitivity of CLL-lo; that's all I really meant.
CLL-lo cannot express S3 precisely for the same reason above. S3 of xorlo says nothing about whether the Skolem functions f(x),g(x),h(x) are Skolem constants or not. In other words, S3 of xorlo does not say the order of bound variables of a statement before Skolemization. Regarding it as S4 is the most general case. Any of the statements with prenex "EY2 Ax EY1 EY3" "EY1 EY2 Ax EY3" etc may be Skolemized into S3, because a Skolen function {zo'e} does not indicate whether it is a Skolem constant or not.
On the other hand, according to CLL-lo, speaker must always select the order of Ax, EY1, EY2 and EY3 of a statement before Skolemization.
> As for the example in my commentary that you pointed out:
>
> {su'o da zo'u loi re lo'i ro mokca noi sepli py noi mokca ku'o da cu
> relcuktai},
>
> the quantifier in the prenex is not universal A but existential E: it is
> not a Skolemized form.
> It is expressed in predicate logic as
>
> Ex R(m,p,x),
> where x is a singular variable bound by an existential quantifier E,
> R is a predicate,
> m and p are constants.
>
> Because this statement contains no other outer quantifier, it is a prenex
> normal form that contains no universal quantifier. It is therefore
> Skolemized into
>
> {loi re lo'i ro mokca noi sepli py noi mokca ku'o zo'e cu relcuktai},
> that is
> R(m,p,z),
> where z is a Skolem constant.
>
> There is no problem for interpreting it as "two sets of points that are
> equidistant from a point P is a double circle."
But you seem to have jumped the existential through the {re} quantifier.
The radii are meant to be allowed to be different for the two circles,
but in the original sentence the radii are quantified with outermost
scope.
I was also confused because the english reads like a definition, whereas
the lojban has no hint of that (and I'm not sure that adding a {ca'e}
would do it).
Martin
{re} in this example is an inner quantifier, and it does not affect the order of outer quantifier.
{zo'e} in the statement {loi re lo'i ro mokca noi sepli py noi mokca ku'o zo'e cu relcuktai} is a plural constant. Precisely saying, this {zo'e} is {lo re zo'e} in this context. This statement does not make clear if each individual of the referent of {zo'e} distributively satisfies {sepli}, but such an interpretation is allowed. I used rather a bound singular variable {su'oda} in the original example because I wanted to make explicit that the radii distributively satisfy {sepli}. When I created the example, I did not consider Skolem functions, but if I wanted to make scopes of the arguments explicit, I should have been said
{py lu'a loi re lo'i ro mokca su'o da lo'i ro mokca zo'u loi re lo'i ro mokca noi sepli py noi mokca ku'o da cu relcuktai},
where I added {lu'a} in order to draw each of {lo se gunma} in the loi-sumti. This trick allows inner quantification to behave as if outer quantification in the prenex.
However, I don't think such a precision by prenex is not necessary for an example of repeating inner quantification.
As a summary, xorlo can express the scopes of arguments without outer quantifier unambiguously as well as ambiguously, while CLL-lo must always do unambiguously.
If we take the interpretation like S7, the scopes of the outmost terbri sumti of a statement become unambiguous also in xorlo, though I think this idea should be at most a plausible interpretation, not a restriction. In general, there are many cases where the order of arguments out of prenex is restricted by grammar, like that example of relcuktai. xorlo allows Lojban users to select the most likely interpretation among some possible ones, while CLL-lo definitely requires prenex even for such a simple example. The idea of xorlo made the language closer to natural expressions, while it reserves also the unambiguity of logic in expressions with prenex.