An excellent proposal for a natural-deduction-based set-theoretic semantics for category theory is presented. In the natural deduction logic NaDSet, only joint denial (neither nor) operators ↓ and universal quantifiers ∀ are used as the primitive constructs. A set of logical rules for the sequent calculus are defined. The existential quantifier ∃ and other logical connectives ∧, ∨, and ⊃ can then be defined, and the corresponding deduction rules can be derived. The logic and its corresponding set theory are natural extensions of Tarski semantics, and they are used as the basis for constructing the notions of categories and functors. The approach avoids the paradoxes in conventional set theory. On the other hand, it has no constraints against self-membership or self-reference. For example, it can be derived that the category of categories and the category of functors are themselves members of the set of categories. There is no need to distinguish between small and large categories. No additional existence assumption is required. Other useful constructs such as opposites, product categories, comma categories, universals, limits, and adjoints can also be defined.

The authors present a promising picture of this remarkable approach. Readers can be excused for being cautious, however. Why can the constraints on conventional set theory be relaxed and the paradoxes solved without newly imposed conditions? Is any tradeoff necessary, and does this otherwise outstanding approach have any limitations?