Michigan State University
Michigan State University
Department of Philosophy
PHL 432 Logic and its Metatheory FS 2019
Home > Courses > Course Descriptions > PHL 432 Logic and its Metatheory FS 2019


This course is a rigorous introduction to logical consequence, the central concept of logic. The primary aim of logic is to tell us what follows logically from what. We shall take logical consequence to be a relation between a given set of sentences and the sentences that logically follow from that set. A central question of the course is: what conditions must be met in order for a sentence to be a logical consequence of others?

In response, we shall develop an account of logical consequence for a symbolic language (specifically, a first- order language (FOL)). This will allow us to investigate formal methods of proof for determining when one FOL sentence follows from others, and will allow us to develop a method for showing that an FOL sentence is not a consequence of others. After becoming familiar with formal and informal methods of proofs of logical consequence, we shall study applications of formal methods of proof in the context of the axiomatic method. Students will be introduced to axiomatizations of Zermelo-Frankel set theory and of natural number theory (Peano Arithmetic). We’ll spend time using the formal proof techniques we’ve learned to derive theorems from the axioms of Zermelo-Frankel set theory and the axioms of Peano arithmetic. Along the way we learn about Russell’s paradox and about a very powerful rule of inference called the principle of mathematical induction. An inherent limitation with the axiomatic method will be highlighted when we come to Gödel's Incompleteness theorems at the end of the course.

The “metatheory” part of PHL 432 concerns historically significant proofs regarding the formal methods we use to determine logical consequence. To understand the proofs, we develop a model-theoretic definition of logical consequence, which is a mathematical characterization of the informal notion of logical consequence that we work with during the first half of semester. Then we shall prove that Fitch, our formal method of proof, is sound. That is, we shall prove that if there is a Fitch-proof of a sentence X from a class K of sentences, then X is a model-theoretic consequence of K. We also prove the Completeness Theorem for Fitch (i.e., we prove that if X is a model-theoretic consequence of K, then there exists a constructible Fitch proof of X from K). The soundness and completeness proofs will offer an enlightening (meta-) perspective on the nature of formal proof, logical consequence, and their relationship. After proving the Completeness Theorem for Fitch, we draw two well-known consequences: the Löwenheim-Skolem Theorem and the Compactness Theorem. These are discussed and applied. The course concludes with a sketch of Gödel's Incompleteness Theorems.

Instructor: Matt McKeon

Other Relevant Majors: Mathematics, Computer Science

Possible Texts: Language, Proof and Logic