Lambda Definability

A set is $\lambda$-definable if a verifier can be written in $\lambda$-calculus

Here is a collection of examples (tbd). $$ A = \{ \# M | \mathbf{\Theta} M =_{\beta\eta} (\lambda x.xx) \} $$ Such $A$ is empty due to the fact that $\forall M. \mathbf{\Theta} M \not \Rightarrow_{\beta\eta}$. Thus $V_A = \mathbf{K} \mathbf{F}$ $$ B = \{ \# M | M \mathbf{T} =_{\beta\eta} M \mathbf{F} \ulcorner M \urcorner \}$$ $$ C = \{ 2^{\#M} \cdot 3^{\#N} | M =_{\beta\eta} N \}$$

Suppose $C$ is $\lambda$-defined by $V_C$, we scheme a set $C' = \{ \#M | M =_{\beta\eta} \mathbf{I} \}$, then it would be defined by

$$ V_{C'} = \lambda n . V_C ( \mathbf{Mul} \, (\mathbf{Exp} \, \mathbf{2} \, n ) \, (\mathbf{Exp} \, \mathbf{3} \, \ulcorner \mathbf{I} \urcorner )) $$

However, $C'$ is not $\lambda$-definable due to Rice's theorem.

Appendix - Common Lambda Terms

• $\mathbf{\Theta} = (\lambda wf.fww)(\lambda wf.fww)$, $\mathbf{\Theta}$ is a fixed-point combinator, i.e. $\mathbf{\Theta}F =_{\beta\eta} F(\mathbf{\Theta}F)$
• $\ulcorner M \urcorner$ is the encoding of $M$ in Church numbers.