確かにそうですね。
まぁその複雑さが現実的な研究価値を減らしているということは
間違っていないと思います。
なぜか2階述語論理が人間にとってすごい便利なんですよね。
特に2階述語論理の中でもヘンキン・モデルとか呼ばれる
論理体系が。
おそらく常に完全性定理が成立するからかな？
スタンダード・モデルでは完全性定理が成立しないし、
3階以上ではほとんど完全性定理が成立しない。
これでは今の証明論が使えないし、
新しく作られた証明論も使いにくいだろうね。
そもそも証明という概念自体を見直す必要さえあるだろうけど。