Book of Proof – An introduction to the methods of proving mathematical theorems
people.vcu.edu
people.vcu.edu
It is readable enough that there is a danger that a reader might read it from cover to cover and believe that they now understand it all. But like programming, mathematics is not a spectator sport - you need to engage it in hand-to-hand contact to get the most out of it.
Reading a book about programming without trying to write programs leaves you with only a superficial understanding, and potentially no extra ability. However, reading a book about programming and writing programs is immensely valuable. And so it is with proofs, and mathematics in general.
So don't just idly read this book and believe you now understand proofs - engage with it. Try to find errors in it, do the exercises, go back and re-read - you will get more the second time through. And based on the quick dips I've had, it will be worth it.
Does anyone know how much of this "Book of Proof" would require re-write to handle Common Logic ?
If you are referring to translating the book's theorems for an automated theorem prover, the book is not nearly pedantic enough to effectively do this from the ground up.
Set theory is a reductionistic system. It's supposed to give a foundation which is as "small" as possible. In set theory you start with almost nothing and you have to encode all useful concepts into sets before you can start proving/programming.
Compare this to Turing machines, where you start with a very primitive model of computation. The first step in most treatments of Turing machines is similar to set theory, you show that some useful concepts (associative memory, high-level control flow, etc.) can be encoded into Turing machines. You then use this encoding to construct arbitrary programs.
Type theory starts out with a functional programming language and you derive new concepts from free constructions. In type theory you shouldn't be encoding things at all. You should be describing concepts (~adding an API) and possibly extending your model (~the compiler).
As analogies go, I'd say that this one is pretty accurate.
There's a lot of mathematics which can't be formalized in classical first-order logic with the ZFC axioms. For most things you can get around this by adding enough Grothendieck universes, but this is still incomplete and always will be.