Equivalences between pure type systems and systems of illative combinatory logic (Q2565990)

In continuation of the paper [``Pure type systems with more liberal rules'', J. Symb. Log. 66, No. 4, 1561--1580 (2001; Zbl 0997.03014)], the authors introduce Systems of Illative Combinatory Logic equivalent to the four Pure Type Systems PTS, APTS, SPTS, and SAPTS, introduced in the paper mentioned above. Properties of the Systems of Illative Combinatory Logic as well as the equivalences are proven in full detail.