Universal quantification via lambda binding?

180 Views Asked by At

I remember once saw somewhere that a universally quantified formula can be written using $\lambda$. But I cannot recall very clearly. I have an vague impression that is is something of the form:

$\forall n \in \mathbf{N} . P(n)$ = $? (\lambda n . P(n))$

Please help if you know. Also, is there any specific reason to write universally quantified formula like this or is it just a style of taste?

1

There are 1 best solutions below

0
On

I found the answer.

$\forall n \in \mathbf{N} . P(n) = \Pi_\mathbf{N} (\lambda n . P(n))$

It is really nothing special. Instead of introducing a new binder, it just shift the binding task to an existing binder, namely $\lambda$. Here $\Pi$ just serves as a marker or a tag, carrying the information that the bound variable $n$ is of type $\mathbf{N}$. Hence, other symbols will do the job too.