# Church numerals without functions

This is really a second part to my first question, but I felt that this was different enough from the first part that it merited its own question.

So, using Church numerals, we define

$$3 = {\lambda} f. {\lambda}x.f(f(f(x)))$$,

and

$$4 = {\lambda} f. {\lambda}x.f(f(f(f(x))))$$.

We can then add with an expression like

$$3\ g\ (4\ g\ z)$$

And this reduces to:

$$(g (g (g (g (g (g (g\ z)))))))$$.

But, of course, this is not how we would define $$7$$ in the scheme above. $$7$$ would be

$${\lambda}g.{\lambda}z.(g (g (g (g (g (g (g\ z)))))))$$.

Why is it still legitimate to call the application $$3\ g\ (4\ g\ z)$$ "7" when we can no longer perform functions with it?

• This is not quite how you add two Church numerals; $g$ and $z$ should be quantified variables. – Yuval Filmus Jan 28 '19 at 3:41

This is just a shorthand, leaving off some things that aren't really needed to understand the concepts. If you want your $$7$$ to be written as a function again, all you need are a couple more implicit lambdas. Here's how I'd write the Church addition with those lambdas in place:
$$3 + 4 = \lambda g . \lambda z . 3 g (4 g z) = \lambda g . \lambda z . 7 g z$$
$$\lambda k . f k = f$$
$$\lambda g . \lambda z . 7 g z = 7$$