>超準解析で表れるような構造を先に定義するような方法を例に挙げてるじゃん

>あと多重量化(つまりΣ2ないしΠ2より複雑な式)は普通の数学に表れるとは言ったが

どう突っ込んで良いのか分からんが、超準解析でやるような言語の設定だと
(上付添字なしの)Σ2とかΠ2とかって普通は定義しないんだが。
少なくとも標準的な定義はないのだからΣ2やΠ2の定義を与えるべき。
こういう多種の言語の場合、どの種の量化かが問題になるので
Σ^m_nみたいにどの種の量化を数えるのかを上付添字で明示するの普通。
>>580は別人なのか本人なのか知らないけど、それを見ていると
そういうこと全く分かっていないで書いてるな、ということがよく分かる。