# Prove ΦxΦ =Φ

1. Sep 3, 2009

### evagelos

Prove:

$$\emptyset\times\emptyset =\emptyset$$

2. Sep 4, 2009

### Preno

The empty set has no elements. Therefore, there is no ordered pair of elements of the empty set (using any of the common definitions of an ordered pair). There isn't really much to prove.

3. Sep 4, 2009

### HallsofIvy

Or, if you want to get "fancy", a proof by contradiction: Suppose that $\Phi \times \Phi$ is not empty. Then there exist a pair, (a, b) in $\Phi \times \Phi$ such that $a\in \Phi$ which contradicts the fact that $\Phi$ is empty.

4. Sep 4, 2009

5. Sep 4, 2009

### jgens

I'm not a mathematician, so perhaps my comment is naive, but the empty set is defined as the unique set which contains no elements. If $a$ were a member of the empty set, then the empty set would not be empty which is a contradiction. Maybe I'm misunderstanding something here?

6. Sep 4, 2009

### Dragonfall

You're not. Evagelos is wrong in assuming that there is no contradiction. It contradicts (assuming we're talking about ZF) the axiom of the empty set.

7. Sep 4, 2009

### Hurkyl

Staff Emeritus
HoI's statement is a theorem.

8. Sep 4, 2009

Halls' approach is, as others have stated, fine.

9. Sep 4, 2009

### techmologist

Yeah, I thought that was pretty much the definition of cartesian product: If A and B are sets, and C = AxB, then y is in C iff there is an a in A and a b in B such that y = (a, b).

If one of A or B is the empty set, then for every y, it is not in C.

10. Sep 4, 2009

### evagelos

Let Hall write a formal proof then to find out whether his proof is right or wrong.

Sorry Halls i know that you dislike formal proofs,but that is the only way,otherwise we will argue indefinitely

11. Sep 4, 2009

### evagelos

No ,i did not say that there is no proof by contradiction,but Hall's contradiction is not based somewhere

12. Sep 4, 2009

### Dragonfall

Like I said, his contradiction is based on the axiom of of the empty set, is it not?

What do you mean by "based on" then?

13. Sep 5, 2009

### CRGreathouse

The proof is so shockingly obvious that I'm surprised even you could ask for it. I can only assume this is a homework problem.

14. Sep 7, 2009

### CompuChip

I fail to see how Hall's proof is not a formal one.

Alternatively, you could give a direct proof: it is true that
$$\emptyset\times\emptyset \subseteq \emptyset$$
because for all $x \in \emptyset\times\emptyset$, $x \in \emptyset$ - similarly the other inclusion follows. (In fact, if $A \subseteq \emptyset$, then it is always the case that $A = \emptyset$).

15. Sep 7, 2009

### HallsofIvy

We have asked evagelos repeatedly what he means by a "formal" proof and he has never answered clearly. I suspect he means something like used in "Principia Mathematica".

16. Sep 7, 2009

### CompuChip

Wait, let me get my ruler and compass...

17. Sep 7, 2009

### Preno

I suppose if you wanna get fancy, you can always try a categorical proof (of isomorphism, that is).

Last edited: Sep 7, 2009
18. Sep 9, 2009

### evagelos

Here is a formal proof of $$\emptyset\times\emptyset = \emptyset$$,a direct one:

1)$$\forall A\forall B [ A\times B =\emptyset\Longleftrightarrow A=\emptyset\vee B=\emptyset]$$.....................................................................................a theorem in set theory

2) $$\emptyset\times\emptyset =\emptyset\Longleftrightarrow \emptyset = \emptyset\vee\emptyset =\emptyset$$..............................................................................from (1) and using Universal Elimination ,where we put $$A=\emptyset$$ and $$B=\emptyset$$

3)$$\emptyset=\emptyset\vee \emptyset =\emptyset\Longrightarrow \emptyset\times\emptyset =\emptyset$$...............................................................................from (2) and using biconditional Elimination

4)$$\forall x[ x=x]$$...........................................................................................................an axiom in equality

5)$$\emptyset =\emptyset$$.............................................................................................................from (4) and using Universal Elimination,where we put $$x=\emptyset$$

6)$$\emptyset =\emptyset\vee \emptyset =\emptyset$$......................................................................................from (5) and using idempotent law ( p ====> p or p)

