In order to understand Montague's method we need to understand lambda abstraction. For the formula A(x) we read the expression λx[A(x)] as a predicate expression. It extension (in a given possible world) is the set of things that satisfy the formula A(x). Lambda abstractors are governed by two rules, known as α-conversion and β-reduction: