Received: by 10.42.19.136 with SMTP id c8mr463173icb.79.1302267947128;
        Fri, 08 Apr 2011 06:05:47 -0700 (PDT)
X-BeenThere: one-logic@googlegroups.com
Received: by 10.231.32.138 with SMTP id c10ls1431696ibd.2.p; Fri, 08 Apr 2011
 06:05:46 -0700 (PDT)
Received: by 10.42.96.71 with SMTP id i7mr515052icn.46.1302267946724;
        Fri, 08 Apr 2011 06:05:46 -0700 (PDT)
Received: by 10.42.96.71 with SMTP id i7mr515051icn.46.1302267946701;
        Fri, 08 Apr 2011 06:05:46 -0700 (PDT)
Return-Path: <generic.intellige...@gmail.com>
Received: from mail-iy0-f180.google.com (mail-iy0-f180.google.com [209.85.210.180])
        by gmr-mx.google.com with ESMTPS id xk8si473774icb.5.2011.04.08.06.05.46
        (version=TLSv1/SSLv3 cipher=OTHER);
        Fri, 08 Apr 2011 06:05:46 -0700 (PDT)
Received-SPF: pass (google.com: domain of generic.intellige...@gmail.com designates 209.85.210.180 as permitted sender) client-ip=209.85.210.180;
Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of generic.intellige...@gmail.com designates 209.85.210.180 as permitted sender) smtp.mail=generic.intellige...@gmail.com; dkim=pass (test mode) header...@gmail.com
Received: by mail-iy0-f180.google.com with SMTP id 40so4854071iyf.39
        for <one-logic@googlegroups.com>; Fri, 08 Apr 2011 06:05:46 -0700 (PDT)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
        d=gmail.com; s=gamma;
        h=domainkey-signature:mime-version:in-reply-to:references:date
         :message-id:subject:from:to:content-type;
        bh=zlmZnvCWfKbBes4OVAZ/oLJrbjjdU0hhcBOtRMG4WE4=;
        b=DAMH+BWpZ3egOa7f/ChqyE+MG4Rkwhz6/xs+mQJXLGhuHnlNMqzkF7VKQqO9ElE2iz
         nRtOjjKUrjJj9wlhWaql2O5Ang2r/5/dzQaJ5o/4gGFDeHOURV/qKqFid/2zMIrmpaaV
         99Mi8UDWKik3wTsg0FHHhNurAKZjwFXiBu4XY=
DomainKey-Signature: a=rsa-sha1; c=nofws;
        d=gmail.com; s=gamma;
        h=mime-version:in-reply-to:references:date:message-id:subject:from:to
         :content-type;
        b=M3K4o0yV9bZ7xFYPk1okPcDSvbejpCZ9k3Pd8yW/Zld1AIqcvDp6UDQQsuKD8kt3gy
         U78lKnk8X0D+PC87C6KIT6POLzipZ9gs0e//G2qetkhSpnUGsWPknlFS32xkPLrWav4b
         LAsO5mIjCKjqVxL+qyIpyw32HDiik4hgAIsX4=
MIME-Version: 1.0
Received: by 10.231.117.129 with SMTP id r1mr2010068ibq.195.1302267946584;
 Fri, 08 Apr 2011 06:05:46 -0700 (PDT)
Received: by 10.231.19.136 with HTTP; Fri, 8 Apr 2011 06:05:46 -0700 (PDT)
In-Reply-To: <BANLkTi=M3KCb=KaP_pNOuP6a+seB+Zf...@mail.gmail.com>
References: <BANLkTikd_DYLkLTvB6YVZvAiffRz1Ug...@mail.gmail.com>
	<BANLkTi=M3KCb=KaP_pNOuP6a+seB+Zf...@mail.gmail.com>
Date: Fri, 8 Apr 2011 21:05:46 +0800
Message-ID: <BANLkTimp4JAEPFOMozv8riLzDSvDQOG...@mail.gmail.com>
Subject: Re: [one-logic] quantifiers
From: =?UTF-8?B?WUtZIChZYW4gS2luZyBZaW4sIOeUhOaZr+i0pCk=?= <generic.intellige...@gmail.com>
To: one-logic@googlegroups.com
Content-Type: multipart/alternative; boundary=0016369201385bcbf604a067e2fb

--0016369201385bcbf604a067e2fb
Content-Type: text/plain; charset=ISO-8859-7
Content-Transfer-Encoding: quoted-printable

On Fri, Apr 8, 2011 at 7:13 PM, Russell Wallace
<russell.wall...@gmail.com>wrote:

Yes.
>
> For all x, p(x)  =3D=3D  p(x) =3D K(true)
> There exists (x), p(x)  =3D=3D  p(x) !=3D K(false)
>

1.
What if I want to write:
      for all x [ p(x) -> q(x) ] ?

2.
The symbols "for all" and "exists" do not seem to be proper combinators
(looking at the above definitions).

They are defined via extra-combinatory-logic rules...

Maybe I can set up the equation:
    =D0XPx =3D=3D ( P(x) =3D K true )
and solve for =D0?

Note:  the left hand side above means:
    "for all x in X, P(x)".

KY

--0016369201385bcbf604a067e2fb
Content-Type: text/html; charset=ISO-8859-7
Content-Transfer-Encoding: quoted-printable

<div>On Fri, Apr 8, 2011 at 7:13 PM, Russell Wallace <span dir=3D"ltr">&lt;=
<a href=3D"mailto:russell.wall...@gmail.com">russell.wall...@gmail.com</a>&=
gt;</span> wrote:</div><div class=3D"gmail_quote"><br><blockquote class=3D"=
gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-=
left:1ex;">
Yes.<br>
<br>
For all x, p(x) =A0=3D=3D =A0p(x) =3D K(true)<br>
There exists (x), p(x) =A0=3D=3D =A0p(x) !=3D K(false)<br></blockquote><div=
><br></div><div>1.</div><div>What if I want to write:</div><div>=A0=A0 =A0 =
=A0for all x [ p(x) -&gt; q(x) ] ?</div><div><br></div><div>2.</div><div>Th=
e symbols &quot;for all&quot; and &quot;exists&quot; do not seem to be prop=
er combinators (looking at the above definitions).</div>
<div><br></div><div>They are defined via extra-combinatory-logic rules...</=
div><div><br></div><div>Maybe I can set up the equation:</div><div>=A0=A0 =
=A0=D0XPx =3D=3D ( P(x) =3D K true )</div><div>and solve for =D0?</div><div=
><br></div><div>
Note: =A0the left hand side above means:</div><div>=A0=A0 =A0&quot;for all =
x in X, P(x)&quot;.</div><div><br></div><div>KY</div></div>

--0016369201385bcbf604a067e2fb--