7)$$\emptyset\times\emptyset =\emptyset$$....................................................................................from (3) and (6) and using M.Ponens.

Now if you wish, write a formal proof using contradiction

19. Sep 10, 2009

Okay (haven't looked through this, right now will take you on face value) but that does not disqualify Hall's proof as being perfectly valid.

20. Sep 10, 2009

### CRGreathouse

Yeah, with theorems like this it's pretty easy.

21. Sep 10, 2009

### evagelos

Of all kinds of proofs short,long,detailed,rigorous e.t.c ,the formal proof is the easiest one to check ,because each step it is either axiom,theorem,definition or the logical conclusion of previous steps using a rule of logic.

I really don't understand why people have difficulties in checking formal proofs.

In a formal proof everything is explicitly mentioned and thus can be checked.

That is why i asked Halls to write a formal contradictory proof so that we will be able to check its validity without any doubt whatsoever .

Some times we write proofs that we think that are right and if somebody says the opposite we can hardly accept that.

22. Sep 10, 2009

I'll make one comment about the tone of your most recent response: I'm not sure of your educational background, but I did see, study, understand, and create, many formal proofs in my undergraduate and graduate careers, and I was not intimidated by the form of your proof-the fact that I was intimidated is what I saw as the implicit message in your most recent post. If I misunderstood, although I don't think I did, I apologize.

However, whether my impression is or is not correct is neither here nor there. The issue I responded to is whether Hall's proof was valid: it is.

Formality in a proof simply for the sake of formality is little more than window dressing: if your point is that some minutiae were not explicitly stated in Halls' proof, that might technically be true, but, just as in textbooks and lectures, it is common to condense things for the sake of brevity (and, some would argue, to ensure that the reader be able to fill in some justifications he/she may have). That does not take away from the correctness of the proof.

It is interesting to read Bromwich's classical treatise on infinite series: although it may sound contradictory, there the writing is formal in a conversational way: the proofs he chose to present are thorough, concise, and clear, without all the formality you believe to be required. Is one of these approaches better than the other? Not really; I will argue strongly that they have different realms of appropriateness. Your proof would be appropriate for a high undergraduate/beginning undergraduate class (on proof methods, mathematical writing, set theory, or another class) in which, more than the proof itself, the goal of the problem is for the writer to grasp, organize, and present, the relevant theory and notations. In a survey class, an introductory class, or the like, the approach Hall (and others) presented would be more appropriate: beginning students' mathematics backgrounds are neither broad enough nor deep enough to be able to understand, or present, your proof. Hall's touches on everything needed without (this is important) sacrificing any of the relevant ideas: it is perfectly sound.

It is not because I don't understand what you posted that I did not read through it: I now see what you meant by "formal proof" and, as I hope I have shown, I did not read through it because I did not (and still do not) think it is necessary to this discussion.

23. Sep 10, 2009

### Hurkyl

Staff Emeritus
How do we know that's a theorem? Give a formal proof of it.

Universal elimination only lets us eliminate one variable -- so you applied it wrong, your proof is invalid.

Hrm. How can I tell if you applied biconditional Elimination correctly? Give a formal proof, so I can eliminate all doubt.

There aren't any p's there; your proof is invalid.

And besides, two column proofs are only for high school geometry -- that's not how you're supposed to write a formal proof.

24. Sep 10, 2009

### Hurkyl

Staff Emeritus
All right, now that that amusing exercise is out of the way....

No, it is not. All evidence points to you asking Halls to write a proof so you can say "haha, that's not a formal proof, try again."

If, despite evidence to the contrary, you really and truly are interested in reviewing formal proofs for the purposes of mechanically checking their validity then I strongly suggest three things:
(1) You work on your people skills
(2) You explicitly state your intent, and do your share of the work (e.g. explicitly set up the framework you want to use, and only ask for proofs of things you truly are unable to manage yourself, or otherwise seek out volunteers to participate in your project)
(3) You seek out projects specifically designed for this purpose, such as the Mizar system.​

25. Sep 10, 2009

### CRGreathouse

I'll stump for Metamath, myself; it's an excellent system at exactly the level of detail evagelos seems to want. While I'm at it I'll mention my recently updated Greasemonkey script for Metamath.