Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters (Q884953)

The author introduces two systems \(\mathbf{G}[\beta]\) and \(\mathbf{G}_{\text{ext}}[\beta]\) which are equivalent to the equational calculi based on the usual \(\lambda\) calculus with \(\beta\) reduction and \(\beta\eta\) reduction, respectively. The key difference is that the \(\beta\) reduction \((\lambda x.t)s = t[x/s]\) is replaced by two rules: \[ \frac{ t[x/r]p_1\cdots p_n = s}{ (\lambda x.t)rp_1\cdots p_n = s} [\beta_l] \quad \frac{t = s[x/r]p_1\cdots p_n}{t = (\lambda x.s)rp_1\cdots p_n} [\beta_r] \quad (n \geq 0). \] For the new systems, the elimination of transitivity of equality is shown. From this result, several standard theorems about \(\beta\) and \(\beta\eta\) reductions are concluded in a new and simple way, as the Church-Rosser theorem for \(\beta\) and \(\beta\eta\) reductions, the Standardization theorem for \(\beta\) reduction and the Normalization and Postponement of \(\eta\) reduction theorems for \(\beta\eta\) reduction.