I'm slightly confused by the successor function for Church numerals.
Written down in my textbook it is defined as follows:
$$succ = \lambda n. \lambda f. \lambda x. n \;f \; (f \; x) $$
Therefore incrementing a number $n$ by one works as follows:
$$ (\lambda n. \lambda f. \lambda x. n \; f \; (f \; x)) \; (\lambda f. \lambda x. f_n \; x)$$ $$ \rightarrow \lambda f. \lambda x. \; (\lambda f. \lambda x. f_n \; x) \; f \; (f \; x)$$ $$ \rightarrow \lambda f. \lambda x. (\lambda x. f_n \; x) \; (f \; x)$$ $$ \rightarrow \lambda f. \lambda x. (f_n \; (f \; x) $$ $$ = \lambda f. \lambda x. f_{n+1} \; x $$
where $n$ is represented as $\lambda f. \lambda x. f_{n} \; x$
My question is why would the following $succ$ formula not work:
$$ succ = \lambda n. (\lambda x. n) \; (f \; x)$$
I believe incrementing a number $n$ by one would work as follows using this formula:
$$ (\lambda n. (\lambda x. n) \; (f \; x)) \; (\lambda f. \lambda x. f_n \; x)$$ $$ \rightarrow (\lambda x. (\lambda f. \lambda x. f_n \; x)) \; (f \; x) $$ $$ \rightarrow \lambda f. \lambda x. f_n \; f \; x $$ $$ = \lambda f. \lambda x. f_{n+1} \; x$$
Does this formula not work because when I am performing $\beta$-reduction on the $x$ variable I am replacing the $x$ with $(f \; x)$ when I should not—possibly because it is bound by the inner abstraction?
Here
$$ \underline{f} = (\lambda x. (\lambda fx. f^n x))(fx) $$
$(\lambda fx.f^n x)$ has its own scope and $x$ in it is bound by it.
So
$$ \underline{f} = (\lambda x. (\lambda fx. f^n x))(fx) = \lambda fx.f^n x = \underline{n} $$
And yes, your function gives wrong result.