Formalization of Lambda Calculus with Explicit Names as a Nominal Reasoning Framework

We formalize the metatheory of lambda calculus in Coq, in its classic form with explicit names. The formalization is founded upon an intuitive \(\alpha \) -equivalence definition without substitution or name swapping. Furthermore, we provide structural and rule induction principles that encapsulate the Barendregt Variable Convention, enabling formal proofs mirroring informally-styled ones. These principles are leveraged to establish foundational results such as the Church-Rosser theorem. Demonstrating the framework’s utility, we extend first-order logic with predicate definitions, ensuring its soundness through properties obtained from the metatheory by encoding propositions as lambda terms.