Why are recursive types needed as primitives for proofs in dependent type systems?
I'm not an expert, but I'll share what I understood so far with an example.

Let's consider the boolean type in CoC, using its standard encoding:
$$
\begin{array}{l}
\mathbb{B} = \Pi_{\tau:*} \tau \to \tau \to \tau
\\
\mathsf{tt} = \lambda \tau:*,x:\tau,y:\tau.\ x
\\
\mathsf{ff} = \lambda \tau:*,x:\tau,y:\tau.\ y
\end{array}
$$
We might expect to be able to prove
$$
\Pi_{b : \mathbb{B}} b={\sf tt} \lor b = {\sf ff} \qquad(*)
$$
Indeed, this quickly follows from the dependent elimination/induction principle we have e.g. in CiC
$$
\mathbb{B}_{ind} : \Pi_{P:\mathbb{B}\to*} P({\sf tt}) \rightarrow P({\sf ff}) \rightarrow \Pi_{b:\mathbb{B}} P(b)
$$

However, we can not really expect (*) to hold in all models of CoC!
Intuitively, a value in $\mathbb{B}$ should roughly be a family of functions
$\{f_\tau\}_{\tau}$ assigning to each type $\tau$ a value in the interpretation of $\tau\to\tau\to\tau$. But this does not force $f_\tau$ to be one between the values of $\sf tt,ff$. We could have e.g. (informally)
$$
f_{\mathbb{N}}(n)(m) = n+m
$$

To be sure that the values of $\sf tt,ff$ are the only possible values, we need to restrict ourselves to parametric models. Indeed (I think) the property $(*)$ can be proven from the free theorem associated to the polytype $\mathbb{B}$.

However, as far as I understand, CoC does not rule out ad-hoc models, where parametricity does not hold. In some of those, $(*)$ is simply false. By soundness, in the presence of a countermodel, we conclude that $(*)$ is not inhabited in CoC. Consequently, there's no $\mathbb{B}_{ind}$ term in CoC, either.