Systems of combinatory logic related to Quine's `New Foundations' (Q809994)

The author introduces a weak system of pure combinatory logic to which are added pairing operators and an equality function. This is made part of a first-order logic with (the combinatory) equality and is called TRC. A variant TRCU of this allows for the presence of ``ur-elements''. The author is able to define a weak form of bracket abstraction in TRC which requires that all occurrences of a variable to be abstracted can be assigned a certain common ``type'', and for a restricted class of terms, any common ``type''. While TRC is of some interest in itself, it comes as a surprise to find that Quine's set theory ``New Foundations'' can be shown to be equivalent in strength to TRC. In a similar way TRCU is shown to be equivalent to the fragment \(NFU+Infinity\) of NF as described by Jensen. The consistency of \(NFU+Infinity\) related to ZFC is known, the question of the consistency of NF remains open, but this work may provide a new means of answering the question.