This course serves as a graduate-level introduction to important topics in the Foundations of Mathematics. The first part covers the basics of Model Theory, including topics such as existentially closed structures, quantifier elimination, ultraproducts, types, and indiscernibles. The remainder concerns intuitionistic logic and its semantics, including a discussion of the simply-typed lambda calculus and the Curry-Howard correspondence, as well as completeness of both the Heyting and Kripke semantics.