# Logical meaning of notation

1. Feb 2, 2005

### Bartholomew

This notation: S={x|Fx} where Fx is some logical fomula of x

I have never seen this formally defined, only explained in words and used. I think that it logically means that "a is an element of S" is logically equivalent to "Fa." Am I right?

2. Feb 2, 2005

### gnome

I'd read it as "S is the set of all x's such that Fx is true".

But then, I'm no authority.

3. Feb 2, 2005

### hypermorphism

I usually read the vertical pipe in these cases as "such that". In many texts, the other symbol for "such that", the colon, is used in its place. One reads S={x|Fx} as "S is the set of all x such that (for which) Fx is true". See http://mathworld.wolfram.com/SuchThat.html .

4. Feb 2, 2005

### Hurkyl

Staff Emeritus
$$a \in \{x | \phi x\} \Leftrightarrow \phi a$$

5. Feb 2, 2005

### gnome

Would you please put that into words?

(Does that agree, or disagree, with what I said?)

Last edited: Feb 2, 2005
6. Feb 2, 2005

### Hurkyl

Staff Emeritus
Yes, {x|Fx} is usually pronounced as "the set of all x's such that Fx is true".

7. Feb 2, 2005

### Physicsguru

Hurkyl, you have made an error in this answer, albeit a minor one.

Suppose that S is defined to be the set of all X, such that P(x) is true. My question now is this. Can a frog be an element of set S, yes or no?

Kind regards,

Guru

Last edited: Feb 2, 2005
8. Feb 2, 2005

### Bartholomew

Okay, thanks.

While I'm at it, is there a symbol for "the nth element of"? As in, "appears as the first element of an ordered pair."

9. Feb 2, 2005

### Hurkyl

Staff Emeritus
A frog is an element of S iff P(frog). I don't see the problem. :tongue:

There is indeed an error; I've presented the set builder notation of naive set theory, which is known to be inconsistent. In ZFC, it becomes the following:

$$a \in \{ x \in A | \phi a \} \Leftrightarrow a \in A \wedge \phi a$$

And if you're combining set theory with other axioms, you also have to specify that all the appropriate things are of the type Set.

Certainly, via the recursion theorem. However, usually one moves beyond the usual model of an ordered pair, and defines an n-tuple as a function whose domain is n. (That is, the set {0, 1, 2, ..., n-1}) So, asking for the "m-th element" is merely evaluating the function at m. This generalizes to using any set as the index set.

10. Feb 2, 2005

### gnome

In Haskell there is a function fst, so you can write
> fst(x,y)
and it returns
> x
S = {fst(X,Y) | fst(A,B) = A}

11. Feb 2, 2005

### Bartholomew

What actually prompted my question was the definition of a function f from A to B -- the set of all ordered pairs (A,B) such that every element in A appears exactly once as the first component of an ordered pair in f. So you can't use functions to describe the m-th element in that context. Order in an n-tuple must be more basic than the concept of a function, or else there must be a better way to define a function.

12. Feb 3, 2005

### matt grime

All one needs to define an ordered pair, is the set{{x},{x,y}} thus you can now define functions. If we assume the continuum hypothesis, then given any index set we can form an ordinal of the same set and talk about the s'th element in the set quite easily. However, forming products of indexed sets indexed over things other than subsets of the natural numbers isn't something you come across at a basic level, though it is important in Category Theory and such associated topics. For finite, positions, one can say that the m'th element of the ordered n-tuple is the element in the set of sets of cardinality m that is not in any of the set of sets of strictly smaller cardinality, where we assume cardinals of finite sets are well understood, since we could if we felt like it talk of them in terms of elements of the inductive set (assuming we're in ZF(C)).

13. Feb 3, 2005

### Physicsguru

Let me ask you something Hurkyl, if you don't mind. Suppose we let R denote a set, and let it denote the set of all sets which aren't elements of themselves. You are now asked to decide whether or not R is an element of itself. Using either ZFC or naive set theory (your choice), how would you make the decision?

Kind regards,

Guru

14. Feb 3, 2005

### matt grime

You can't formaluta that in a proper permissible statement in ZFC, ie you need

R= {x in S | x not in x}
however, what is S?

15. Feb 24, 2005

### Owen Holden

Not quite.
imo, {x|Fx} is read 'the x's such that Fx is true'

It is a described class that is defined in context:

D1. G{x|Fx} =df Ey(Ax(x e y <-> Fx) & Gy).

EyAx(x e y <-> Fx) -> [(z e {x|Fx}) <-> Fz]

Proof:

1. (z e {x|Fx}) <-> Ey(Ax(x e y <-> Fx) & (z e y))

By, D1.

2. (z e {x|Fx}) <-> Ey(Ax(x e y <-> Fx) & Fz)

By: 1, (Ax(Hx <-> Kx) & Hz) <-> (Ax(Hx <-> Kx) & Kz).

3. (z e {x|Fx}) <-> (EyAx(x e y <-> Fx) & Fz)

By: 2, Ex(Hx & p) <-> (ExHx & p).

4. EyAx(x e y <-> Fx) -> [(z e {x|Fx}) <-> Fz]

By: 3, (p <-> (q & r)) -> (q -> (p <-> r)).

That is to say: z e {x|Fx} <-> Fz, only if, EyAx(x e y <-> Fx) is true.

If we have a theory of types then, z e {x|Fx} <-> Fz is valid.

16. Feb 24, 2005

### Owen Holden

D1. G{x:Fx} =df Ey(Ax(x e y <-> Fx) & Gy)

{x:~(x e x)} e {x:~(x e x)} <-> Ey(Ax(x e y <-> ~(x e x)) & y e y)

But, Ax(x e y <-> ~(x e x)) is contradictory.
Because, Ax(xSy <-> ~(xSx)) -> (ySy <-> ~(ySy)) for all relations S.
i.e. ~Ax(xSy <-> ~(xSx)) is a theorem for all y and all S.

Therefore Ey(Ax(x e y <-> ~(x e x)) & y e y) is a contradiction.

Therefore, ~({x:~(x e x)} e {x:~(x e x)}), is a theorem.

The Russell Class (R), {x:~(x e x)}, is not a member of itself.