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>:
> 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} .
>
> Thank you for the question. Here is my answer. I will add this topic to the
> commentary.
>
> 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}.
> (I omit x2 of {mlatu} for simplicity.)
>
> Unless all cats in this universe of discourse were born to common parents
> at the same time at the same place, these {zo'e} are not constants but
> Skolem functions f(x) g(x) h(x) respectively:
>
> 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)),
> where x corresponds to {da}, and is a singular variable bound by a
> universal quantifier A,
> ~ is negation,
> v is OR,
> M and J are predicates.
>
> 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}.
Martin
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.
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.
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."