Quantifiers in lambda calculus

I'm learning lambda calculus, however I'm quite confused about the quantifiers in lambda calculus. As far as I know, quantifiers such as "∃" are concepts of first order logic (FOL), which are not needed by lambda calculus. Moreover, I didn't find anything about quantifiers in any tutorials I have read.

However, I find this paper (Lambda Dependency-Based Compositional Semantics), in the first page of which the author used quantifier in lambda calculus.

So, are quantifiers used in lambda calculus? If so, what do they mean? Is it the same as in FOL?

Precisely, what does "∃" mean in the following lambda calculus?

λx.∃e.PlacesLived(x, e) ∧ Location(e, Seattle)

There is no notion of quantification in the standard $\lambda$-calculus as introduced by Church. As far as I can tell from Liang's paper, it deals with a specialized version of $\lambda$-calculus in which $\lambda$-expressions can be logical expressions containing quantifiers and logical connectives. This approach is meant as a way of formally representing natural language statements. Thus, we are really dealing with an applied $\lambda$-calculus with function symbols that correspond to logical connectives and function symbols and are to be interpreted in this way.

StackExchange Computer Science Q#64824, answer score: 5