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)

• Since lambda-calculus doesn't contain "PlacesLived", "$\wedge$" and "Location", it's safe to assume that the author uses some kind of short-hand that might not be properly defined. – adrianN Oct 19 '16 at 10:38
• Agreed with @adrianN — this seems to be some mash-up of Lambda calculus and Prolog/1O logic. – Jules Oct 19 '16 at 15:44

It appears that the author is using lambda notation for sets and relations. That is, sets are represented as boolean-valued unary functions, and relations are represented as boolean-valued binary (or k-ary) functions. In other words, we work with the sets/relations' characteristic functions instead, with no loss of generality.

For instance $\{n | n\geq 5\}$ is written as $\lambda n.\ n\geq 5$ where "$n\geq 5$" must be understood as the boolean $\sf true$ or $\sf false$, depending on the value of $n$.

The existential expression $\exists x.\ p(x)$ must be understood similarly: it "evaluates" to true iff there is some value of $x$ which satisfies $p$.

Also, note that, in the theory of typed lambda calculi, we do have some powerful type systems which allow $\forall/\exists$ to appear. For instance the second-order lambda calculus $\lambda 2$ (AKA System F) allows universals in types. In the very powerful Calculus of Constructions we can indeed write things such as $\lambda x:\tau.\ \exists y:\sigma.\ p x y$ which is a function of type $\tau \rightarrow *$. It takes a value of type $\tau$, and returns an existential type.

You do not need this theory for the paper you mention, though.

• I'm still a little confused. So what is the difference between "λ" and "∃"? It seems that these two are exchangeable. For example, to my understanding, λn. n≥5 and ∃n. n≥5 can both be understood as "the boolean truetrue or falsefalse, depending on the value of n". – Zhao Oct 20 '16 at 2:06
• Consider an applied $\lambda$-calculus with arithmetic expressions. Here you can write e.g. $\lambda x. x +3$; the variables bound by $\lambda$-abstractions can occur in arithmetic expressions. The function symbol $+$ is not at the same level of importance as the $\lambda$-binder. In your case, we have an applied $\lambda$-calculus that instead uses first-order formulae. Here, the quantifier is at the same level of importance as $+$ was in the calculus with arithmetic expression. – Hans Hüttel Oct 20 '16 at 5:03
• @Zhao The expression/formula $\exists n.\ n\geq 5$ is equivalent to the logical constant $\sf true$. The expression $\lambda n.\ n\geq 5$ is not: it doesn't even have a boolean type! It has type "function from naturals to booleans". This function can be applied to several different values of $n$, and will return a boolean value accordingly. – chi Oct 20 '16 at 9:07

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.

• As an aside: the $\lambda$-calculus was invented to be a foundation of logics: $\forall$ as well as $\exists$ and propositional connectives are definable in the systems Church proposed, see e.g. his A Formulation of the Simple Theory of Types. The use of $\lambda$-calculus for programming comes much later. – Martin Berger Oct 19 '16 at 12:40
• So are there any tutorials about λ -calculus for natural language? I've searched a lot but it appears that all the tutorials are about programming language. – Zhao Oct 20 '16 at 2:08
• Your answer is also very helpful but unfortunately I can only choose one to accept. I accept the above one because there are more discussions above. Thank you anyway! – Zhao Oct 20 '16 at 14:18