Abstraction Logic: A New Foundation

Abstraction logic is a logic designed to bridge the gap between informal and formal mathematical reasoning. The key innovation lies in its ability to simultaneously support general binders and maintain a single mathematical universe\emdash two features that have traditionally appeared incompatible in formal logic. This is achieved by carefully distinguishing between mathematical objects, operations, and operators. A comprehensive theory of abstraction logic is presented, including its algebraic foundations, a semantic account of alpha equivalence, and sound proof systems for both natural deduction and sequent calculus. Furthermore, natural deduction is shown to be complete.