一句话：证明了带受限 U 量词的 MSO 逻辑对递归方案生成树的模型检测可判定，并给出反射与有效选择性质。
论文研究递归方案（recursion schemes）的模型检测问题：给定高阶递归方案生成的树，判定其是否满足某个逻辑句子。已知 MSO 逻辑下该问题可判定；本文将其扩展到带 U（unbounding）量词的 MSO。U 量词表示某子公式对任意大的有限集合成立，但仅允许用于所有自由变量都表示有限集合的子公式，无限制使用会导致不可判定。作者证明这种受限扩展仍可判定，并进一步说明该逻辑对递归方案生成的树具有反射（reflection）和有效选择（effective selection）性质。
We study the model-checking problem for recursion schemes: does the tree generated by a given higher-order recursion scheme satisfy a given logical sentence. The problem is known to be decidable for sentences of the MSO logic. We prove decidability for an extension of MSO in which we additionally have an unbounding quantifier U, saying that a subformula is true for arbitrarily large finite sets. This quantifier can be used only for subformulae in which all free variables represent finite sets (while an unrestricted use of the quantifier leads to undecidability). We also show that the logic has the properties of reflection and effective selection for trees generated by recursion schemes.