Title:  Logic, Algorithms, and Formal Languages
Authors: Richmond Thomason and Jamie Tappenden

Brief Description:  Logic has become the science of formal languages. It tells us how to design these languages and prove their important properties. The traditional use of these languages was to provide an account of valid reasoning in relatively well-behaved reasoning domains, and most especially in mathematics.

The general organization of logic textbooks used in serious introductions to this sort of logic ("symbolic" or "mathematical" logic) has not changed much in over 60 years. These textbooks concentrate on "classical" systems of logic that are recognized as central and important, and provide an introduction to the theory of proofs, of truth in models, and of the connection between the two.

These things are in fact still central to logical theory. But logic has developed and changed in many ways. It is still the science of formal languages, but the uses of formal languages have proliferated enormously, because of the importance of these languages in instructing computers and enabling many tasks to be performed with computers. The internet would be impossible without languages that are designed for storing and presenting information of various kinds, and for enabling computers to communicate.

At the same time, applications have been found for logic that illuminate many aspects of reasoning besides mathematical proofs.

This textbook aims to present the core ideas of logical theory while recognizing these developments. It attempts to provide a foundation for the theory of formalized languages using ideas that have developed in computational courses. The first chapter of the book, for instance, introduces the notion of a data type, which is an important and useful conceptual tool in thinking about formal languages. And the book tries to convey a clear idea of the notion of an algorithm. This idea was central to logic long before the development of digital computers. To understand how symbolic logic deals with proofs, for instance it is crucial to see that there is an algorithm for deciding whether or not a formal object is a proof.

This book takes a more holistic approach to formalization. Formalization is treated not as a matter of translating individual sentences into a logic, but of formalizing entire domains.

The chapters that are available have been revised several times, but some typograpical errors may remain. Chapters 12 ("Formalizing domains with FOL") and 13 ("Advanced topics") are still incomplete and have not been posted as of this date (August, 2011).