Introductory semantics textbooks generally fall into three categories: empirically-driven; philosophically-driven; and formally-driven. Yoad Winter’s very careful and thorough new book, *Elements of Formal Semantics*, falls into the latter category, making it a welcome and accessible successor to Allwood, Andersson, and Dahl’s (**1977**) *Logic in linguistics* and L.T.F. Gamut’s (**1991**) *Logic, language, and meaning*.

*Elements of formal semantics* (henceforth *EFS*) is published in a series geared towards “the later years of undergraduate study” but it is additionally quite suitable for two other populations: undergraduates with strong formal backgrounds interested in learning about basic linguistic semantics (students “of relevant undergraduate courses in artificial intelligence, computer science, cognitive science and philosophy,” **Winter 2016: 7**); and beginner graduate students (perhaps alongside supplemental, empirically-driven texts).

*EFS* divides naturally into two parts. The first part addresses, quite efficiently, the standard underpinnings of Montague Grammar: set theory and model theory (Chapter 2), type logic and lambda calculus (Chapter 3), and Generalized Quantifier Theory (Chapter 4). The second part consists of useful extensions of this formal foundation, in particular a directly compositional treatment of relative clauses and other long-distance dependencies (Chapter 5), and a possible-worlds semantics for intensional expressions (Chapter 6).

*EFS* has several notable assets: it is formally careful and deliberate, as thorough as any logic textbook; it has a lot of varied and well-thought-out exercises (including practice exercises with solutions); a Conclusions chapter containing references on a number of phenomena (adjectives, definiteness, plurality, tense and aspect) students can extend the formal foundation to; and, at the end of each chapter, a Further Reading section that cites innovative, contemporary research articles as well as historical sources and other textbooks. As a result, it is a very versatile book, useful as a primary textbook, as a secondary textbook for more advanced or formally inclined students, or as a source of supplementary formal definitions and exercises.

The first four chapters of *EFS* cover roughly the same content as the first seven chapters of the familiar *Semantics in generative grammar* (henceforth *SGG*) by Heim and Kratzer (**1993**), and a direct comparison is useful for illustrating the unique contribution of the former. Both cover, in the same order: set theory; characteristic functions of sets; type logic; lambda calculus; and the semantics of quantifiers. *SGG* concentrates on the empirical motivation for each formal innovation, as well as creating a semantic theory that conforms to movement-based theories of syntax (introducing, famously, a semantics of traces and moved operators). But it does so at the cost of a thorough formal introduction: many teachers, including myself, have supplemented the text with their own inventory of metalanguage definitions and rules (e.g. a rule for beta-reduction in the lambda calculus) to allow students to perform the requested proofs in a principled way.

In contrast, *EFS* introduces its formalism (as well as its terms and notational conventions) impeccably carefully, in the tradition of logic textbooks, in a way that allows for more clear, thorough, and easy-to-follow exercises, and for students to more easily extend the formalism on their own to related phenomena if they choose to. Relations of type are, for instance, motivated formally (as a natural byproduct of the logic) instead of empirically (i.e. as needed for the treatment of transitive verbs). It accomplishes this, however, at the cost of some of the empirical motivation many linguistics students may be accustomed to, and it takes for granted that its readers know how to use a metalanguage and construct a proof.

Another notable difference is that *EFS* doesn’t rely on any particular syntactic assumptions to treat these issues (although it does presuppose that its readers are familiar with constituency and tree diagrams). Instead of a treatment of moved operators (e.g. the Predicate Abstraction Rule in *SGG*), then, *EFS* introduces ‘currying’ (**Winter 2016: 57**) and type lifting (**Winter 2016: 129**), instruments that are refined in Chapter 5. And instead of assimilating the treatment of reflexives with traces and pronouns, as in *SGG, EFS* gives them a directly compositional variable-free treatment (**Winter 2016: 70**), inspired by Pauline Jacobson’s work. These chapters additionally include a nice discussion of the difference between attributive and predicative adjectives on the one hand and intersective and subsective adjectives on the other; and of the properties of monotonicity and conservativity that are familiar from Generalized Quantifier Theory.

The second part of *EFS* turns to extensions of the formal foundation in this similarly precise, efficient, and directly compositional way. Chapter 5 introduces the Lambek-Van Bentham Calculus and treats relative clauses using a careful and intuitive explication of abstract types and function introduction. The contents of this chapter are the least standard of the book, but its discussion is so careful that it will be a useful exercise for even the most pro-movement of students, especially when viewed in contrast to the treatment of relative clauses in *SGG*. It can, at the very least, be read independently from the other chapters.

Chapter 6 is the most empirically rich chapter in the book, and is a nice combination of the motivating discussion of possible-world semantics in Allwood, Andersson and Dahl’s *Logic in linguistics* and the modern, lambda-calculus introduction to intensional semantics in von Fintel and Heim’s (**2011**) *Intensional semantics* lecture notes. Most notably, it contains an explicit model-theoretic discussion of intensions, and a very clear and theory-neutral explication of “The Quine-Montague Hypothesis,” alleging that *de dicto/de re* ambiguities can be treated by the same mechanisms as scope ambiguity.

Students who are new to semantics tend to come in two varieties: those who have formal backgrounds, but little knowledge of syntax or linguistic methodology generally; and those who know linguistics, but have little experience with logics or formal systems. *EFS* is a great gift to the former, in the way that Heim and Kratzer’s *Semantics in generative grammar* has been helpful to the latter. I believe that many teachers and students will benefit from a careful balance of both approaches, at both the undergraduate and graduate levels.