>>646
「超準解析で表れるような」実数、実数値関数などなどのsortを持つ言語で十分だろ？
「普通の数学」では量化は全部タイプがついているんだから。
通常の数学はmany-sortなのに、Π3とかΣ2とかone-sortを前提にした用語を不用意に使ったのが問題なだけ。
自分の不用意発言を根拠に「普通の数学では言語をはっきり固定して議論しない」とか勝手に結論出すなよ。