论文标题
抽象逻辑：（计算机）数学的新基础
Abstraction Logic: A New Foundation for (Computer) Mathematics
论文作者
论文摘要
抽象逻辑是一种新的逻辑，是数学的基础。它结合了谓词逻辑和高阶逻辑的特征：可以将抽象逻辑视为高阶逻辑减去静态类型以及谓词逻辑加算子和可变绑定。我们认为，抽象逻辑是最好的基础逻辑，因为它可以最大程度地提高简单性和实际表现力。该论点得到了以下观察结果，即抽象逻辑具有比所有其他一般逻辑更简单的术语和更简单的证明概念。同时，抽象逻辑可以正式化直觉和经典的抽象逻辑，并且对于这些逻辑和所有其他逻辑，可以与均等进行推论逻辑。
Abstraction logic is a new logic, serving as a foundation of mathematics. It combines features of both predicate logic and higher-order logic: abstraction logic can be viewed both as higher-order logic minus static types as well as predicate logic plus operators and variable binding. We argue that abstraction logic is the best foundational logic possible because it maximises both simplicity and practical expressivity. This argument is supported by the observation that abstraction logic has simpler terms and a simpler notion of proof than all other general logics. At the same time, abstraction logic can formalise both intuitionistic and classical abstraction logic, and is sound and complete for these logics and all other logics extending deduction logic with equality.
