一句话：扩展静态逻辑框架，证明最小谓词主义无限集理论是计算性的，且足以形式化大部分科学适用数学。
本文延续将不同强度集合论形式化并机械化的静态逻辑框架。作者首先为框架加入定义扩展机制，使理论可被连贯地扩展而不破坏其静态性质。随后研究该框架中最小且谓词主义可接受、能证明无限集存在的理论。证明该理论是计算性的：其最小传递模型（即 Jensen 层谱的第二宇宙）中每个元素都由某个闭项指称。进一步，作者展示这一极小理论已足以发展绝大部分（若非全部）科学适用数学；为此需将实数集合视为真类，即通过静态扩展方法引入的一元谓词。结果表明极小计算集合论可作为大量科学数学的形式化基础。
In previous papers on this project a general static logical framework for formalizing and mechanizing set theories of different strength was suggested, and the power of some predicatively acceptable theories in that framework was explored. In this work we first improve that framework by enriching it with means for coherently extending by definitions its theories, without destroying its static nature or violating any of the principles on which it is based. Then we turn to investigate within the enriched framework the power of the minimal (predicatively acceptable) theory in it that proves the existence of infinite sets. We show that that theory is a computational theory, in the sense that every element of its minimal transitive model is denoted by some of its closed terms. (That model happens to be the second universe in Jensen's hierarchy.) Then we show that already this minimal theory suffices for developing very large portions (if not all) of scientifically applicable mathematics. This requires treating the collection of real numbers as a proper class, that is: a unary predicate which can be introduced in the theory by the static extension method described in the first part of the paper.
@article{paperbot370,
title = {Applicable Mathematics in a Minimal Computational Theory of Sets},
author = {Arnon Avron and Liron Cohen},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 4},
year = {2018},
doi = {10.23638/lmcs-14(4:1)2018}
}