# predecessor and multiplication prove

I have trouble, when attempting to :

1- prove mult defines the multiplication function.

2- Prove pred defines the predecessor function.

1- for mult:

Base Case:

mult 0x= 0

Inductive case:

:= $$(\lambda m. \lambda n. \lambda f . \lambda x.m (nf)x) (\lambda f. \lambda x.x)(\lambda fx. \lambda x.(f^{(n)} x))$$

the result is $$(\lambda f. \lambda x.x)$$.

2- for pred:

Base Case:

f(0,..)= 0

Inductive case:

$$\lambda n.\lambda f. \lambda x.n (\lambda g. \lambda h.h (gf)) (\lambda u.x)( \lambda u.u)$$.

(f(s(x),..) = n-1

And I am unsure of where to go from there, because I have no parameters for the n to be n-1.

• The fact that $(λm.λn.λ f .λx.m (nf)x) (λf. λx.x)(λfx.λx.(f^{(n)} x))$ reduces to $(λf. λx.x)$ proves that $\text{mult} \, 0 \, n = 0$. The inductive case for $\text{mult}$ is completely lacking. – Taroccoesbrocco Jan 26 at 11:17
• what about predecessor ? – Jared Jan 26 at 12:40
• @Taroccoesbrocco I have been create post for multiplication question. – Jared Jan 28 at 1:06

The proof that the term $$\text{pred}$$ encodes the predecessor function over natural numbers is quite technical and requires a lemma.

For any $$n \in \mathbb{N}$$, let $$\underline{n} = \lambda f \lambda x. f^{n} x = \lambda f \lambda x. \overbrace{f (\cdots (f}^{n \text{ times}} x) \cdots)$$ (in particular, $$\underline{0} = \lambda f \lambda x.x$$).

Lemma. Given $$n \in \mathbb{N}$$, $$(\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x)$$ reduces to $$\lambda h.h (f^n x)$$

Proof. By induction on $$n \in \mathbb{N}$$.

• Base case ($$n = 0$$):

\begin{align} (\lambda g \lambda h.h (g f)) (\lambda u.x) \to \lambda h.h ((\lambda u.x) f) \to \lambda h.h x \,. \end{align}

• Inductive step: we suppose that $$(\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x)$$ reduces to $$\lambda h.h (f^n x) \,$$ (induction hypothesis) and we show that $$(\lambda g \lambda h.h (g f))^{n+2} (\lambda u.x)$$ reduces to $$\lambda h.h (f^{n+1} x)$$.

\begin{align} (\lambda g \lambda h.h (g f))^{n+2} (\lambda u.x) &= (\lambda g \lambda h.h (g f)) \big((\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x) \big) \\ &\to^* (\lambda g \lambda h.h (g f)) (\lambda h.h (f^n x)) \quad \text{(by induction hypothesis)} \\ & \to \lambda h.h ((\lambda h.h (f^nx)) f) \to \lambda h.h (f (f^n x)) = \lambda h.h (f^{n+1} x) \, .\\ &\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \square \end{align}

Let $$\text{pred} = \lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u)$$. Thanks to the lemma above, let us show that the term $$\text{pred}$$ encodes the predecessor function over natural numbers, i.e. that $$\text{pred} \, \underline{0}$$ reduces to $$\underline{0}$$, and $$\text{pred} \, \underline{n+1}$$ reduces to $$\underline{n}$$ for any $$n \in \mathbb{N}$$.

• Case $$n = 0$$: \begin{align} \text{pred} \, \underline{0} =& \ \big(\lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \big) \lambda f \lambda x.x \\ \to& \ \lambda f \lambda x. (\lambda f' \lambda x'.x') (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda x'.x') (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. x = \underline{0} \end{align}

• Case $$n + 1$$: \begin{align} \text{pred} \, \underline{n+1} =& \ \big(\lambda n \lambda f \lambda x.n (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \big) \lambda f \lambda x. f^{n+1}x \\ \to& \ \lambda f \lambda x. (\lambda f' \lambda x'. (f')^{n+1}x') (\lambda g \lambda h.h (g f)) (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda x'. (\lambda g \lambda h.h (g f))^{n+1} x') (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda g \lambda h.h (g f))^{n+1} (\lambda u.x) (\lambda u.u) \\ \to& \ \lambda f \lambda x. (\lambda h. h (f^n x)) (\lambda u.u) \quad \text{(by the lemma)}\\ \to& \ \lambda f \lambda x. (\lambda u.u) (f^n x) \\ \to& \ \lambda f \lambda x. f^n x = \underline{n} \, . \end{align}

The proof that the term $$\text{mult}$$ encodes the multiplication function over natural numbers is similar to (and slightly simpler than) the proof above.

• Thanks. but for mult do I need to have exponential ? – Jared Jan 26 at 22:52
• @Jared - Yes, but I guess a complete answer for $\text{mult}$ requires a new question, otherwise this answer becomes too long. – Taroccoesbrocco Jan 27 at 9:46
• Ok , I will post it. math.stackexchange.com/questions/3089352/multiplication-prove – Jared Jan 27 at 9:49