Five Axioms of Alpha-Conversion

We present five axioms of name-carrying lambda-terms identified up to alpha-conversion, that is, up to renaming of bound variables. We assume constructors for constants, variables, application and lambda abstraction. Other constants represent a function Fv that returns the set of free variables in a term and a function that substitutes a term for a variable free in another term. Our axioms are: (1) equations relating Fv and each constructor; (2) equations relating substitution and each constructor; (3) alpha-conversion itself; (4) unique existence of functions on lambda-terms defined by structural iteration; and (5) construction of lambda-abstractions given certain functions from variables to terms. By building a model from de Bruijn’s nameless lambda-terms, we show that our five axioms are a conservative extension of HOL. Theorems provable from the axioms include distinctness, injectivity and an exhaustion principle for the constructors, principles of structural induction and primitive recursion on lambda-terms, Hindley and Seldin’s substitution lemmas, and the existence of their length function. These theorems and the model have been mechanically checked in the Cambridge HOL system.