In the $\lambda$-calculus, is the family of $\lambda$-terms $(N_i)_{i \in \mathbb{N}}$, defined below, a representation of Church numerals? I think it is, but how do I (sufficiently) show it? If not, what is it?
The terms $N_i$ and $N'_i$ for each natural number $i$ are defined as follows. ($x$ and $c$ are variables while $i$ stands for a number.) \begin{align} N'_0 &= x \\ N'_i &= c \,i\, N'_{i−1} &&\text{for } i > 0 \\ N_i &= \lambda c. \lambda x. N'_i &&\text{for any }i \in \mathbb{N} \end{align}
Disclaimer. I assume that the inductive definition of the $\lambda$-terms $(N_n')_{n \in \mathbb{N}}$ given in the original question, i.e., \begin{align} N_0' &= x \\ N_n' &= f \, n \, N_{n-1}' &\text{if } n > 0 \end{align}
contains a typo: $N_n'$ should be defined as $f \, N_{n-1}'$ when $n > 0$, because $n$ is a natural number and not a $\lambda$-term, so the expression$f \, n \, N_{n-1}'$ does not make any sense in the $\lambda$-calculus. My answer below considers the amended version of that definition.
Church numerals are the $\lambda$-terms used to encode natural numbers in the $\lambda$-calculus.
Usually, for every natural number $n$, the Church numeral $\underline{n}$ representing $n$ is defined as the $\lambda$-term $$\tag{1} \underline{n} = \lambda f. \lambda x. f^n x = \lambda f. \lambda x. \overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots)) $$ ($f^n x$ is just a shorthand for $\overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots))$, for any $n \in \mathbb{N}$).
This definition is slightly informal because it uses dots, which$-$strictly speaking$-$are not in the syntax of the $\lambda$-calculus. How can we define Church numerals in a more rigorous way?
As human beings, we are perfectly able to understand what dots mean. If we fix $n \in \mathbb{N}$, from $(1)$ we are able to write the concrete Church numeral for $n$. For instance: \begin{align} \underline{0} &= \lambda f. \lambda x. x & \underline{1} &= \lambda f. \lambda x. fx & \underline{4} &= \lambda f. \lambda x. f(f(f(fx))) \end{align} So, for the usual practice, definition $(1)$ is perfect. But if we want to write a very rigorous proof of a property of the $\lambda$-calculus involving all Church numerals, what do we do? Are we sure that dots cannot hide some pathological and unexpected behavior of Church numerals?
This search for a more rigorous definition is not only a pedantic issue, but it is of practical interest. Suppose that we want to implement the $\lambda$-calculus in a computer, for instance to use automated theorem provers to verify some property of the $\lambda$-calculus involving Church numerals. How can a computer understand dots?
In mathematics, when you use dots to define an object, it usually means that the object is defined by induction. In the case of Church numerals, we proceed by induction on $n \in \mathbb{N}$. Actually, in $(1)$ dots appear only in the $f^n x$ part, so the inductive definition is required only for a rigorous definition of $$\tag{2} f^n x = \overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots)) $$ Formally, for every $n \in \mathbb{N}$ we define the $\lambda$-term $N_n'$ by induction on $n$ as follows: \begin{align} N_0' &= x &&\text{(base case)} \\ N_{n}' &= f \, N_{n-1}' &&\text{(inductive step, for $n > 0$)} \end{align}
What is the relation between this inductive definition and $(2)$?
Property. For every $n \in \mathbb{N}$, we have $$\tag{3} f^n x = N_n'. $$
Proof. By induction on $n \in \mathbb{N}$.
$$ f^{n+1} x = \overbrace{f(f( \cdots (f}^{n+1 \text{ times }}x)\cdots)) = f \,(\overbrace{f(f( \cdots (f}^{n \text{ times }}x)\cdots))) = f (f^n x) \overset{\text{IH}}{=} f \, N_{n}' = N_{n+1}'. \quad \square $$
We have just proved $(3)$, that is, that for every $n \in \mathbb{N}$ the $\lambda$-term $f^nx$ defined via dots in $(2)$ is the same as the $\lambda$-term $N_n'$ defined inductively. From $(3)$ it follows that Church numerals defined in $(1)$ are exactly the same as the $\lambda$-terms $(N_n)_{n \in \mathbb{N}}$ defined as follows:
\begin{align} N_n &= \lambda f. \lambda x. N_n' &\text{for every } n \in \mathbb{N}. \end{align}
Indeed, for every $n \in \mathbb{N}$, we have $$\underline{n} = \lambda f. \lambda x. f^n x \overset{(3)}{=} \lambda f. \lambda x. N_n' = N_n. $$