Church numerals: How should I interpret the numbers from expressions?

Question

Can someone explain to me using substitutions how we get a number "zero" or the rest of natural numbers?

For example the value: "zero"

λf.λx.x

if I apply this expression on an another expression:

"(λf.(λx.x)) a"

then using substitution:

:=[a/f](λx.x)
:=(λx.x)

what am I missing? How should I interpret these number expressions?

Answer 1

The church numeral n is a function that takes another function f and returns a function that applies f to its argument n times. So 0 a (where 0 is, as you said, λf.λx.x ) returns λx.x because that applies a to x 0 times.

1 a gives you λx. a x, 2 a gives you λx. a (a x) and so on.