quantifiers

[YKY (Yan King Yin, 甄景贤)]

Hi all =)

I probably asked this before, in private to Abram, but I forgot the answer...

Is it possible to define "for all" and "exisits" purely in terms of S, K, I, in combinatory logic?

It seems that Curry's formulations (and there are many) often use Π and Ξ as primitives -- ie, they are not further reducible to other combinators.

For your reference, Π and Ξ are defined via:

     MN |- ΞM

and

     ΠMN, MP |- NP.

Thanks!! =)

KY

[Russell Wallace]

2011/4/8 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>:

> Hi all =)
> I probably asked this before, in private to Abram, but I forgot the
> answer...
> Is it possible to define "for all" and "exisits" purely in terms of S, K, I,
> in combinatory logic?

Yes.

For all x, p(x) == p(x) = K(true)
There exists (x), p(x) == p(x) != K(false)

Whether it is pragmatically more useful to so reduce them or keep them
as basic syntax, I'm not yet sure.

[YKY (Yan King Yin, 甄景贤)]

Sorry, I confused Ξ with Σ.

The correct definition of  Ξ is this:
     ΞXY == for all x in X, Yx
which is universal quantification.

Curry's Π and Σ are defined via:
     MN |- ΣM

and
     ΠMN, MP |- NP.

It seems that Π is equivalent to Ξ.

KY

[YKY (Yan King Yin, 甄景贤)]

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

Yes.

For all x, p(x)  ==  p(x) = K(true)
There exists (x), p(x)  ==  p(x) != 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:

    ΠXPx == ( P(x) = K true )

and solve for Π?

Note:  the left hand side above means:

    "for all x in X, P(x)".

KY

[Russell Wallace]

2011/4/8 YKY (Yan King Yin, 甄景贤) <generic.in...@gmail.com>:

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

(p(x)->q(x)) = K(true)

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

Right, they are binding syntax - same status as lambda.

[YKY (Yan King Yin, 甄景贤)]

On Fri, Apr 8, 2011 at 9:08 PM, Russell Wallace <russell...@gmail.com> wrote:

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

Right, they are binding syntax - same status as lambda.

Oh, so it is impossible to define Π and Σ as combinators in terms of S,K,I?

Damn, this has beguiled me for a lonnnng time... =)

KY