On W= ed, Dec 26, 2012 at 10:53 AM, Felipe Gon=E7alves Assis &l= t;felipeg.assi= s@gmail.com> wrote:

coi latro'a

Your confusion is well-founded. I'll introduce an example without
analysis to make
the discussion accessible to non-mathematicians. Then I'll get to your = point.

Let's prove "Everyone has an uncle" from "Everyone has a= mother" and
"Everyone has a brother".

(1) Everyone has a mother.
(2) Bob has a mother.
(3) Let Mary be a mother of Bob.
(4) Everyone has a brother.
(5) Mary has a brother.
(6) Let Sam be a brother of Mary.
(7) Sam is a brother of a mother of Bob.
(8) Sam is an uncle of Bob.
(9) Bob has an uncle.
(10) Everyone has an uncle.

This is a sequence of valid inferences:
(1) and (4) are hypotheses;
(2) and (5) are Universal Instantiations;
(3) and (6) are Existential Instantiations;
(7) and (9) are Existential Generalizations;
(10) is Universal Generalization;
(8) is definition.

In prose:
"Let Bob be an arbitrary folk. By hypothesis, Bob has a mother. Let Ma= ry be
a mother of Bob. Again, by hypothesis, Mary has a brother. Let's call h= im Sam.
Well, Sam is the brother of Mary, and Mary is the mother of Bob, therefore,= by
definition, Sam is an uncle of Bob. We have concluded that Bob has an uncle= .
Since Bob was arbitrary, everyone has an uncle."

Now to your point: Let's see how a mathematician could write that argum= ent
using logical formulae:
"We wish to prove
=A0 (for all Bob)(there exists z) UNCLE(z, Bob).

We have
=A0 (for all x1)(there exists Mary) MOTHER(Mary, x1);
=A0 (for all x2)(there exists Sam) BROTHER(Sam, x2).

Setting x1=3DBob, we obtain Mary such that MOTHER(Mary, Bob).
Setting x2=3DMary, we obtain Sam such that BROTHER(Sam, Mary).
Now set z=3DSam to get
=A0 BROTHER(z, Mary) and MOTHER(Mary, Bob)
from where, by definition,
=A0 UNCLE(z, Bob)
as desired."

What happens is
=A01. Universal Generalization and Existential Instantiation are
anticipated in the
bound variable names of the thesis and hypotheses, respectively, and done implicitly.
=A02. Universal Instantiation and Existential Generalization are done with = a "set
x=3Dy" wording.

Of these, what appears to trouble you is the implicit Existential Instantia= tion.
The reuse of the bound variable as the witness object is not how
formal inference
rules typically work. The free Mary in "MOTHER(Mary, Bob)" is
something different
from the bound Mary in "(for all x1)(there exists Mary) MOTHER(Mary, x1)". It would
be equally logical to say, e.g.,
=A0 "Setting x1=3DBob, we obtain Eve such that MOTHER(Eve, Bob)" = .

This "set x1=3DBob and obtain a Mary" thing only works because Ma= thematicians
use a peculiar set of inference rules, which involves naming bound variable= s
differently across sentences in hypothesis and thesis and "using"= each formula
only once.

Regarding Lojban, instead of trying to translate something like
=A0"There exists Bob such that Bob is blue, therefore we obtain a blue= Bob."
Try translating
=A0 "There exists x such that x is blue. Let Bob be a blue thing."= ;

My initial suggestion is
=A0 {da blanu .i[seji'ubo] la .bab. ca'e go'i}

A dual question is how to translate Universal Generalization:
=A0 "Let Bob be arbitrary. [...] Bob is blue, therefore everything is = blue."

I suggest
=A0 {la .bab. ca'e [...] .i la .bab. blanu .i ja'o ro da go'i}<= br>
a'o mi sidju do
mu'o mi'e .asiz.

On 24 December 2012 20:53, Ian Johnson <blindbravado@gmail.com> wrote:
> This is rather subtle, so I think it's best to begin with an examp= le. This
> example isn't all that mathematically heavy, but it does involve t= he
> interaction of several sentences which each have a "forall exists= forall"
> quantifier structure. This does have something to do with Lojban, but = it
> will be a while before that is actually clear. You've been warned = :)
>
> Suppose g : R->R is uniformly continuous and f : R -> R is integ= rable on
> [a,b]. Define the new function
> (f * g)(x) =3D integral from a to b of g(x-z) f(z) dz
> We want to show that the function f * g is continuous at every point, = that
> is:
> (for all x in R,e1 > 0)(there exists d1 > 0)(for all y in R) |x-= y| < d1 ->
> |(f * g)(x) - (f * g)(y)| < e1.
>
> (I write quantifiers in almost-prenex-normal form; my apologies if it = is
> hard to read.)
>
> Let e1 > 0.
> Using the uniform continuity of g we have
> (for all e2 > 0)(exists d2 > 0)(for all x,y in R) |x-y| < d2 = -> |g(x) -
> g(y)| < e2.
>
> So let e2 > 0, obtain the desired d2 > 0, and take x,y with |x-y= | < d2.
> Then:
>
> | (f * g)(x) - (f * g)(y) | =3D | integral from a to b of f(z) (g(x-z)= -
> g(y-z)) dz |
> <=3D integral from a to b of |f(z) (g(x-z) - g(y-z))| dz
> =3D integral from a to b of |f(z)| |g(x-z) - g(y-z)| dz
> < integral from a to b of |f(z)| e2 dz
> =3D Me2
> where M =3D integral from a to b of |f(z)| exists and is finite by ass= umption.
>
> (Now comes the weird part.)
>
> Setting e2 =3D e1/M, obtain d2 using the continuity of g, then set d1= =3Dd2. Then
> if |x-y| < d1, from the above |(f * g)(x) - (f * g)(y)| < M e1/M= =3D e1 as
> desired. Thus f*g is continuous at every point.
>
> What is weird here is that we're playing with e2 and d2 as if they= 're real.
> e1 and d1 are interacted with as the quantifier structure suggests: yo= u
> introduce e1, do some work, and find a valid value of d1. But e2 is no= w
> instantiated (in this case in a trivial way, thankfully) under the e1<= br> > quantifier, and then d2 is instantiated under the e2 quantifier, follo= wed by
> folding back up to obtain the original statement. None of this instant= iation
> is "real", it's all syntactic, but we operate better whe= n objects appear to
> be concrete. This is all ultimately valid reasoning, and indeed can be=
> compressed so that everything is in normal form, but syntactically it&= #39;s very
> strange, because it's analogous to {da goi ko'a}, which as I t= hink most of
> us know doesn't actually make any sense.
>
> I was originally curious about this because I don't know how I wou= ld render
> proofs like this in Lojban; I would be forced, in order to "set d= 1=3Dd2" and
> such, to bind d2, which is bound under a quantifier, to a variable, wh= ich
> doesn't actually make logical sense.
>
> Any thoughts?
>
> mu'o mi'e la latro'a
>

> --
> You received this message because you are subscribed to the Google Gro= ups
> "lojban" group.
> To post to this group, send email to lojban@googlegroups.com.
> To unsubscribe from this group, send email to
> lojban+unsubs= cribe@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/lojban?hl=3Den.

--
You received this message because you are subscribed to the Google Groups &= quot;lojban" group.
To post to this group, send email to lojban@googlegroups.com.
To unsubscribe from this group, send email to lojban+unsubscribe@googlegroups.com.
For more options, visit this group at http://groups.google.com/group/lojba= n?hl=3Den.