Received: from mail-we0-f187.google.com ([74.125.82.187]:41201)
	by stodi.digitalkingdom.org with esmtps (TLSv1:RC4-SHA:128)
	(Exim 4.76)
	(envelope-from <lojban+bncBDUNF3UDXIJBBXVE5ODAKGQE5LSWP4A@googlegroups.com>)
	id 1TnoIR-0008O9-8C; Wed, 26 Dec 2012 02:33:26 -0800
Received: by mail-we0-f187.google.com with SMTP id r3sf3323929wey.24
        for <multiple recipients>; Wed, 26 Dec 2012 02:33:03 -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:date:from
         :to:subject:message-id:references:mime-version:content-type
         :content-disposition:in-reply-to:user-agent: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;
        bh=hyZNrwoca+RbjgipPzR2FI8DkU/dVwpizfLdVbHFgUg=;
        b=rI8C0hQbCl3uMJz4dYDQtmSbQG1rb0XoMfLXEBZ9NWiXLiDWHzoFEgfkXpWXKFRKFM
         757W6k1ahH5q4lnqMXYz4cUs3PsYVQ9PTYkctpEA+7FStxYfdzwuNSJfQmpeKYQROGqB
         w3siwCYFr+eAVTdgzT1tBOcL7A7epVaenukHuO6o036c1aTxsHetLOFd7DpwDIkRcd1S
         QFevdtdntTp9iiFMUH5IE7Sh54U+CezAQC16iZo8LDqEt6h707qP6iTSJbDYnGroUuAn
         zxTWtkbRAxMQO8i2fUxOcK0ICPcryexAB9SkDrJlqu+E9jMF+EYNjkCgMkLNm/JctSQe
         eeGA==
X-Received: by 10.180.84.200 with SMTP id b8mr3090901wiz.19.1356517983398;
        Wed, 26 Dec 2012 02:33:03 -0800 (PST)
X-BeenThere: lojban@googlegroups.com
Received: by 10.180.94.101 with SMTP id db5ls3109819wib.35.gmail; Wed, 26 Dec
 2012 02:33:02 -0800 (PST)
X-Received: by 10.14.214.197 with SMTP id c45mr34353245eep.7.1356517982311;
        Wed, 26 Dec 2012 02:33:02 -0800 (PST)
X-Received: by 10.14.214.197 with SMTP id c45mr34353244eep.7.1356517982295;
        Wed, 26 Dec 2012 02:33:02 -0800 (PST)
Received: from dd17822.kasserver.com (dd17822.kasserver.com. [85.13.138.119])
        by gmr-mx.google.com with ESMTPS id z44si9726016een.0.2012.12.26.02.33.02
        (version=TLSv1/SSLv3 cipher=OTHER);
        Wed, 26 Dec 2012 02:33:02 -0800 (PST)
Received-SPF: neutral (google.com: 85.13.138.119 is neither permitted nor denied by best guess record for domain of me@v4hn.de) client-ip=85.13.138.119;
Received: from samsa (brln-4dbc2cdc.pool.mediaWays.net [77.188.44.220])
	by dd17822.kasserver.com (Postfix) with ESMTPA id D33D9860387
	for <lojban@googlegroups.com>; Wed, 26 Dec 2012 11:33:00 +0100 (CET)
Date: Wed, 26 Dec 2012 11:33:00 +0100
From: v4hn <me@v4hn.de>
To: lojban@googlegroups.com
Subject: Re: [lojban] Some weirdness in how mathematicians work with quantifiers
Message-ID: <20121226103259.GD7855@samsa.fritz.box>
References: <CA+gZtgL4eA1WnuSmJP-=S8ZmsDpbTkrmmj1uKMGrCT=HwotnRA@mail.gmail.com>
MIME-Version: 1.0
Content-Type: multipart/signed; micalg=pgp-sha1;
	protocol="application/pgp-signature"; boundary="fXStkuK2IQBfcDe+"
Content-Disposition: inline
In-Reply-To: <CA+gZtgL4eA1WnuSmJP-=S8ZmsDpbTkrmmj1uKMGrCT=HwotnRA@mail.gmail.com>
User-Agent: Mutt/1.5.21 (2010-09-15)
X-Original-Sender: me@v4hn.de
X-Original-Authentication-Results: gmr-mx.google.com; spf=neutral (google.com:
 85.13.138.119 is neither permitted nor denied by best guess record for domain
 of me@v4hn.de) smtp.mail=me@v4hn.de
Reply-To: lojban@googlegroups.com
Precedence: list
Mailing-list: list lojban@googlegroups.com; contact lojban+owners@googlegroups.com
List-ID: <lojban.googlegroups.com>
X-Google-Group-Id: 1004133512417
List-Post: <http://groups.google.com/group/lojban/post?hl=en_US>, <mailto:lojban@googlegroups.com>
List-Help: <http://groups.google.com/support/?hl=en_US>, <mailto:lojban+help@googlegroups.com>
List-Archive: <http://groups.google.com/group/lojban?hl=en_US>
Sender: lojban@googlegroups.com
List-Subscribe: <http://groups.google.com/group/lojban/subscribe?hl=en_US>, <mailto:lojban+subscribe@googlegroups.com>
List-Unsubscribe: <http://groups.google.com/group/lojban/subscribe?hl=en_US>, <mailto:googlegroups-manage+1004133512417+unsubscribe@googlegroups.com>
X-Spam-Score: -0.0 (/)
X-Spam_score: -0.0
X-Spam_score_int: 0
X-Spam_bar: /


--fXStkuK2IQBfcDe+
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: quoted-printable

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) =3D integral from a to b of g(x-z) f(z) dz

=2Euesai lonu tavla fi la'o gy. convolution .gy vecu'u le mriste kei spaji =
mi
=2Ei 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, tha=
t 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.)
>=20
> 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:
>=20
> | (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 assump=
tion.
>=20
> (Now comes the weird part.)
>=20
> Setting e2 =3D e1/M, obtain d2 using the continuity of g, then set d1=3Dd=
2.

You use P as a method of obtaining d2 here. If you'd skolemize P before, yo=
u 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 existen=
tial 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 rea=
l.

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 vari=
able)

> Any thoughts?

di'u selpensi mi


mi'e la .van. mu'o

--fXStkuK2IQBfcDe+
Content-Type: application/pgp-signature

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.12 (GNU/Linux)

iEYEARECAAYFAlDa0lsACgkQMBKLZs4+wjxIRQCfR5ShfdM6R7Cd45BCfL6nPze9
C0wAn1CYPOAoodSZP6oRsX/oO8CA+L/c
=060S
-----END PGP SIGNATURE-----

--fXStkuK2IQBfcDe+--