We present abstraction logic, a foundation for formal mathematics and interactive theorem proving that combines the single mathematical universe of first-order logic with the general variable binding facility of higher-order logics. Its terms coincide with those of second-order equational logic, but its restriction to the unityped case yields a general and complete logic with elementary semantics. Abstraction logic can naturally express a wide range of other logics while forming a coherent whole and remaining closer to informal mathematics.