|Abstract:||Term-generic first-order logic, or simply generic first-order logic (GFOL), is presented as a first-order logic parameterized with terms defined axiomatically (rather than constructively), by requiring them to only provide generic notions of free variable and substitution satisfying reasonable properties. A complete Gentzen deduction system is given, as well as complete equational and many-sorted extensions. It is shown that various calculi with binding, such as lambda-calculus and System F, can be faithfully defined as GFOL theories. Since GFOL is complete, by defining a logic or calculus as a GFOL theory one gets, at no additional effort, a semantics for that logic or calculus. A fragment of GFOL called Horn^2 is also defined, on whose theories, under certain conditions, the generic Gentzen deduction system is equivalent to a simplified deduction system which resembles the derivation system of the calculi that we intend to explicitly capture. Consequently, GFOL and especially its fragment Horn^2 can serve as a foundationaldefinitional framework for other calculi and logics, providing these with models and complete deduction.