>>725
>1階のPAだと帰納法の公理に現れるのは具体的な述語たちだけど
うん、無限個すべてを書ききれないからメタ変数を使って見た目上ひとつの公理かのように書いたものが公理図式だね

>2階だと任意の述語についてのひとつの公理にできる
うん、二階なら述語を量化可能だからメタ変数を使わずとも形式体系内で記述できるね。
そのことが一階と違ってモデルが範疇的となる原因だね。
但し二階の場合正しい命題は必ずしも証明可能でないけどね。

>みたいな表現力のパワーアップをZFCでは何階でも自動でできる
表現力が高いのはその通りだけど、君が公理の話をしてるのでそれについて言うなら、ZFCの公理図式を形式体系内で記述することはできない。
タルスキの真理述語の定義不能性定理により、集合論の任意の文ψに対して ψが真⇔コード化されたψ∈F を満たす集合Fを集合論で定義できない。
仮に定義できたとしたら、任意の一変数論理式φ(x)に対して {x∈A|φ(x)}:={x∈A|コード化されたφ(x)∈F} により分出公理を（メタ変数を用いず）形式体系内で記述できるが、実際はそうでない。