The $\lambda_I$-calculus is a restricted version of the usual $\lambda$-calculus. The set of expressions in this restricted calculus, $\Lambda_I$, can be defined inductively:
- If $x$ is a variable, then $x \in \Lambda_I$.
- If $M \in \Lambda_I$ and $x$ is a free variable in $M$, then $(\lambda x.M) \in \Lambda_I$.
- If $M, N\in\Lambda_I$, then $(MN)\in\Lambda_I$.
The restriction is the added requirement in the abstraction rule (rule $2$) that $x$ be a free variable in $M$. In particular, in the usual $\lambda$-calculus we have "constant" expressions like $\lambda y.x$; here we do not. However, with the usual definition of $I=\lambda x.x$, we see that by rule $2$, $I\in \Lambda_I$.
Recall that the Church numerals are usually defined as follows:
- $C_0 := \lambda fx.x = \lambda f.I$
- $C_1 := \lambda fx.fx$
- $C_2 := \lambda fx.f(fx)$
- $C_3 := \lambda fx.f(f(fx))$
and so on, with $C_{n+1} := \lambda fx.f(C_n f x)$. Clearly $C_n \in \Lambda_I$ for $n>0$, so we can just define $C_n^I=C_n$ for $n>0$. But $C_0 \not\in \Lambda_I$, so we are forced to use an alternate version:
- $C_0^I := \lambda f x. f I I x$.
A theorem of Kleene says: a partial numeric function is $λ_I$-definable iff it is partial recursive. So there must be a $λ_I$-definable version of the Predecessor function, which satisfies ${\mathsf{Pred}} \;C^I_{n+1} = C^I_n$. Is there a construction of this function?