Constructive NF

Thomas Forster, University of Cambridge. Part of the Logic Seminar Series.

Quine's NF is known to prove the existence of infinite sets and to thereby support an interpretation of Peano Arithmetic.  

INF is its constructive fragment (same nonlogical axioms, weaker logic) and proves that the universal set is not Kuratowski-finite.  However its strength is not well constrained.  

The proof of the axiom of infinity does not appear to have enough constructive content to support an implementation of Heyting Arithmetic; on the other hand the obvious strategy of showing INF to be strong by means of a Powell-style negative interpretation into the classical theory is sabotaged by illfoundedness.

There remains the tantalising possibility of a (realizability-inspired) proof of Con(INF) that is radically different from Holmes' terrifying proof of the consistency of the classical theory to be revealed later the same day.