ZFCの公理のコードを
（計算可能なように、例えば閉論理式を文字列として見て辞書順になるように）
並べて{’φi’}（i∈ω） とする。（ここで’a’は┌ a ┐の代用のつもり）
以下簡単のためにψi≡φ0∧φ2∧……∧φi とする。
さらに ’ψi’を満たすモデル M_i |= ’ψi’を取って
M_i たちの超積をとり、M とすると、φnを満たさない M_i はn個以下で任意のnに対して有限なので
MはZFCのモデルとなる。
つまりZFC |- ∃M ( M |= ZFC) となることが示された。

って議論は、たぶんどこかおかしいと思うんですけど、どこがおかしいんでしょうか。

<i , ’ψi’>_{i} ってただの帰納的関数で具体的にプログラム組めるくらいなので
当然こういう関数は可算モデルだろうが何だろうが最初から持っているはずですよね。
(1) ’ψi’をパラメータとして使うことが許されてもなお、
i の関数として ψi をみたすモデル M_i は取れない？
(2) V と任意の閉文について真偽を等しくするelememtary submodel M 自体は作れるが
M が φi を満たすことの証明に公理 φi の使用が必要なので、M がZFCのモデルとなることは示せない？

細かい事情が分からないので誰か分かる人御教示ください