>>413 補足

(参考)
fuchino.ddo.jp/books/intro-to-set-theory-and-constructibility.pdf
第I部
構成的集合と公理的集合論入門
以下のテキストは「ゲーデルと20世紀の論理学第４巻」（東京大学出版会，2007）の，渕野 昌の執筆した第I部です．　

（重要ポイントを引用しておきますね）
P95
3.3 集合論の内部での論理とモデル理論

集合論の中での集合論の言語もL∈とよぶことにして，論理式の全体の集合をFmlL∈と表し，
L∈文の全体をClFmlL∈と表わすことにする．
φを集合論の外側での本物の論理式とするとき，φに対応する集合としてのφが存在するが，
この逆は必ずしも成り立たないし，そもそも，この逆を考えること自体が意味をなさない．

たとえば，(∃φ∈FmlL∈)(・・・)という形の論理式がZFCで証明されたとき，
この論理式で存在の主張された論理式φを対応する”本物の”論理式φが具体的に構成できるとは限らないからである．

ZFCに対応するClFmlL∈の部分集合をZFCとあらわすことにする．
この場合にも，具体的に与えられた論理式φがZFCの公理なら，
対応する集合としての論理式φはZFCの元であるし，φがZFCの公理でなければ，
対応する集合φはZFCの元でない．
証明，証明可能などの概念も集合論の述語として自然に翻訳できる．
以下略す
(引用終り)
以上