Thomas Forster (Cambridge)
Constructive NF
The classical version of Quine's set theory NF is known to be strong but not known to be consistent. The strength emerges in some highly bizarre proofs (Of the axiom of infinity and the negation of the axiom of choice) and it is not clear what their constructive content is. Naturally one wonders about the status of the constructive version of the theory. Is there perhaps an easy proof of its consistency, perhaps using realizability ideas arising from Specker's equiconsistency for NF and version of typed set theory?
Nothing of any significance has been published on constructive NF, and this paper is the result of my attempts to prepare - in collaboration with Randal Holmes - a background survey paper which would be useful to people thinking of working on this topic.