  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.
