Received: from mail-qc0-f190.google.com ([209.85.216.190]:35528) by stodi.digitalkingdom.org with esmtps (TLSv1:RC4-SHA:128) (Exim 4.76) (envelope-from ) id 1TnrBK-0000s2-1n; Wed, 26 Dec 2012 05:38:18 -0800 Received: by mail-qc0-f190.google.com with SMTP id d10sf4881297qca.7 for ; Wed, 26 Dec 2012 05:37:55 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20120806; h=x-received:x-beenthere:x-received:x-received:received-spf :mime-version:in-reply-to:references:date:message-id:subject:from:to :x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:x-google-group-id:list-post :list-help:list-archive:sender:list-subscribe:list-unsubscribe :content-type; bh=SaLrHDHU0HerixkEAlSk1kjgrBwCKnj0ysCdAdG2pOY=; b=ny4ZJN2qoa1BXFCfUsAfa/e+C7dSZkwrYcQS2KjDsvaG4Njn5O1Z1onTV+951VbTVH q3TSJZaExmj+ZwT9sLlf2tHaQGmFSKmchWApqXC9vPjD+Lzxw+p287ovHBy4MqcEH6UM RnexoUmhU20H3HV+t2/7rVDzb9CYnbGlKO6akxDj8sgqnA/4RuJf3wRbBIKAjQIAHfzq AUHyJ8EmQH7yJkKhBWmSnQuDrksjzYPuwyN/U1uIiBto7pDaCAOdfYANn2FT+M9Uk/6C AtunJZFxA0gZWsXNE2AI1Nmol4JP6QdnJFbQxw5OG1G6NM9F5m1gtu0gX5xrC4+Z9N0L BR2w== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-received:x-beenthere:x-received:x-received:received-spf :mime-version:in-reply-to:references:date:message-id:subject:from:to :x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:x-google-group-id:list-post :list-help:list-archive:sender:list-subscribe:list-unsubscribe :content-type; bh=SaLrHDHU0HerixkEAlSk1kjgrBwCKnj0ysCdAdG2pOY=; b=KaHeCno1y10MDue6FxOGHBAXP6etUEfL2McEA2uRJlT1+U6GEWMQytVDbGSetzG1+i mcZIXczty8F0s/ZEQX6AZXraffNCRS9QN+XZy9cy47LrAtazSKLYhntUFLClTrThqgCS eRNG6ocCXQ8rVJJYPjKfrRIhLjZXfWuRseKAV8Se7/Zoamt++Euv66K0E7qJfPNNMNMW feRysP1g7lGpOjq9myw6CNtxVXXZfYSr3RxO7n29AUazKqj+0OgITuGlAkxE/e4WT21i KYMpcOTXH3ogzb5vf+5Df223hZsNJa7SLC7WhjITQRm4q7vQ3rCKjYzg4w3YUVuArUfe MauA== X-Received: by 10.49.87.1 with SMTP id t1mr3809523qez.41.1356529075300; Wed, 26 Dec 2012 05:37:55 -0800 (PST) X-BeenThere: lojban@googlegroups.com Received: by 10.49.1.5 with SMTP id 5ls3695863qei.18.gmail; Wed, 26 Dec 2012 05:37:53 -0800 (PST) X-Received: by 10.52.71.109 with SMTP id t13mr4495524vdu.2.1356529073891; Wed, 26 Dec 2012 05:37:53 -0800 (PST) X-Received: by 10.52.71.109 with SMTP id t13mr4495523vdu.2.1356529073870; Wed, 26 Dec 2012 05:37:53 -0800 (PST) Received: from mail-vb0-f43.google.com (mail-vb0-f43.google.com [209.85.212.43]) by gmr-mx.google.com with ESMTPS id h20si8168731vdg.3.2012.12.26.05.37.53 (version=TLSv1/SSLv3 cipher=OTHER); Wed, 26 Dec 2012 05:37:53 -0800 (PST) Received-SPF: pass (google.com: domain of blindbravado@gmail.com designates 209.85.212.43 as permitted sender) client-ip=209.85.212.43; Received: by mail-vb0-f43.google.com with SMTP id fs19so8927859vbb.30 for ; Wed, 26 Dec 2012 05:37:53 -0800 (PST) MIME-Version: 1.0 Received: by 10.52.22.107 with SMTP id c11mr36627576vdf.73.1356529073755; Wed, 26 Dec 2012 05:37:53 -0800 (PST) Received: by 10.220.13.197 with HTTP; Wed, 26 Dec 2012 05:37:53 -0800 (PST) In-Reply-To: <20121226103259.GD7855@samsa.fritz.box> References: <20121226103259.GD7855@samsa.fritz.box> Date: Wed, 26 Dec 2012 08:37:53 -0500 Message-ID: Subject: Re: [lojban] Some weirdness in how mathematicians work with quantifiers From: Ian Johnson To: lojban@googlegroups.com X-Original-Sender: blindbravado@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of blindbravado@gmail.com designates 209.85.212.43 as permitted sender) smtp.mail=blindbravado@gmail.com; dkim=pass header.i=@gmail.com Reply-To: lojban@googlegroups.com Precedence: list Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com List-ID: X-Google-Group-Id: 1004133512417 List-Post: , List-Help: , List-Archive: Sender: lojban@googlegroups.com List-Subscribe: , List-Unsubscribe: , Content-Type: multipart/alternative; boundary=20cf307c9eaa91967004d1c18902 X-Spam-Score: -0.1 (/) X-Spam_score: -0.1 X-Spam_score_int: 0 X-Spam_bar: / --20cf307c9eaa91967004d1c18902 Content-Type: text/plain; charset=ISO-8859-1 The weirdness in the original post is that we don't know how exactly we're going to relate e1 and d1 to e2 and d2 in advance. In this case the relationship turns out to be basically trivial; in complicated cases it can be much less trivial. In either case, the way the analysis actually happens, you wind up introducing e1 and d1, introducing e2 and d2, and then doing some work to see what the latter have to do with the former. You can go back afterward and introduce e1 and d1, define e2 and d2 relative to them immediately (knowing how they will be related), and then obtain the desired result, but that's not the way the reasoning happens the first time, and there should be a "logical" way of showing the initial reasoning. You point out the ability to Skolemize the statement P. I'm familiar with this, and am pretty fond of it as well, but in practice (at least in analysis) this style is quite atypical. Indeed, even the style of subscripting quantified variables as I did here is pretty unusual; typically people just don't write out their quantified statements, and just "use the continuity of g to get delta ... such that ... < epsilon/3" or such things. I think the Skolemized style may be the better choice for adapting this idea into Lojban style (or indeed for eventually writing mathematics in Lojban). (Also, you needed a ku or a cu after kei :)) On Wed, Dec 26, 2012 at 5:33 AM, v4hn wrote: > On Mon, Dec 24, 2012 at 06:53:34PM -0500, Ian Johnson wrote: > > Suppose g : R->R is uniformly continuous and f : R -> R is integrable on > > [a,b]. Define the new function > > (f * g)(x) = integral from a to b of g(x-z) f(z) dz > > .uesai lonu tavla fi la'o gy. convolution .gy vecu'u le mriste kei spaji mi > .i le do mupli ku pluja sei mi jinvi fi loi purci nu casnu > > > 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. > > I'll call this P. > > > So let e2 > 0, obtain the desired d2 > 0, and take x,y with |x-y| < d2. > > Then: > > > > | (f * g)(x) - (f * g)(y) | = | integral from a to b of f(z) (g(x-z) - > g(y-z)) dz | > > <= integral from a to b of |f(z) (g(x-z) - g(y-z))| dz > > = 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 > > = Me2 > > where M = integral from a to b of |f(z)| exists and is finite by > assumption. > > > > (Now comes the weird part.) > > > > Setting e2 = e1/M, obtain d2 using the continuity of g, then set d1=d2. > > You use P as a method of obtaining d2 here. If you'd skolemize P before, > you don't need > to introduce an additional variable(d2). Also e2 is simply e1/M, so if you > think > e1 is "real" (whatever you mean by that), then how is it different from > e1/M? > > P could be written as (Given a function d: R->R, which replaces the > existential quantifier): > > (forall e2 > 0)(forall x,y in R) [|x-y| < d(e2) -> |g(x) - g(y)| < e2] > > So now you are just applying universal instantiation to derive > > (forall x,y in R) [|x-y| < d(e1/M) -> |g(x) - g(y)| < e1/M] > > which you need for your above derivation. The rest should work out fine, > replacing your d2 with d(e1/M) and e2 with e1/M. > > > What is weird here is that we're playing with e2 and d2 as if they're > real. > > As I said, they are as "real" as everything else (though you might want > to consider viewing d2 as a function instead of an existentially bound > variable) > > > Any thoughts? > > di'u selpensi mi > > > mi'e la .van. mu'o > -- You received this message because you are subscribed to the Google Groups "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/lojban?hl=en. --20cf307c9eaa91967004d1c18902 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable The weirdness in the original post is that we don't know how exactly we= 're going to relate e1 and d1 to e2 and d2 in advance. In this case the= relationship turns out to be basically trivial; in complicated cases it ca= n be much less trivial. In either case, the way the analysis actually happe= ns, you wind up introducing e1 and d1, introducing e2 and d2, and then doin= g some work to see what the latter have to do with the former. You can go b= ack afterward and introduce e1 and d1, define e2 and d2 relative to them im= mediately (knowing how they will be related), and then obtain the desired r= esult, but that's not the way the reasoning happens the first time, and= there should be a "logical" way of showing the initial reasoning= .

