This course follows up on the content of the undergraduate courses II Logic & Set Theory and II Automata & Formal Languages and introduces students to three important fields in Foundations: proof theory, model theory, and computability theory.  Topics include the syntax and semantics of intuitionistic propositional and first-order logic, the untyped and simply typed lambda-calculus, the Curry-Howard correspondence, ultraproducts, model-theoretic types and indiscernibles, relative computability, and Tennenbaum's Theorem.