This course introduces core logical frameworks for the logic of classes, types, and properties, as well as their main application. For example, these logical systems allow us to model inferences such as the one from "That cow is courageous" and "That horse is not courageous" to the conclusion "That cow is something that the horse is not." In particular, the course presents three frameworks for thinking about classes: set theory, second-order logic and type theory. After a main block of ten weeks on these, the class will consider three kinds of application: (1) philosophical applications of higher-order logic in metaphysics; (2) linguistic applications of type theory in semantics; (3) applications of type theory in computer science, with particular attention to the foundations of programming languages. Students will be expected to have rough familiarity with each of these three applications, but to pursue only one in depth according to their background and interests.