type theory and higher order logic? : Functional

Application Development · #61 02-22-2007, 02:00 AM

"Marlene Miller" <marlenemiller@worldnet.att.net> writes:
> Let M be the set of primitive pairs whose first component is a
> member of the second component. [x, x'] is in M iff x is in
> x'. Doesn't look circular to me.

I don't see that there can be such a set as M, under the usual notions
of set theory, but I'm not sure what set theory would look like with
this concept of primitive pairs added to it.

Application Development · #62 02-22-2007, 09:09 AM

"Marlene Miller" <marlenemiller@worldnet.att.net> wrote in
news:OOaDh.2418$as2.348@bgtnsc05-news.ops.worldnet.att.net:

> "V.J. Kumar"
>> >
>> > I wonder if what I meant by "primitive pair" got lost.
>> >
>> > Suppose we take pairs to be a primitive notion rather than being
>> > defined in terms of sets. Apparently a primitive pair has a first
>> > component and a second component which can be members of sets.
>> > Suppose a relation is a set whose members are primitive pairs. Then
>> > I guess the membership relation would be the set of primitive pairs
>> > whose first component is a member of the second component.
>>
>> So you define membership (the membership relation) as membership
>> ("the membership relation would be the set of primitive pairs whose
>> first component is a member of"). Does not it strike you as a bit
>> circular ; ?
>
> Let M be the set of primitive pairs whose first component is a member
> of the second component. [x, x'] is in M iff x is in x'. Doesn't look
> circular to me.

OK, so you define a formal entity M that you call "the membership
relation" based on the intuitive notion of set membership. It's a pretty
trivial formalization (one of many). Nothing much is gained by it, the
notion of membership is still undefined despite being more or less
intuitively clear; the notion is just expressed in the set theory
language.

Application Development · #63 02-22-2007, 09:12 AM

Paul Rubin <http://phr.cx@NOSPAM.invalid> wrote in
news:7xr6sid6de.fsf@ruckus.brouhaha.com:

> "Marlene Miller" <marlenemiller@worldnet.att.net> writes:
>> Let M be the set of primitive pairs whose first component is a
>> member of the second component. [x, x'] is in M iff x is in
>> x'. Doesn't look circular to me.
>
> I don't see that there can be such a set as M, under the usual notions
> of set theory,

That would a class under "unusual" notions of set theory, e.g. NBG.

> but I'm not sure what set theory would look like with
> this concept of primitive pairs added to it.

See NFU for a possible application.

>

Application Development · #64 02-22-2007, 12:46 PM

"V.J. Kumar" <vjkmail@gmail.com> writes:
> > I don't see that there can be such a set as M, under the usual notions
> > of set theory,
>
> That would a class under "unusual" notions of set theory, e.g. NBG.

Is that von Neumann-Bernays-Godel? M would be a proper class, I think,
and still not a set.

> > but I'm not sure what set theory would look like with
> > this concept of primitive pairs added to it.
> See NFU for a possible application.

What's that?

Application Development · #65 02-22-2007, 12:49 PM

In article <7xzm76nl0n.fsf@ruckus.brouhaha.com>, Paul Rubin wrote:
> "V.J. Kumar" <vjkmail@gmail.com> writes:
>> See NFU for a possible application.
>
> What's that?

Quine's New Foundations with primitive elements.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Application Development · #66 02-22-2007, 01:12 PM

Lauri Alanko <la@iki.fi> writes:
> Now form a new set from all the second components of A, and the empty
> set. Call the result B.

That would be the notorious "set of all sets". I don't know how
primitive pairs are supposed to be defined so maybe it's in a way that
one can't extract components from them like that.

Application Development · #67 02-22-2007, 01:14 PM

Paul Rubin <http://phr.cx@NOSPAM.invalid> wrote in
news:7xzm76nl0n.fsf@ruckus.brouhaha.com:

> "V.J. Kumar" <vjkmail@gmail.com> writes:
>> > I don't see that there can be such a set as M, under the usual
>> > notions of set theory,
>>
>> That would a class under "unusual" notions of set theory, e.g. NBG.
>
> Is that von Neumann-Bernays-Godel?
Yes.

>M would be a proper class, I think,
> and still not a set.

That's what I wrote isn't it ?

>
>> > but I'm not sure what set theory would look like with
>> > this concept of primitive pairs added to it.
>> See NFU for a possible application.
>
> What's that?

New Foundations with Urelements

>

Application Development · #68 02-22-2007, 01:15 PM

In article <Xns98DE82795BCDAvdghher@194.177.96.26>, V.J. Kumar wrote:
> Neelakantan Krishnaswami <neelk@cs.cmu.edu> wrote in
>>
>> That depends on what you mean by "membership relation". For any given
>> set, you can define a membership relation in exactly the way you
>> describe, as a set of pairs where the first component is an element of
>> the second component.
>
> In a set theory set membership is an undefined primitive (along with the
> notion of set), both being understood intuitively. Set membership can be
> *interpreted*, but not defined, as a relation. Otherwise, you'll get a
> chicken-and-egg problem.

Yes, that was a bad choice of language on my part.

> What do you mean ? Are you claiming that when we say a sheep is a member
> of a flock, we consider the sheep a flock (set) as well ?

Yes. ZF and its usual derivatives do not have primitive atoms (urelements), so
if you have an interpretation of a sheep in ZF, then it's a set.

(As an aside, I think "an interpretation of a sheep in ZF" is the
funniest phrase I've written all week, so thank you!)

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Application Development · #69 02-22-2007, 01:22 PM

Neelakantan Krishnaswami <neelk@cs.cmu.edu> wrote in
news:slrnetrnds.at9.neelk@gs3106.sp.cs.cmu.edu:

> In article <Xns98DE82795BCDAvdghher@194.177.96.26>, V.J. Kumar wrote:
>> Neelakantan Krishnaswami <neelk@cs.cmu.edu> wrote in
>>>
>>> That depends on what you mean by "membership relation". For any
>>> given set, you can define a membership relation in exactly the way
>>> you describe, as a set of pairs where the first component is an
>>> element of the second component.
>>
>> In a set theory set membership is an undefined primitive (along with
>> the notion of set), both being understood intuitively. Set
>> membership can be *interpreted*, but not defined, as a relation.
>> Otherwise, you'll get a chicken-and-egg problem.
>
> Yes, that was a bad choice of language on my part.
>
>> What do you mean ? Are you claiming that when we say a sheep is a
>> member of a flock, we consider the sheep a flock (set) as well ?
>
> Yes. ZF and its usual derivatives do not have primitive atoms
> (urelements), so if you have an interpretation of a sheep in ZF, then
> it's a set.

OK, sounds good

>
> (As an aside, I think "an interpretation of a sheep in ZF" is the
> funniest phrase I've written all week, so thank you!)
>
>

Application Development · #70 02-23-2007, 01:36 AM

Neelakantan Krishnaswami wrote:
> Marlene Miller wrote:
> > In this metaphor, I am not sure what is meant by the representation
> > of the semantics module.
>
> Sorry for any confusion.
>
> Suppose that you're a compiler writer, and you want to find out if a
> particular optimization is justified. For example, you want to find out
> whether a common subexpression elimination is safe:
>
> (x + y) * (x + y) --> let z = x + y in z * z
>
> You open up your semantics textbook, and you read that the lambda
> calculus has a model, which satisfies the following equation:
>
> (let z = e in e') == e'[e/z]
>
> You realize that if you take e to be x + y, and e' to be z * z, then
> your proposed optimization is an instance of this schema.
>
> In this sense, you're a client of the semantics module -- you're using
> the fact that the lambda calculus has a semantics, and you're using
> the fact that it satisfies the above equation. How that was done is
> not important to verifying your optimization as long as it was done.
>
> The justification for this are the actual semantics and proofs of the
> equations. This is the implementation. The representation of the
> lambda calculus might be the domain theoretic model, in the same way a
> finite set type might be represented by a binary tree in a computer
> program. Likewise, the proofs of the various equalities would be part
> of the implementation of the semantics module, just as the
> implementation of the set membership function is part of the
> implementation of the set module.

Then, as a first approximation, a representation is a model. A model has an
implementation. (Some implementations have an interface.)

>
> The book ToP explains how all those constructions work, which is the
> sense in which I mean that it is giving the implementation of the
> semantics module.
>
> I hope this is clearer, though if it's not it's probably not worth
> worrying too much about.

I guess the thing being represented is a concept. The representation is a
formal theory.

>
> --
> Neel R. Krishnaswami
> neelk@cs.cmu.edu

Similar Threads
Thread	Thread Starter	Forum	Replies	Last Post
higher-order function	usenet	lisp	3	11-03-2007 07:35 PM
higher order functions	usenet	Functional	10	06-01-2007 05:41 PM
HOM: Higher Order Messaging	usenet	Object	3	11-07-2006 05:39 PM
Higher order curves	usenet	Java-Games	12	05-15-2005 10:34 PM
Higher order curves	usenet	Graphics	6	05-15-2005 10:34 PM

type theory and higher order logic? : Functional

Similar Threads