Analytic proof systems for λ-calculus:the elimination of transitivity, and why it matters

ABSTRACT. We introduce new proof systems G[β] and G_ext[β], which are equivalent to the standard equational calculi of λβ- and λβη-conversion, and which may be qualified as ‘analytic’ because it is possible to establish, by purely proof-theoretical methods, that in both of them the transitivity rule admits effective elimination. This key feature, besides its intrinsic conceptual significance, turns out to provide a common logical background to new and comparatively simple demonstrations — rooted in nice proof-theoretical properties of transitivity-free derivations — of a number of well-known and central results concerning β- and βη-reduction. The latter include the Church–Rosser theorem for both reductions, the Standardization theorem for β-reduction, as well as the Normalization (Leftmost reduction) theorem and the Postponement of η-reduction theorem for βη-reduction.