# zbMATH — the first resource for mathematics

$$\lambda \rho$$-calculus. II. (English) Zbl 1280.03016
Summary: In Part I [Bull. Sect. Log., Univ. Łódź, Dep. Log. 31, No. 2, 65–70 (2002; Zbl 1036.03011)], the author introduced the system $$\lambda \rho$$-calculus and stated without proof that the strong normalization theorem holds. Here we introduce a lemma (Lemma 4.10) and use it to prove the strong normalization theorem. While a typed $$\lambda$$-term itself is a derivation of the natural deduction for intuitionistic implicational logic, a typed $$\lambda \rho$$-term itself is a derivation of the natural deduction for classical implicational logic. Our system is simpler than the implicational fragment of M. Parigot’s $$\lambda \mu$$-calculus (cf. [Lect. Notes Comput. Sci. 624, 190–201 (1992; Zbl 0925.03092)]).

##### MSC:
 03B40 Combinatory logic and lambda calculus 03B05 Classical propositional logic
Full Text: