[ Readings ] [ Synopsis ] [ Grading ]


There is no required text. We will use Semantic Tableaux so the texts below have been selected because they emphasize this method. I strongly recommend any of the three supplemental texts. Raymond Smullyan's texts are the best treatment of the subject. Alternatively, the first four chapters of Simpson's course notes are an excellent introduction to tableaux in propositional and first-order logic.

Supplemental Texts
  1. Raymond Smullyan, First-Order Logic.
  2. Raymond Smullyan, Logical Labyrinths
  3. Stephen Simpson, Course Notes for Mathematical Logic
The following texts use semantic tableaux as a basis for automated reasoning. If you are interested in these applications, the following texts provide a very good alternative.
Alternative Texts
  1. Mordechai Ben-Ari, Mathematical Logic for Computer Science.
  2. Melvin Fitting, First-Order Logic and Theorem Proving
  3. Jean Gallier, Logic for Computer Science
  4. Anil Nerode and Richard Shore, Logic for Applications


Formal logic is concerned with the systematic study of the principles of valid inference. There is a broad audience interested in the methods of formal logic: philosophers, computer scientists and mathematicians. This course is intended to be broad, elementary and rigorous. Our aim is to study the relationship between truth and proof in propositional logic and first-order logic. We deal with the mathematical foundations of these formal systems in several stages:

  1. Syntax
  2. Semantics, the appropriate notions of truth in an interpretation, validity and consequence
  3. Proof, formal methods of deduction and inference. Our primary proof system is semantic tableaux, but we will consider other proof systems as well.
  4. The fundamental theorems connecting proof and truth: soundness, completeness and compactness. Our focus will be to develop general methods for establishing these properties.
The primary proof method used in this course will be the method of semantic tableaux, developed by Raymond Smullyan in the 1960's but with roots extending back to Gentzen's work in the 1930's. The tableaux method is the easist proof method to learn and use. The method seeks to find a proof of a statement by the systematic search for a counterexample. If the method fails to produce a counterexample, then the statement is proven; otherwise the method will produce a counterexample to the validity of the statement The semantic tableaux method provides the clearest and most direct route to understanding the relationship between proof and truth as captured in the soundness and completeness theorem. The method also provides a foundation for many other proof techniques of interest to philosophers, computer scientists and mathematicians: axiomatic proof systems, systems of natural deduction, the Gentzen sequent calculus and resolution. We will also present a natural deduction system since it follows quite closely the deduction techniques found in mathematics.

As time permits, we will prove the Craig Interpolation Theorem, Robinson Consistency Theorem and Beth Definability Theorem for first-order logic. These are not usually presented in an introductory mathematical course, but their proofs are elementary using the method of tableaux.


The following components will determine the final grade.

Total points: 600 points.
  • Homework: 250 points (five assignments).
  • First Midterm Exam: 100 points. (October 23, covering propositional logic)
  • Second Midterm Exam: 100 points.(November 20, covering first-order logic)
  • Final Exam: 150 points.
The midterms will be held in class. The final exam will be a take home exam.