Is weak second-order logic sufficient for Humanities research?

In the process of reading Jouko Väänänen's article on "Second-order and Higher-order Logic" in the Stanford (Internet) Encyclopedia of Philosophy, I came across the question of whether weaker forms of second-order logic are decidable or not.

One interesting paper in this regard is Michael O. Rabin's paper from July of 1969, where he shows the decidability of some second-order theories (using the automata on infinite trees, a reduction of a Turing machine that can only read but not write to the tape).

Perhaps most promising seems to me to be that both linearly ordered sets (Corollary 2.2) and countable well-ordered sets (Corollary 2.3) is decidable. The result that Rabin seems to be especially proud of, that the second-order theory of a unary function in a countable domain is decidable (Theorem 2.4), seems to be unhelpful for the knowledge representation needs of the Humanities.

What seems unclear at this point is whether weak second order logic allows the relating of sentences as well as contextualization. That seems to be the crux of the matter for the Humanities, after all. Väänänen writes:

In weak second-order logic we have no function variables and the relation variables range over finite relations only. The resulting logic is in many ways similar to the extension of first order logic by the generalized quantifier $Q_0$. 

The inability to iterate over the functions seems acceptable, as we can turn all finite function applications into terms anyway.

Perhaps it will require a look at finite model theory to make progress on this question.

Addendum: Notice that Daniel Leivant's Higher Order Logic discussion also emphasises that the key features of weak second-order logic is that the relations variables "range over finite relations" [p44], which is later clarified to mean that the relation variable "R is ranging over finite sets" [p.45] and that there are not function variables [p44]. Among the noteworthy results, Leivant mentions that

• Though the upward Skolem-Löwenheim property does not hold, the downard Skolem-Löwenheim property does [p.45]
• The set of f-valid second order formulas is PI-1/1 [p.45].
• Linear ordering and one function are both decidable [p.45].