Formal models of knowledge and belief have been used by a wide range of communities including computer scientists, economists and philosophers. One important challenge is to determine to what extent these formal models represent the social situations that they are intended to model. With this challenge in mind, we will survey the main approaches to formalizing social interactive situations from the computer science, game-theoretic and philosophical literature. This includes both probabilistic models (such as Harsanyi type spaces) and non-probabilistic models (such as Kripke structures and Aumann structures). We will then discuss some of the key theorems (such as Aumann's agreement theorem and related results) and conceptual puzzles. An important part of the course will be a thorough presentation of common knowledge and related concepts as well as a discussion of applications in game theory