First-Order Logic: Simplifying $\exists x. (P(x))\,(\lambda y.see(y,x))$

Question

In Chapter 10 section 4.2 (of the on-line documentation supporting the Natural Language Toolkit), there are 3 sets of equations (39), (40), (41). The author talked about how careful one should be in selecting variables due to $\beta$-reduction. My problem is I cannot see how $\beta$-reduction is taking place moving from equation (40a) to (41a). Here's the 3 equations:

39a) \y.see(y, x)

40a) \P.exists x.P(x)(\y.see(y, x))

41a) exists x.see(x, x)

So here's my interpretation:

The $\lambda$-calculus expression for 39a is $$\lambda y.see(y,x)$$

The $\lambda$ term added to the term converting to 40a is $\lambda P.(\exists x. (P(x)))$ and so it converts to 40a which is

$$\lambda P.(\exists x. (P(x)))\,(\lambda y.see(y,x))$$

So since $x$ is the free variable in 40a, how do I reduce it to yield 41a? I'm thinking (first line is copied from above...which means there might already be mistakes in that line)

$$\lambda P.(\exists x. (P(x)))\,(\lambda y.see(y,x))$$ removing the $\lambda P$ term: $$\exists x. (P(x))\,(\lambda y.see(y,x))$$ sub. all occurrences of $x$ on LHS with $(\lambda y.see(y,x))$ term: $$\exists x. ((\lambda y.see(y,x))$$ and somehow yields

$$\exists x. see(x,x)$$

which is 41a. Is there a mistake in how I do the $\beta$-reduction?

Answer 1

$β$ -reduction is the process of "evaluating" the function.

The $\lambda$ symbolism is aimed at avoiding the "sloppiness" of the traditional mathematical symbolism where (usually) $f(x)$ denotes the function and $f(a)$ denotes the value of the function for input $a$.

Thus, the function (of one argument) is denoted $\lambda x . f(x)$ and its value for input $a$ is the result of the "application" of $\lambda x . f(x)$ to argument $a$, getting:

$\lambda x . f(x)(a)$ that reduces to the "usual" $f(a)$.

See the simple example of the function $\lambda x . \text {walk}(x)$ applied to argument $\text{angus}$ to get $\text {walk} (\text {angus})$.

So far, quite simple.

A little bit tricky is the next step: to consider a function whose argument is not an "individual" but a function, like:

$λP . P(\text {angus})$.

In this case, we have a "function-of-$P$"; if we applies it to argument (a function) $λx . \text {walk}(x)$ what we get is:

$λP . P(\text {angus})(λx . \text {walk}(x))$ i.e. $λx . \text {walk}(x)(\text {angus})$.

The final step is evaluating the resulting function of $x$ to the argument $\text {angus}$ getting $\text {walk}(\text {angus})$.

---

In the example with the quantifier inside, the difference is that $∃x P(x)$ is not a function of $x$.

When the variable $P$ is replaced with the name of a function, the result will be a sentence that does not refer to any $x$. Thus the $λ$ sign must disappear.

If we read the name of the function $λP . (\exists x \ P(x))$ as:

"being a $P$ such that there is something that is a $P$",

we have to compare it to:

(41.b) "there is something such that it sees $z$",

versus:

(41.a) "there is something such that it sees itself".

---

The story is this (about predicate logic): in an expression $\forall x \ \alpha(x)$ (the same with $\exists x$) we cannot replace $x$ with a term containing $x$ free, because the "capturing" of the new occurrence of $x$ by the quantifier will change the meaning.

Silly example from arithmetic: from the soud $\exists x \ (x=0)$ we can get the wrong $\exists x \ (x+1=0)$ if we put $x+1$ in place of $x$.