便乗して質問です。
以前、整列順序<ω_1CK, ＜>は算術の述語を用いてω上に定義することができないと
このスレにあった気がするのですが、
Σ1文では上手くいかないというのは分かるのですが、
もっと量化の複雑な式を用いて定義することはできるのではないでしょうか？

上の質問と関連するのですが、第一不完全性は、
公理（のゲーデル数）の集合がΣ1ではなくて
Σnだったときにも一般に成立するんでしょうか？