For exery x exists y equal to x

[haael]

I'm having problems with this statement in first-order logic with equality:

$$\forall x \exists y . x = y$$

For every element x there exists element y equal to that one. This seems obviously correct.

My questions: Is this an axiom? If not, how to proove it from other equality axioms?

 

[Hornbein]

I'm having problems with this statement in first-order logic with equality:

$$\forall x \exists y . x = y$$

For every element x there exists element y equal to that one. This seems obviously correct.

My questions: Is this an axiom? If not, how to proove it from other equality axioms?

I dunno. Quite often a set of axioms is rather arbitrary in that there are several different bu logically equivalent sets.

 

[Fredrik]

My questions: Is this an axiom?

That question doesn't really make sense. A set of statements defines a branch of mathematics...the branch in which all the statements are true. The individual statements are called axioms...for that branch of mathematics.

If not, how to proove it from other equality axioms?

What are the other axioms?

 

[haael]

Let's say we work in a finite structure. For example let's have a structure with 4 elements {a, b, c, d} and relations on them.

What are the other axioms?

Equality is reflexive, symmetric and transitive:
$$\forall x. x = x$$
$$\forall x,y. x = y \rightarrow y = x$$
$$\forall x,y,z. x = y \wedge y = z \rightarrow x = z$$

And for each relation R on each position when element x is substituted to the equal element y, the value of the relation doesn't change:
$$\forall x,y. x = y \rightarrow (R(..., x, ...) \leftrightarrow R(..., y, ...))$$

The sentence in question has something to do with the identity function. I'm not sure, but it probably states that the identity function exists.
$$\forall x \exists y. id(x) = y$$
$$\forall x. id(x) = x$$
$$\forall x \exists y. x = y$$

This does not follow from any axiom as far as I can tell, but can the identity function NOT exist? Isn't the existence of the identity function obvious? So it should be an axiom.

 

[Fredrik]

It seems to me that if the set is non-empty, then the axiom you're concerned about can be proved from the others by an informal argument: Let z be an element of the set. The axiom $\forall x~x=x$ tells us that z=z. This implies that $\exists y~z=y$. Since z is arbitrary, this implies that $\forall x\exists y~x=y$.

If my argument can be turned into a formal derivation, then maybe the axiom should be viewed as saying that we're dealing with non-empty sets?

Not sure if this argument can be formalized in this system. I'm still not very good at formal logic. I'm trying to learn more about it though. I'd be interested in seeing how this is presented in your book. What book is it?

You seem to be thinking that "obvious" statements shouldn't be axioms. This suggests some kind of misunderstanding. In this context, all statements should be viewed as meaningless strings of text. There are rules that tell us which strings of text can be considered "formulas", and rules that tell us how to construct formulas from formulas. The axioms are just the formulas that appear on the list of formulas that defines the branch of mathematics that we're currently interested in.

Since you seem to be concerned about the last three axioms you listed, but not the first three, I'm guessing that you have chosen to view = as a meaningless symbol. (If we think of x=y as the statement that the symbols x and y represent the same thing, then the first three axioms are all obvious). Wouldn't it make just as much sense to view "id" as a meaningless symbol, instead of as "the identity function"? (I have to admit, I don't see the point of the "id" axioms. That's one of the reasons I'd like to see the book).

In ZFC set theory, the identity function on a set X is (usually defined as) a specific subset of the cartesian product X×X. It takes several axioms to ensure the existence of the cartesian product. The axiom of separation ensures the existence of the appropriate subset.

 

[Erland]

Using natural deduction (a related proof by Hilbert style axioms is also possible):

1. $\forall x\ x=x\vdash\forall x\ x=x$ (Conclusion among hypotheses)
2. $\forall x\ x=x\vdash x=x$ (1, $\forall$-elimination)
3. $\forall x\ x=x\vdash\exists y \ x=y$ (2, $\exists$-introduction) (OK, since $x$ is free for $y$ in $x=y$.)
4. $\forall x\ x=x\vdash\forall x\ \exists y \ x=y$ (3, $\forall$-introduction) (OK, since the hypothesis in 3 does not contain $x$ freely.)

So, $\forall x\ \exists y \ x=y$ is a logical consequence of the equality axiom $\forall x\ x=x$.

 

[haael]

Thanks. That was the answer I needed.