Stanford Phil 151: First-Order Logic

Created by: Roger Grosse
Intended for: Phil 151 students, anyone interested in logic

Phil 151, First-Order Logic, is the second term of Stanford's undergraduate logic sequence. First-order logic (FOL) refers to a logical system which includes the propositional connectives, variables, functions, relations, and quantifiers. In a sense, FOL is powerful enough to describe all of mathematics, yet its syntax and semantics can be defined precisely enough to say quite a lot about it.

While the course is listed in the philosophy department, it's really more like a math course. It formally defines the syntax and semantics of FOL, and most of the class is concerned with proving things about the logical system itself. It's a required course for the symbolic systems major, and has a reputation as a weeder course because, for a lot of students, it is their first course that requires writing rigorous mathematical proofs. The class roughly follows the first two chapters of Enderton's A Mathematical Introduction to Logic.

This roadmap roughly corresponds to the course as it was taught in 2005.

Background: logical languages, proof techniques

The course assumes that students are already comfortable working with propositional logic and first-order logic, at the level of understanding what the symbols mean, being able to express statements in those languages, and being able to write formal proofs (in some formal system).

It also assumes knowledge of a few concepts in set theory:

Finally, it requires a certain level of comfort with several mathematical proof strategies: direct proof, proof by contradiction, and mathematical induction.

Weeks 1-3: propositional logic