Is \dot{F} in ZFU an Injection from Urelements to Naturals?

[CRGreathouse]

I'm reading a paper and I came across a passage that seems wrong. The context is describing axioms for a system ZFU, with an operation \dot F that relates urelements to natural numbers. \dot U(v) holds exactly when v is an urelement. The first line, then, says that \dot F(u,v) is a relation between a natural number u and an urelement v.

\forall u\forall v(\dot F(u,v)\to(u\in\mathbb{N}\operatorname{\&}\dot U(v)))\operatorname{\&}
\forall v(\dot U(v)\to\exists u(\dot F(u,v)))\operatorname{\&}
\forall u\forall v\forall w((\dot F(u,v)\operatorname{\&}\dot F(u,w))\to v=w)

(The [above three lines] states that \dot F describes a bijection between \mathbb{N} and the set of urelements.)
​

But surely, the axiom quotes says that \dot F is an injection from the set of urelements to the naturals? The paper does assume the existence of at least one urelement, but not infinitely many.Second, the paper opens with a discussion of category theory:

Visser introduced five different categories of interpretations between theories, namely, INT₀ (the category of synonymy), INT₁ (the category of homotopy), INT₂ (the category of weak homotopy), INT₃ (the category of equivalence), and INT₄ (the category of mutual interpretability)​

The reference in the paper is to conference proceedings from the '70s, which aren't particularly accessible. Any better references -- especially for one who will be browsing, and who doesn't actually know category theory?

 

[Hurkyl]

But surely, the axiom quotes says that \dot F is an injection from the set of urelements to the naturals?

Looks like the third clause does. The second clause looks like it's saying F is a surjection.

Second, the paper opens with a discussion of category theory:

Are you sure 'category' is being used in the sense of category theory, rather than just in the English sense?

 

[CRGreathouse]

Looks like the third clause does. The second clause looks like it's saying F is a surjection.

Thanks, that's why I post here. (sigh) I'll look it over more carefully.

Are you sure 'category' is being used in the sense of category theory, rather than just in the English sense?

No, I'm not sure, but it looked like category theory to my unpracticed eyes: "The objects in these categories are first-order theories, the morphisms are interpretations up to some level of identification between interpretations."

Regardless, have you heard of the INT categories or the scale of interpretations (synonymy, homotopy, weak homotopy, equivalence, mutual interpretability)? The paper doesn't actually define them, it just gives the briefest of descriptions.

 

[Hurkyl]

Hrm. I now notice that you said a reverse of what I thought you said.

It asserts that F is the graph of a partial function from N to the urelements that is surjective and one-to-one, but I now notice it doesn't assert that partial function is everywhere-defined! As you observe, that is the same as F being (the converse of) the graph of an injective function from the urelements to N.


Yep, that looks like category theory. I can't say that I've heard of those categories, sorry.

 

[CRGreathouse]

The importance is that the text implies that there are a countably infinite number of urelements, where the formula itself seems only to require a countable number of urelements.

My reading on the lines:
1. F is a relation between numbers and urelements.
2. All urelements have a number.
3. Two urelements with the same number are the same.

Yep, that looks like category theory. I can't say that I've heard of those categories, sorry.

That's actually something of a relief. If you don't know it, at least its use is probably confined to category theory proper (not a part of category theory that 'everyone knows').

 

[Hurkyl]

If you don't know it, at least its use is probably confined to category theory proper (not a part of category theory that 'everyone knows').

I find it much more likely that it's confined to model theory proper -- it looks like he's making use of categories in the study of formal logic, not the other way around.

 

[CRGreathouse]

Hmm, I hadn't even heard of model theory. I'll poke around and see if I can find anything.

 

[peos69]

I think you should present the whole paper here so we can all criticize it for the following reasons:
1) First of all what is F(u,v), an operation between N and V, a function,arelation ?
2)The 3rd formula simply says that F(u,v) is a function between N and V ( assuming that F(u,v) it is another notation for F:N------>V.Remember? No two ordered pairs have the same
first member
3) To say that F(u,v) is abijection from N to V here is the way:
Let (x) denote: for all x
Let Ey denote: there exists a y
Let E!y denote: there exists a unique y
And F is a bijection between N and V <=====> (v)[ vεV------->E!u( uεΝ & (u,v)εF)]
Now the E!u( uεΝ & (u,v)εF) part is equivalent to
Eu( uεΝ & (u,v)εF& (u)(w)[(uεΝ & (u,v)εF)&(wεΝ& (w,v)εF)------->u=w]
And the (u)(w)[(uεΝ & (u,v)εF)&(wεΝ& (w,v)εF)------->u=w] part is equivalent to the known
formula (u)(w)[F(u) =F(w)-------> u=w]

 

[CRGreathouse]

I think you should present the whole paper here so we can all criticize it for the following reasons

I linked to it in the first sentence of my first post. Here's the link again:
http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.ndjfl/1143468313

1) First of all what is F(u,v), an operation between N and V, a function,arelation ?

I explained this in my first paragraph as well:
"The first line, then, says that \dot F(u,v) is a relation between a natural number u and an urelement v."

2)The 3rd formula simply says that F(u,v) is a function between N and V ( assuming that F(u,v) it is another notation for F:N------>V.

I'm not willing to assume that the relation F is a function from N to V. I see no reason, for example, to think that the natural number 2 maps to anything. Now it does look like it is a function N\leftarrow V -- and that is the essence of my question.

 

[peos69]

Tomorrow we will clear things out

 

[peos69]

I'm reading a paper and I came across a passage that seems wrong. The context is describing axioms for a system ZFU, with an operation \dot F that relates urelements to natural numbers. \dot U(v) holds exactly when v is an urelement. The first line, then, says that \dot F(u,v) is a relation between a natural number u and an urelement v.

\forall u\forall v(\dot F(u,v)\to(u\in\mathbb{N}\operatorname{\&amp;}\dot U(v)))\operatorname{\&amp;}
\forall v(\dot U(v)\to\exists u(\dot F(u,v)))\operatorname{\&amp;}
\forall u\forall v\forall w((\dot F(u,v)\operatorname{\&amp;}\dot F(u,w))\to v=w)

(The [above three lines] states that \dot F describes a bijection between \mathbb{N} and the set of urelements.)
​

Well what is it then operation, relation,function?

 

[CRGreathouse]

F is a relation.

 

[peos69]

HOW do you know?

 

[CRGreathouse]

HOW do you know?

Because it's obvious from context? Because the paper that I linked to, twice, says that explicitly?

"The language of ZFU will be a language with two binary relations \in and \dot{F}"