> Church ends up defining zero as the identity function

Zero is not the identity function. Zero takes a function and calls it zero times on a second function. The end result of this is that it returns the identity function. In Haskell it would be `const id` instead of `id`.

    zero := λf.λx.x
    one  := λf.λx.fx
    two  := λf.λx.ffx

    id   := λx.x

Why isn't the identity function zero? Given that everything in lambda calculus is a function, and the identity function is the simplest function possible, it would make sense to at least try!

If you try, I suspect you'll quickly find that it starts to break down, particularly when you start trying to treat your numerals as functions (which is, after all, their intended purpose).

Church numerals are a minimal encoding. They are as simple as it possibly gets. This may not speak to Church's exact thought process, but I think it does highlight that there exists a clear process that anyone might follow in order to get Church's results. In other words, I suspect that his discover was largely mechanical, rather than a moment of particularly deep insight. (And I don't think this detracts from Church's brilliance at all!)