Normalization without reducibility Original Research Article

In Gallier (Ann. Pure Appl. Logic 91 (1998) 231–270), general results (due to Coppo and Dezani, Arch. Math. Logic 19 (1978) 139–156; Coppo et al., Z. Math. Log. Grund. Math. 27 (1981) 45–58) relating properties of pure λ terms and their typability in some systems with conjunctive types DΩ and D are proved in a uniform way by using the reducibility method. This paper gives a very short proof of the same results (actually, one of them is a bit stronger) using purely arithmetical methods.