モデルの話でZFCを前提にしていいのはわかったけど、
じゃあ「任意の解釈で」みたいな言及はどう扱うの？
ZFCにクラスを「ねじ込んだ」体系ではクラスに関して∀量化子とかは使えないわけだが、
「任意の解釈で論理値trueをもつ」とかいうのはどうやって証明するの？

はじめからクラスと集合の概念があるあの体系（名前は忘れたが）を使うしかないんじゃないか？