Proof of ΦxΦ = Φ and the special case of \emptyset\times\emptyset =\emptyset

[evagelos]

Prove:

\emptyset\times\emptyset =\emptyset

 

[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.

 

[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.

 

[evagelos]

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.

Wrong, no theorem to base your contradiction.

 

[jgens]

Wrong, no theorem to base your contradiction.

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?

 

[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.

 

[Hurkyl]

Wrong, no theorem to base your contradiction.

HoI's statement is a theorem.

 

[statdad]

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

 

[techmologist]

Wrong, no theorem to base your contradiction.

HoI's statement is a theorem.

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.

 

[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

 

[evagelos]

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.

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

 

[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?

 

[CRGreathouse]

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

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.

 

[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).

 

[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".

 

[CompuChip]

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

 

[Preno]

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

 

[evagelos]

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".

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

 

[statdad]

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.

 

[CRGreathouse]

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

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

 

[evagelos]

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.

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.

 

[statdad]

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.

 

[Hurkyl]

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

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

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

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

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

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

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

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.

 

[Hurkyl]

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

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 .

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.​

 

[CRGreathouse]

(3) You seek out projects specifically designed for this purpose, such as the Mizar system.[/indent]

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.

 

[evagelos]

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



Universal elimination only let's 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.

IF this is not nonsenses what is it ??

If i were you i would open a book in logic and look at least what a formal proof look like never mind study it.

All evidence now points to you trying to make ridicule of other peoples writing using unfounded nonsenses,and so making a ridicule of your self

if you have the guts and the nerve leave this post to exist as an answer to your posts

and use your worthless power to ban me instead of my post, because that was what always you had in mind since you could not and will not ever be able to write a single formal proof.

I challenge you on that.

And remember i am not the one who discover formal proof .

So all accusations and nasty remarks about formal proofs are against those brilliant men who formulated the concept.

 

[HallsofIvy]

I don't believe that anyone has said any thing "nasty" about formal proofs. The only point I wanted to make is that "formal proofs" are overkill for general mathematics problems.

 

[statdad]

evagelos, I suggest you go back and read my post at 22: if you read it carefully, and honestly, you won't find any "disparaging" of formal proofs. You will find my explanation about why, in the current context, the purely formal approach is neither required nor the best possible.

 

[Hurkyl]

IF this is not nonsenses what is it ??

It is nonsense, and that's the point -- you would never see such levels of pedantry in a serious mathematical discussion. Mathematical discourse best operates at the level of precision needed to efficiently convey information, and at the level of abstraction needed to brush aside irrelevant details.


On the other hand, if you were truly interested in explicit formal proofs, then this level of pedantry is important -- if you get a little detail wrong, it is not a valid formal proof.

My specific objections were chosen to illustrate a point: there isn't a One True Formal System. There are lots of choices, each with their own grammar for statements, grammar for proofs, rules of inference, and axioms. Without explicitly specifying the system, one cannot deal explicitly with a formal proof.

It's a trivial exercise to find, e.g., a set of rules of deduction where substitution is allowed only for one variable at a time, or a grammar where proofs are sequences of logical statements. (in particular, they do not state exactly how to infer each statement from previous ones)

(in particular, it seems relatively uncommon for formal systems to have their proofs include what rule is used at each step -- instead, proofs consist merely of a sequence of statements, and its the job of a verifier to figure out which rule is used)


Now, none of the above has anything to do with why you have been given infractions. There have been many occasions where you have shown no apparent interest in learning or understanding anything, but instead seem interested only in berating people who don't hand you on a silver platter an complete answer in exactly the particular form you want (but have never stated).

This is your last warning.

 

[Tobias Funke]

That must have been his 508th warning since every single thread he makes is the same. Is there a tediouslogicforums.com?