Reverse Mathematics in Constructive Set Theory

部分解决了构造性逆数学中的一些公开问题，如单调完备性定理、二元展开定理和中值定理。单调完备性定理等价于LPO、弱归纳公理和一种可数选择，二元展开定理和中间值定理等价于树上具有一定凸性条件的WKL的各种形式。这些结果也适用于构造性集合论的一个子系统。提出了一种将集合论解释为运算理论的方法，作为一种对初等分析理论有解释的中间理论。给出了APP中足以解释空集公理、对公理、无穷公理和弱分离公理。对APP中足以解释可拓性公理的一个公理进行了广泛的研究。

Some open problems in constructive reverse mathematics, such as the monotone completeness theorem, the binary expansion theorem and the intermediate value theorem have been partially solved. The monotone completeness theorem is equivalent to LPO, a weak induction axiom and a kind of countable choice, and the binary expansion theorem and the intermediate value theorem are equivalent to versions of WKL with some convexity conditions on trees. Those results also hold in a subsystem of the constructive set theory.A method of interpreting a set theory by interpreting it into the theory of operation APP, as an intermediate theory, which has an interpretation in to a theory of elementary analysis has been proposed. Axioms in APP which are sufficient to interpret the axioms of empty set, pair, infinity and a weak separation have been given. An extensive investigation on an axiom in APP which is sufficient to interpret the axiom of extensionality has been carried out.