Solution (source code)

= Solution

Let $N$ be a <well-founded model of set theory> of the complete theory $T$, and suppose that a <Paris model> $M\models T$ were ill-founded. Its internal <ordinals> would then contain an external descending sequence
$$
\alpha_0\ni^M\alpha_1\ni^M\alpha_2\ni^M\cdots.
$$
For every $n$, choose a <first-order formula> $\varphi_n$ that uniquely defines $\alpha_n$ in $M$. The sentences asserting that $\varphi_n$ uniquely defines an ordinal and that the object defined by $\varphi_{n+1}$ belongs to the object defined by $\varphi_n$ are true in $M$. Since $T$ is complete, all its models satisfy the same <first-order sentences>, so the corresponding uniquely defined ordinals in $N$ form an external descending membership sequence. This contradicts the well-foundedness of $N$. Thus <Paris models are well-founded when their complete theory has a well-founded model> proves that \b[every Paris model of $T$ is well-founded.]