This was something that I had to stop reading because of the exam season, and finally finished within 24 hrs of the exam getting over.
It is a rightly acknowledged classic in the field of popular mathematics (Stuff which makes abstruse mathematical ideas accessible to the (almost) general public).
It was believed that given a finite set of axioms and a set of rules to operate on them, one can mindlessly manipulate symbols to generate every known theorem. A simple example would be translating geometry into algebra ( is how a circle would look in algebraic terms ). So, we can say that if algebra is consistent, then geometry is consistent.
Hilbert developed a method to provide proofs of consistency, which was then taken over by the logicians of the time to try and provide similar proofs to certain parts and eventually all of mathematics.
That is, until Godel came along. How he did it is explained beautifully in the book and is unecessary to reproduce here. Godel proved that any system for number theory that is consistent is incomplete, i.e, you can produce a true theorem which cannot be proved within the system. Thus, we cannot have a formal system describing all of mathematics. We can have formal systems with finite set of axioms, but not for something like number theory, where Godel proved it was impossible to generate a finite set of axioms.
The book also has a section on the philosophical implications of this proof, which essentially says that present day A.I is a far cry from imitating the human brain, and unless we can actually describe the human brain as a logical system with a finite set of axioms.
There are many approaches to imitate human intelligence, like neural networks, but they run on a system with a very limited set of axioms and rules of inference commonly known as a digital computer. Maybe we need some new kind of ‘computer’. Researchers have a lot of work to do!!
Simply, a must read.