Abstract

This paper extends the results of an earlier paper by the author . New subsystems of the combinatory logic TRC shown in that paper to be equivalent to NF are introduced; these systems are analogous to subsystems of NF with predicativity restrictions on set comprehension introduced and shown to be consistent by Crabbé. For one of these systems, an exact equivalence in consistency strength and expressive power with the analogous subsystem of NF is established