>>633
Sat自体はただの充足関係を形式的に定義したものでラヨ数固有のものではありません。
また、自由変数xを持つ任意の1変数論理式φ(x)について、∀xφ(x)という文字列を、メタ側で、
「(ある理論の)任意のモデルが、φ(x)のxに任意の要素を代入した論理式(の意味)を充足する」
で定義できるため無関係ではないと思います。

趣旨がよく分からなくなってきたので整理しますが、
>>608では構造の領域という意味で「ドメイン」という言葉をつかいました。
L-論理式φ(x)に現れる自由変数xが量化されると、
その自由変数xに任意の対象を代入してもφが成り立つ(全称量化)、
または、
xに代入してφが成り立つ対象が存在する(存在量化)
のいづれかを意味するようになる、でよろしいでしょうか。

また対象言語の自由変数x'_1,x'_2,x'_3,...を意味するメタ理論の項が存在する、というのはよろしいでしょうか。