Formal logic aims at developing techniques for evaluating logical consequence and consistency. It originated in the ancient world with Aristotle who developed techniques for evaluating a limited range of quantified inferences (inferences that use quantifiers such as ‘all’, ‘some’, and ‘none’). The Stoics independently developed formal techniques for evaluating inferences with sentential operators such as ‘and’, ‘or’, and ‘if… then…’ For thousands of years philosophers wondered how the two sets of techniques, and the various schemas and logical rules-of-thumb that had accumulated over the ages, might fit together in a single system. They wondered, moreover, whether such a system would be powerful enough to enable them to evaluate inferences such as “Every horse is a mammal; therefore, every head of a horse is the head of a mammal” – inferences which they felt certain must be valid, but whose validity couldn’t be represented using any of the available schemas or rules. The breakthrough finally came in the late-19th Century with the pioneering work of Gottlob Frege. He made it evident how the quantified inferences studied by Aristotle and the sentential inferences studied by the Stoics could be fit into a single overarching system with the power to represent and test the validity of literally an infinite number of inferences. The upshot was an unprecedented expansion in the scope and power of formal techniques. These are the techniques students learn in this course. They learn to represent natural-language sentences in formal languages such as sentential logic and first-order predicate logic, and then learn to evaluate inferences and construct proofs using a variety of methods including truth tables, truth trees, and a system of natural deduction. If time permits they might also learn a system of intensional logic such as modal logic, or explore some of the philosophical issues surrounding the use of formal systems.