Re: [lojban] Some weirdness in how mathematicians work with quantifiers

[Ian Johnson <blindbravado@gmail.com>]

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 <me@v4hn.de> 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.