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, predicates, 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

The first three weeks focus on propositional logic (PL), and correspond to Chapter 1 of Enderton. This part of the course is essentially a warm-up for the second part, since it asks the same questions about PL that are later asked about FOL. (The questions are much easier in the propositional case.) The results from this part are also needed mathematically, since some of the proofs for FOL assume the corresponding results for PL (PL essentially being a subset of FOL).

The syntax and sematics of PL are both defined rigorously. Analyzing the syntax requires showing that every PL formula has a unique parse tree. The semantics of first-order sentences is defined in terms of truth conditions, or mappings from truth assignments to truth values. (These mappings can be represented as truth tables). Defining the semantics requires two mathematical results which allow one to formulate and reason about recursive definitions: structural induction, and the Recursion Theorem. An important result is that PL is complete, in the sense that any truth condition can be represented with some sentence in PL.

One important result about PL is that consistency is decidable: there is a computational procedure which always halts, and which correctly determines if a set of statements is consistent. Another result is the compactness of PL: given any (potentially infinite) set of sentences S, if S is contradictory, then some finite subset of S is contradictory.

Weeks 4-9: first-order logic

The rest of the course analyzes FOL, starting with rigorous definitions of the syntax and semantics. For the syntax, just as in the propositional case, one needs to show that every sentence has a unique parse tree. Furthermore, one can define a deductive calculus, or formal proof system, for FOL. Even though each of the allowed proof steps is justified intuitively in terms of the semantics, the mathematical definition is purely syntactic. This is important, as one would like the proofs to be checkable by a relatively simple automated procedure.

The semantics of FOL is defined in terms of possible worlds. More precisely, a first-order structure consists of a collection of things, together with sets corresponding to the functions and predicates of the language. One defines the semantics of FOL by defining the truth or falsehood of a sentence of FOL, evaluated on any particular structure.

The syntax and semantics of FOL give two different ways in which a set of hypotheses S can imply a conclusion T:

  • The syntactic notion: there is some formal proof which assumes S and proves T
  • The semantic notion: S logically implies T if any first-order structure satisfying S must also satisfy T

The most basic requirement is soundness: if you can prove T from S, then S had better logically imply T. Fortunately, this can be proved of the deductive system used in this course.

What about the other direction? Godel's Completeness Theorem is a powerful result showing that any semantic entailment can be proved. More precisely, either there is a proof of T starting from S, or there is some first-order structure which satisfies S but doesn't satisfy T. Together with soundness, this result shows that the semantic and syntactic notions given above are equivalent.

The rest of the course then focuses on some interesting consequences of Godel's Completeness Theorem:

  • The consistency of a set S of FOL sentences is semi-decidable, in that there exists a computational procedure which halts if S is inconsistent, but doesn't halt otherwise. (In particular, it exhaustively enumerates all strings, and halts as soon as it encounters a proof of contradiction starting from S.) This is in contrast with PL, which is actually decidable.
  • FOL is compact, meaning that if a set S of FOL sentences is inconsistent, then there is a finite subset of S which is inconsistent. (This results from the fact that a proof of contradiction can have only finitely many steps.) This allows us, for instance, to extend a proof of the Four Color Theorem for finite maps to the case of infinite maps. It also lets us define nonstandard analysis, a rigorous notion of infinitesimals in calculus.
  • The Lowenheim-Skolem Theorems show that if a first-order theory with a finite alphabet has an infinite model, then it has models of all infinite cardinalities. This leads to a number of bizarre results: one one hand, the Peano axioms (which define the natural numbers) must have an uncountable model. On the other hand, the Zermelo-Frankl axioms of set theory must have a countable model, despite the fact that Z-F can express Cantor's diagonalization argument, which proves the existence of uncountable sets! Both of these results hint at inherent limits in our ability to formalize mathematical theories.