Thread: proofs about countable sets

Hello

I have some questions about proofs presented while proving that some set is
countable. In Velleman's "How to prove it" , author is trying to prove that there is
a bijection from to
. He gives the arrangement as shown in the attached figure and then also gives the formula for that arrangement.



and then he asks the reader to show that the above function is indeed a bijection
between the said sets. But I have seen the arguments where people just give the
triangular arrangement as shown in the figure and argue that the arrangement is
one to one and onto between to
. The wikipedia article on "countable set" has such arguments. My question is , are these valid arguments ? Velleman's way of reasoning seems more rigorous to me. We need to come up with some functional
form of the given arrangement and then prove using usual methods that its a
bijection. Please comment and move this thread to sub forum where its appropriate.

Thanks

Originally Posted by issacnewton

Hello

I have some questions about proofs presented while proving that some set is
countable. In Velleman's "How to prove it" , author is trying to prove that there is
a bijection from to
. He gives the arrangement as shown in the attached figure and then also gives the formula for that arrangement.



and then he asks the reader to show that the above function is indeed a bijection
between the said sets. But I have seen the arguments where people just give the
triangular arrangement as shown in the figure and argue that the arrangement is
one to one and onto between to
. The wikipedia article on "countable set" has such arguments. My question is , are these valid arguments ? Velleman's way of reasoning seems more rigorous to me. We need to come up with some functional
form of the given arrangement and then prove using usual methods that its a
bijection. Please comment and move this thread to sub forum where its appropriate.

Thanks

It depends on what you think a proof is. Virtually no proof you will have seen is rigorous in the sense that it is machine verifiable.

If you think an proof is a argument that would convince nearly all mathematicians (in the sense that they would believe they could construct a proof that would satisfy their standard of proof using the idea) then the diagram in figure 2 might well suffice (though there will always be some who disagree).

That is; most proofs are informal on some level, what is an acceptable level varies between contexts and individuals.

CB

So is there no standard of what proof is ? I do find the argument using that arrangement in Fig 2 convincing but are there mathematicians who refuse to accept it ?

Are mathematicians supposed to come up with machine verifiable proofs ?

Originally Posted by issacnewton

Are mathematicians supposed to come up with machine verifiable proofs ?

Absolutely not
I have followed all of these posts.
I have looked into the Velleman text.
I must tell you that after teaching the foundations text material for more that thirty years, that text is the poorest I have ever reviewed( that is more the fifty in print)
Look at that function that you posted, Velleman is a sadist.
There are two standard ways of doing the question.
1) Let can be shown to be a bijection.
OR
2) Notice that is a injection.

DO NOT, make more of a problem that is called for!

The last chapter (chapter 7) in Velleman's "How to prove it" is pretty difficult for someone (that's me )who has done every single problem in first 6 chapters. He should make the transition more smooth.

Plato, thanks for the input. Since you have reviewed so many foundational texts, which one would you suggest after I finish Velleman's "How to prove it".

In regard to this specific proof, what Velleman does is show that there is a bijection from to an infinite subset of rather than getting a bijection to itself. However, since every infinite subset of is countable, that is sufficient to show that is countable.

Originally Posted by HallsofIvy

In regard to this specific proof, what Velleman does is show that there is a bijection from to an infinite subset of rather than getting a bijection to itself.

Well, I think he is showing the bijection from to if we look at the Fig 2 and the function given.

Originally Posted by issacnewton

So is there no standard of what proof is ?

Yes, there is. Mathematical logic gives a precise definition of a proof. Such definitions have been implemented on computers, and one can construct a completely formal proof of the fact above where every inference rule is verified by the computer.

People, though, have very powerful intuition when it comes to finite sets and sequences of objects. Relying on it is often more convincing than on written formulas. After a certain point, too much detail makes a proof more difficult to understand.

The level of details appropriate in a proof depends on the area and audience: e.g., textbooks have to be much more detailed than conference articles.

Originally Posted by issacnewton

Are mathematicians supposed to come up with machine verifiable proofs?

Absolutely yes! I am somewhat kidding, but the dream of the formal methods community is to reduce the difficulty of proof formalization (the possibility to formalize any proof is already there). Even though explaining a proof to a computer will probably generally remain more difficult than writing a paper proof, the hope is that mathematicians will want to formalize their proofs to avoid errors and get help with difficult calculations, and conference program committees will encourage formalized submissions to cut time on checking.

By the way, to understand the relationship between the formula and the figure in the OP you may consider this thread.

emakarov,

In Velleman's book, in the earlier chapters, he asks readers to present proofs
using some software which is there on his website. These proofs are regarding set theorems , so they are easy to put in formal language. And its good that there
are efforts going on to make formalized proofs easier, as that will definitely save lot of
time .............