[Book] Mathematical Proof

[phantomotap]

Can someone with a strong background in mathematics recommend a good book examining formal proofs with breakdown and explanation? Something like/the equivalent of "3000 Solved Problems in Calculus"?

One of the young programmers I work with wants to learn the "grit" behind formal proofs. I'm not nearly as experienced with mathematics as I am with programming. My explanations are all visual demonstrations. The demonstrations are apparently not very satisfying.

*shrug*

I usually just assume the mathematicians know what they are talking about.

[Edit]
Sorry. Feel free to move this around...
[/Edit]

Soma

[bernt]

If you're looking for an intro to formal proofs, this is pretty good.
There's another one here, it looks much more complex but the only major difference is the use of notation (on the other hand it may be useful if you plan on reading other people's proofs).

wants to learn the "grit" behind formal proofs

The grit is usually nothing more than algebra. Sure, you can learn techniques for constructing proofs, but it [almost] always comes back to algebra in the end.*

I guess the thing to brush up on is your theorems, since those are the real "meat and potatoes" of a proof. All that's left to do is string them together, like writing a computer program, so that you get the right output for whatever input you put in. Unfortunately most are named after their discoverers and not their content so it's difficult to find the right one.

*I say almost because geometric proofs like the one for the Pythagorean theorem are out there and I'd hate to take away from the validity of those.

[Mad_guy]

You want something like a good course in First-Order Logic. You can use FOL to prove the completeness and soundness of certain axiomatic systems, such as Zermelo-Frankel set theory (a.k.a. ZFC,) which is commonly known as the 'foundation of mathematics.' FOL is a great tool for understanding what exactly a 'proof' and a proposition are and has very deep implications all throughout mathematics and even computer programming.

It turns out through said very deep implications, logical systems like First-Order Logic are in fact directly isomorphic to certain classes of programming languages (ones which are based on what we call the 'lambda calculus,') this is called the 'Curry-Howard Correspondence'. What's significant about this is that it creates a direct link between two seemingly completely unrelated things: proofs, and programs. I'll get back to this in a second.

The best book I know of on the subject is the Handbook of Practical Logic and Automated Reasoning. You can find a description here: Handbook of Practical Logic and Automated Reasoning - Cambridge University Press

The book primarily takes you through the steps of doing Propositional and First-Order logic (first order logic = propositional logic + quantifiers.) It's primary, overall focus is the practice of automated reasoning and interactive theorem proving, that is, using mechanized computer tools to reason about and prove formally properties about both mathematics, as well as computer programs. It turns out through the aforementioned Curry-Howard correspondence, that you get a *lot* of nice things by doing this, depending on where you come from. Namely, because it states that programs are actually proofs of propositions, it allows you to state propositions and proofs in 1 language, using code. Many theorem provers then will allow you to extract real, executable code from that proof and proposition, in effect giving you a formally mechanized computer program! They say there is no such thing as bug-free code, but there really is, and this is how you do that.

I would like to highlight that I'm suggesting an interactive, computer based theorem prover for learning things like this because they have many tools which make reasoning about proofs and working with them much easier than on paper. A benefit of this - like any programming language - is that many people have used this tools and in effect, written libraries for them, providing certain other proofs for different things. In the same way you wouldn't write a linear algebra library, with these tools, you don't need to show that the equivalence relation '=' (equals) is transitive. Someone else has already proved that and it's in a library - you can just use it. In effect, by treating proofs like code, you get a lot of reusability.

If you don't have any experience in any sort of formal logic, I would recommend you first start with a book like Harrison's and go through first-order logic, doing things on paper to get a feel for how a proof is supposed to be carried out. After this, you can use an interactive theorem prover to do a lot more heavy lifting (protip: you *can* just read Harrison's book, because through the entire book he steps through the process of building your own theorem prover basically); I say this because if you don't really know how a basic proof is carried out traditionally, the interface will probably seem very obtuse to you. After the fact it will make much more sense.

Once you get to the point of using tools, there are a good amount of choices out there, in particular, look into 'HOL Light', 'Coq' and 'Isabelle'. They are very popular theorem provers for proving mathematical properties and programs and extracting code from your proof. Most attention these days go towards Coq, as it is both a theorem prover, and a programming language, and has a highly advanced basis for a programming language (a variant of the lambda calculus we call 'Dependently typed,') and it has an extremely large library of proofs for things like geometry and algebra, etc..

Feel free to ask questions if this is a bit confusing - proofs and logics aren't really hard, they just take some time to warm up to.