  is an example of a stratified theorem of first-order logic that has stratified proofs but no stratified cut-free proofs. Crabbé [1991], [1994] has given two proofs of the fact that SF (NF with extensionality dropped altogether) admits cut-elimination. The connections with type theory make constructive versions of NF an obvious target for investigation, but nothing publishable has emerged so far. The only known proof (Specker’s) of the axiom of infinity in NF has too little constructive content to allow a demonstration that INF (NF with a constructive instead of classical ambient logic) admits an implementation of Heyting arithmetic, but opinion is divided on whether or not this tells us that INF is significantly weaker than NF. 