Language, Proof and Logic

Language, Proof and Logic covers topics such as the boolean connectives, formal proof techniques, quantifiers, basic set theory, and induction. Advanced chapters include proofs of soundness and completeness for propositional and predicate logic, as well as an accessible sketch of Godel's first incompleteness theorem. The book is appropriate for a wide range of courses, from first logic courses for undergraduates (philosophy, mathematics, and computer science) to a first graduate logic course.

Textbook

Language, Proof, and Logic is a textbook and software package, intended for use in undergraduate level logic courses. The text covers topics such as the boolean connectives, formal proof techniques, quantifiers, basic set theory, and induction. The last few chapters include material on soundness, completeness, and Godel's incompleteness theorems. The book is appropriate for a wide range of courses, from first logic courses for undergraduates (philosophy, mathematics, and computer science) to a first graduate logic course.

Online Course

We constructed an online course based on Language, Proof and Logic courseware package, with lectures by the authors. With more than sixteen hours of video, the course covers the first two parts of Language, Proof and Logic, on propositional and first-order logic. The course is structured like the book, divided into 14 chapters each containing between two and six individual lectures. We recommend studying approximately one chapter per week. You can sign up at Stanford Online to get access to video lectures, quizzes and assignments. Or watch videos on our website.

Software

Language, Proof and Logic contains three logic programs (Boole, Fitch and Tarski's World), and an Internet-based grading service (which is free to students who purchase the package). Tarski's World is a program that teaches the basic first-order language and its semantics; Fitch is a natural deduction proof environment for giving and checking first-order proofs; Boole is a program that facilitates the construction and checking of truth tables and related notions (tautology, tautological consequence, etc.); Submit is a program that allows students to submit exercises done with the above programs to the Grade Grinder, the online grading service.