Received: from mail-gh0-f186.google.com ([209.85.160.186]:35359) by stodi.digitalkingdom.org with esmtps (TLSv1:RC4-SHA:128) (Exim 4.76) (envelope-from ) id 1TnHq2-0006cx-1v; Mon, 24 Dec 2012 15:53:54 -0800 Received: by mail-gh0-f186.google.com with SMTP id f11sf2650918ghb.3 for ; Mon, 24 Dec 2012 15:53:35 -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: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=R6nRrLDsIQdmnIJ9SJqcDytA9mwCM0VzDM3DxqyuzBY=; b=UmBsx2zJOkTue2azAmm4DeSMovsz+qnep7E19cjXkjvAH592R7ktXarHISEVxLHPz/ pvlZdeszBAHn/NxtRTtJw4NtFygymrNIX7bwG9RzqLsnWXdFLJYjRrX4upTYVZN1zfDM JD+CPdyBA1X9iCLvb5qN0cmy4qnhAv4T2NS0nCU3vvcWMJ5VU3zK83cYr/Lyu1NK7IoX CnLI2AadKxXmZGhA69SGSyGG5fgkqwk54MobMaKJVHaWENd+KrPokTfdMBmHwsZm9RYF SSqdDAmqTkFEztLUE53scl3ttEXkGiRqJRknSJCF4uFxxrvHT5DPqyXkuKg1cRjAZKM7 BPzA== 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: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=R6nRrLDsIQdmnIJ9SJqcDytA9mwCM0VzDM3DxqyuzBY=; b=FmaGp6vaOh3uT89gExeBTMSGn9MPH69biHyAP9fbA4ac1Q9SPjW7vKBPGxyD19tcuw 2Fu8s81Qj1AYufwKaas/V/2gB+VsrcGEdgn8Feo/HaZWFZhV03k2No4GKRpt56Ckpykb rqGAXDDMxJySKNDaepcffLksdmjQRLict4frLgBHfvk+ZlClWqpBZgx4HVmUDunEjP+u TYOt1Ew+nxiB5MUznEVfxxBc2MZ6Fn3DJnekC8E9LPjF7mSoGWW1X6a+1P2xSmuE2eKb 1/fPI2AUF/DRPuTq0l8wBbAeIl8kWrXpTs2xbtALnLa07e3AGzOvWxBjyTSLTdwfBUGY xxGQ== X-Received: by 10.49.62.164 with SMTP id z4mr3361580qer.34.1356393215483; Mon, 24 Dec 2012 15:53:35 -0800 (PST) X-BeenThere: lojban@googlegroups.com Received: by 10.49.24.37 with SMTP id r5ls2943915qef.85.gmail; Mon, 24 Dec 2012 15:53:35 -0800 (PST) X-Received: by 10.58.255.230 with SMTP id at6mr10659049ved.31.1356393215053; Mon, 24 Dec 2012 15:53:35 -0800 (PST) X-Received: by 10.58.255.230 with SMTP id at6mr10659048ved.31.1356393215041; Mon, 24 Dec 2012 15:53:35 -0800 (PST) Received: from mail-vb0-f45.google.com (mail-vb0-f45.google.com [209.85.212.45]) by gmr-mx.google.com with ESMTPS id q13si6698203vdh.0.2012.12.24.15.53.35 (version=TLSv1/SSLv3 cipher=OTHER); Mon, 24 Dec 2012 15:53:35 -0800 (PST) Received-SPF: pass (google.com: domain of blindbravado@gmail.com designates 209.85.212.45 as permitted sender) client-ip=209.85.212.45; Received: by mail-vb0-f45.google.com with SMTP id p1so7876962vbi.32 for ; Mon, 24 Dec 2012 15:53:35 -0800 (PST) MIME-Version: 1.0 Received: by 10.52.68.175 with SMTP id x15mr30225184vdt.107.1356393214928; Mon, 24 Dec 2012 15:53:34 -0800 (PST) Received: by 10.220.13.197 with HTTP; Mon, 24 Dec 2012 15:53:34 -0800 (PST) Date: Mon, 24 Dec 2012 18:53:34 -0500 Message-ID: Subject: [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.45 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=20cf3078131ec0669904d1a1e742 X-Spam-Score: -0.1 (/) X-Spam_score: -0.1 X-Spam_score_int: 0 X-Spam_bar: / --20cf3078131ec0669904d1a1e742 Content-Type: text/plain; charset=ISO-8859-1 This is rather subtle, so I think it's best to begin with an example. This example isn't all *that* mathematically heavy, but it does involve the 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 integrable on [a,b]. Define the new function (f * g)(x) = 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) | = | 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. Then if |x-y| < d1, from the above |(f * g)(x) - (f * g)(y)| < M e1/M = 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: 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) under the e1 quantifier, and then d2 is instantiated under the e2 quantifier, followed by folding back up to obtain the original statement. None of this instantiation is "real", it's all syntactic, but we operate better when 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's very strange, because it's analogous to {da goi 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 would render proofs like this in Lojban; I would be forced, in order to "set d1=d2" and such, to bind d2, which is bound under a quantifier, to a variable, which 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 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. --20cf3078131ec0669904d1a1e742 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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

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