You point out the ability to Skolemize the statement P. I'm familia= r with this, and am pretty fond of it as well, but in practice (at least in= analysis) this style is quite atypical. Indeed, even the style of subscrip= ting quantified variables as I did here is pretty unusual; typically people= just don't write out their quantified statements, and just "use t= he continuity of g to get delta ... such that ... < epsilon/3" or s= uch things. I think the Skolemized style may be the better choice for adapt= ing this idea into Lojban style (or indeed for eventually writing mathemati= cs in Lojban).

(Also, you needed a ku or a cu after kei :))

On Wed, Dec 26, 2012 at 5:33 AM, v4hn <me@v4hn.de> wrote:

On Mon, Dec 24, 2012 at 06:53:34PM -0500, Ian Johnson wro= te:
> 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

.uesai lonu tavla fi la'o gy. convolution .gy vecu'u le mrist= e kei spaji mi
.i le do mupli ku pluja sei mi jinvi fi loi purci nu casnu

> 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.

I'll call this P.

> 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.

You use P as a method of obtaining d2 here. If you'd skolemize P = before, you don't need
to introduce an additional variable(d2). Also e2 is simply e1/M, so if you = think
e1 is "real" (whatever you mean by that), then how is it differen= t from e1/M?

P could be written as (Given a function d: R->R, which replaces the exis= tential quantifier):

(forall e2 > 0)(forall x,y in R) [|x-y| < d(e2) -> |g(x) - g(y)| &= lt; e2]

So now you are just applying universal instantiation to derive

(forall x,y in R) [|x-y| < d(e1/M) -> |g(x) - g(y)| < e1/M]

which you need for your above derivation. The rest should work out fine, replacing your d2 with d(e1/M) and e2 with e1/M.

> What is weird here is that we're playing with e2 and d2 as if they= 're real.

As I said, they are as "real" as everything else (though yo= u might want
to consider viewing d2 as a function instead of an existentially bound vari= able)

> Any thoughts?

di'u selpensi mi

mi'e la .van. mu'o

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