I read that there is sequent calculus for second order substructural predicate logic https://link.springer.com/chapter/10.1007/978-3-319-08587-6_5 and sequent calculus for second order (what it means?) propositional logic https://pdfs.semanticscholar.org/1857/895c0797587afa4c6da7714a366dec03563a.pdf but is there sequent calculus for classical (non-substructural) second order predicate logic of higher order predicate logic? Are there any obstacles to obtain them or maybe they are so simple generalization of the calculus for the first/second order predicate logic that journals don't accept them as important results for publication and so - they stay as folklore?
Of course, proof theory for higher order logic is not very nice but without requiring all the niceties why not to devise the sequent calculus that can capture the maximum reasoning power?