On Mon, Dec 24, 2012 at 6:53 PM, Ian Johnso= n <blindbravado@gmail.com> wrote:

This is rather subtle, so I think it's best to begin with an example. T= his example isn't all that mathematically heavy, but it does inv= olve the interaction of several sentences which each have a "forall ex= ists forall" quantifier structure. This does have something to = do with Lojban, but it will be a while before that is actually clear. You&#= 39;ve been warned :)

Suppose g : R->R is uniformly continuous and f : R -> R is integr= able 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 continuo= us at every point, that is:
(for all x in R,e1 > 0)(there exists d1 > 0)(for all y in R) |x-y| &l= t; 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
< integ= ral 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 assumption.

(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 desire= d. Thus f*g is continuous at every point.

What is weird here is that we're playing with e2 and d2 as if they&= #39;re real. e1 and d1 are interacted with as the quantifier structure sugg= ests: you introduce e1, do some work, and find a valid value of d1. But e2 = is now instantiated (in this case in a trivial way, thankfully) unde= r the e1 quantifier, and then d2 is instantiated under the e2 quantifier, f= ollowed by folding back up to obtain the original statement. None of this i= nstantiation is "real", it's all syntactic, but we operate be= tter when objects appear to be concrete. This is all ultimately valid reaso= ning, and indeed can be compressed so that everything is in normal form, bu= t syntactically it's very strange, because it's analogous to {da go= i ko'a}, which as I think most of us know doesn't actually make any= sense.

I was originally curious about this because I don't know how I woul= d render proofs like this in Lojban; I would be forced, in order to "s= et d1=3Dd2" and such, to bind d2, which is bound under a quantifier, t= o a variable, which doesn't actually make logical sense.

Any thoughts?

mu'o mi'e la latro'a