超準解析で表れるような構造を先に定義するような方法を例に挙げてるじゃん
きちんと論理式として表現できてるでしょ
それをマトモに感じるかどうかは知らんけど

ZFC上Δ0やΔ1であっても、それより弱い理論での量化の階層を考えることには
(ロジックとしては)意味があると思うけど。
(尤も普通の数学では事実としてそんなこと一切気にしていない、という流れではあるが。)
一番簡単な例で言うとPeano算術の部分理論のreflectionを考えたりするときに
各階層ごとの真理述語とかを定義したりするでしょ。
ZFCの言明としてはΔ0なんだからそれらの言明も本当はΔ0なんだ、というのは違うと思う。

あと多重量化(つまりΣ2ないしΠ2より複雑な式)は普通の数学に表れるとは言ったが
Σ5論理式が現れるなんて言ってないし、そういう例を頑張って探してくるつもりもないからね。
だいたい元から労力がやたら掛かるから言明ごとにこれはΣいくつ、これはΠいくつ、
と分類したりしない、と言う話なんだから。