@JoelDavidHamkins Certainly, it does not seem trivial to me. However, in his book "Proper and improper forcing", VII 3.20, Shelah says: "The small gain is that we directly find a function specializing $T$ rather than finding one specializing a closed unbounded set of levels, and then using a theorem saying this is equivalent". But I cannot find a proof or a reference of that theorem in the book or elsewhere.

I see! For each mathematical formula $\phi$, we can define another mathematical formula $p\Vdash\phi$ in such a way that $M\vDash p\Vdash \phi$ ($M$ a set) satisfies the fundamental theorem. Thanks!

Thank you. The problem is that in order to use the hypothesis that $N\prec H_\lambda$ to prove $N[G]\prec H_\lambda[G]$, using $\Vdash$ seems unavoidable, and, in view of the answer to Question 1, it seems we should restrict ourselves to consider meta-mathematical formulas.

Thank you, Joel. I did not know the result of Laver and Woodin, but I have found it in internet.

Thanks. Yes, working with sufficiently large sets is clearly enough in this context.I think that the results that Jech proves to show that the Cohen model satisfies the ordering principle will be enough to "translate" the Halpern and Lévy proof to a modern language. Now I am jammed in a step in the proof that every set has a minimal support, but the problem has nothing to do with the present question.

@AsafKaragila It is a bit strange: If I start a new answer and copy the code for de diagram, it does not work. Then I add \require{AMScd} and it works, but if then I remove this command, the code still works.

@AsafKaragila : I tried to do it, but I did not know how to load the package. Now I have consulted the MO meta and I have edited the diagram. Thanks.

Of course. The answer to you question is negative in a very general setting: in any model of set theory / arithmetic containing non-standard natural numbers, the sets that are externally finite cannot be characterized by a formula, since otherwise the induction principle would be violated inside the model.

I succeeded in proving the step I mentioned, so please do not worry about it. @Andreas Blass Thank you for the idea. I will try to work it with some examples.