Synopsis This book addresses problem like: Can we prove all that is true? Can symbolic manipulation capture everything? Is there a general method to solve a class of solvable problems? Is mathematics contradictory? To answer these fundamental questions, it comes up with results such as Deduction, reductio ad absurdum, Monotonicity. Compactness, Completeness, Undecidability and Incompleteness as expounded in the works of Herbrand, Godel, Skolem, Lowenheim, Beth, Tarski, Post, Turing and others. It deals with the logics of sentences and predicates as formal languages giving stress on formal languages giving stress on formal semantics. It considers major styles of presenting these logics such as axiomatics, Gentzen systems, analytic tableaux, resolution refutation as various proof techniques. However it requires nothing from the reader but a mere willingness to remain logical and have a fearless attitude towards precise use of symbols.