Failure of Cartesian closedness in NF

Extract

On any reasonable definition of functions, neither the category of sets nor the category of small categories is cartesian closed in New Foundations (NF). The latter category is sometimes proposed as a foundation for category theory since it is among its own objects. Our result shows it is a poor one.

In NF, as in other set theories, a "function" f from a set A to a set B is defined to be a set f of ordered pairs 〈x, y〉 with x in A and y in B, such that (a) if 〈x, y〉 ∈ f and 〈x, y′〉 ∈ f then y = y′, and (b) for every x in A there is some y in B with 〈x, y〉 ∈ f. But in NF different definitions of ordered pairs give significantly different functions. I say a reasonable definition must give:

1. The formula z = 〈x, y〉 is stratifiable.

2. For every set S there is a set {〈x, x〉 ∣ x ∈ S}.

3. If f is a function from A to B, and g one from B to C, there is a set {〈x, z〉∣(∃y)〈x, y〉∈ f & 〈y, z〉∈ g}.

Principles 2 and 3 are needed for identity functions and composites. By principle 1, any sets A and B have a set A × B of all ordered pairs 〈x, y〉 with x in A and y in B, but it does not follow that functions exist making A × B a categorical product of A and B.