二阶逻辑的部分完备性及演绎闭包中语句的可推导性问询

嘿，我最近在琢磨二阶逻辑的演绎闭包相关问题，想请教大家一些关于语句可推导性的事儿。先跟大家铺垫下基础背景：咱们都知道一阶逻辑是完备的——也就是说，给定一个一阶理论，任何在该理论的所有模型中都为真的语句，都能从这个理论推导出来。同样大家也清楚，二阶逻辑一般来说是不完备的。不过呢，咱们还是可以考虑某个二阶理论的演绎闭包，并且尝试去刻画它。

我的核心问题就是：这个演绎闭包里可能包含哪些类型的语句？尤其是下面这两类语句，如果它们为真的话，是否是可推导的：

• 本质上属于一阶的二阶语句：这类语句的所有量化（甚至参数）都是元素类型的，而非子集类型。这类语句如果为真的话，并不是显然可推导的，因为理论的每个公理化都可能包含“真”的二阶语句。
• 一个声明了[原提问内容此处截断，未完整呈现]的二阶语句

备注：内容来源于stack exchange，提问作者Carlyle