A SCHEMATIC PROOF OF STRONG NORMALIZATION FOR THE SYSTEMS OF THE $\lambda$-CUBE*

Abstract

This paper describes a set-theoretical argument for proving Strong Normalization (SN) for the systems of the so-called $\lambda$-cube. The argument is relatively simple and, moreover, flexible. It can be adapted to extensions of the systems considered, such as additional sorts, inductive types or sub-types.