[Phil 151, First-Order Logic](http://web.pacuit.org/classes/phil151winter09.html), is the second term of Stanford's undergraduate logic sequence. [First-order logic (FOL)](first_order_logic) 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](https://symsys.stanford.edu/) 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](http://www.amazon.com/Mathematical-Introduction-Logic-Second-Edition/dp/0122384520).
  
  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](propositional_logic) and [first-order logic](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](propositional_proofs) (in some formal system). 
  
  It also assumes knowledge of a few concepts in set theory:
  
- * basic [operations on sets](operations_on_sets)
+ * basic [operations on sets](set_operations)
  * how to [represent functions and relations as sets](functions_and_relations_as_sets)
  * the distinction between [countable and uncountable sets](countable_sets)
  * [Russell's Paradox](russells_paradox), and why it justifies the need for a system of axioms for set theory (e.g. the [Zermelo-Frankl axioms](zermelo_frankl_axioms)).
  
  Finally, it requires a certain level of comfort with several mathematical proof strategies: [direct proof](http://en.wikipedia.org/wiki/Direct_proof), [proof by contradiction](http://en.wikipedia.org/wiki/Proof_by_contradiction), and [mathematical induction](http://en.wikipedia.org/wiki/Mathematical_induction).
  
  
  
  ## Weeks 1-3: propositional logic
  
+ The first three weeks focus on [propositional logic (PL)](propositional_logic), 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 mappings from truth assignments to truth values (intuitively, [truth tables](http://en.wikipedia.org/wiki/Truth_table)). Defining the semantics requires some mathematical results which allow one to make recursive definitions: [structural induction](structural_induction), and the [Recursion Theorem](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.
+ 
+ Another important result from this part of the course is the [compactness of PL](compactness_of_propositional_logic): 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
+ 
+ 
+