* Monday, 2014-05-26 at 08:01 -0700 - guskant <gusni.kantu@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
> In Skolemizing S4 into S3, {su'oidexipa}, {su'oidexire} and {su'oidexici}
> of S4 are replaced by {zo'e}s that are respectively equal to f(x), g(x) and
> h(x). If {zo'e} were not Skolem functions, we should have abandoned the
> interpretation "S1 = S2" so that the omitted sumti could have been bound
> variables. (It would not be the case if we accepted the idea in "Section
> 4.3.1. If zo'e could be a bound plural variable" of my commentary, but it
> is another story.)
>
> If we want to make explicit that a Skolem function {zo'e} is a Skolem
> plural constant (that is, the referent of {zo'e} does not vary according to
> {da}), we should say the corresponding plural variable earlier than {roda}
> in the prenex of the statement before Skolemization.
> For example, in order to mean that {zo'e} at x4 of {jbena} refers to the
> Earth that is common to all cats, the statement before Skolemization should
> be
>
> S5- {su'oidexici roda su'oidexipa su'oidexire zo'u
> ganai da mlatu gi da jbena dexipa dexire dexici},
> that is
> EY3 Ax EY1 EY2 ~M(x) v J(x,Y1,Y2,Y3).
>
> By skolemizing S5, we obtain a statement that is
> S6.1- Ax ~M(x) v J(x,f(x),g(x),h),
> where h is a Skolem plural constant: h does not depend on x because EY3 of
> S5 was said earlier than Ax in the prenex.
>
> Lojban expression of S6.1 might not officially be explained, but I would
> profit the property that Lojban prenex can include constants:
>
> S6- {cy zo'u ro mlatu cu jbena fo cy},
> which is the same as
> {cy roda poi mlatu zo'u da jbena fo cy}
> and
> {cy roda zo'u ganai da mlatu gi da jbena fo cy}.
>
> In S6, I used {cy} instead of {zo'e} for the constant, otherwise we could
> not distinguish which {zo'e} was on the prenex.
>
>
> Although it might be off-topic, the following thread on the order of tagged
> sumti and its scope suggests me of an idea:
> https://groups.google.com/d/topic/lojban/PhZD1fO64jc/discussion
>
> I suggest that not only the scope of tagged sumti but also that of terbri
> sumti reflects their order. For example, I suggest considering that S6.1
> and S6 are the same as
>
> S7- {fo cy fa ro mlatu cu jbena}.
Attachment:
signature.asc
Description: Digital signature