話変わるけど、この定義だと「コード化されたφ(x)∈F」にはxが自由に現れないから、{x∈A|φ(x)}は∅かAのどっちかにしかならなくね？

>仮に定義できたとしたら、任意の一変数論理式φ(x)に対して {x∈A|φ(x)}:={x∈A|コード化されたφ(x)∈F} により分出公理を（メタ変数を用いず）形式体系内で記述できるが、実際はそうでない。