Barendregt Recursion encoding

Question

There is a definition in "Lambda Calculi with Types" by Henk Barendregt (pdf) that I am really struggling with. There are seemingly no examples of it, and I can't find anyone else on the internet using it. Is this a number? I can try and use this definition and apply # to something like PRED and end up with something like <3, <3, #n, <3, #f < ...>>> and that really means nothing to me. And then they applied it to a set and then I get even more confused. A is recursive is #A is recursive? The more I think about it the less I understand. Please help

Answer 1

The first clause in Def. 2.2.13 just introduces a convenient notation $v^{(n)}$ for the symbol (presumably a variable) consisting of the letter $v$ with $n$ primes attached. The second clause introduces, for each expression $A$ of the lambda calculus, a number $\#A$. The three equations in this clause might suggest that $\#A$ is actually a pair of pairs of $\dots$ pairs of numbers, but the very beginning of this clause says that $\langle x,y\rangle$ is not a pair but a number coding the pair (in some standard pairing function). The last clause in this definition introduces a notation ($M$ with corner-quotes around it) for the lambda term that represents the number $\#M$.

You complained that "they applied it to a set", which probably refers to the $\#\mathcal A$ in the last clause of Def. 2.2.14. But that notation is defined right there; it means apply $\#$ to all the members $M$ of the set $\mathcal A$.

I think that covers what you were asking about, in regard to $\#$. The other clauses in the definitions don't involve $\#$.