Oh, actually, I would say that NF is not an instance of the “parametric polymorphism trick”, but yet something else and much stranger that we don’t understand nearly as well. NF’s motivation is very much related, but—this is very fuzzy, but models of NFU seem to have to use much deeper logical trickery than the examples I was talking about, and it seems from my amateurish perspective that the reason is that NF “crosses levels” in stronger ways than the basic parametric polymorphism trick. Also, I’ve tried in the past to apply the trick to find simpler models of NFU and failed completely, though that’s very weak evidence.
Oh, actually, I would say that NF is not an instance of the “parametric polymorphism trick”, but yet something else and much stranger that we don’t understand nearly as well. NF’s motivation is very much related, but—this is very fuzzy, but models of NFU seem to have to use much deeper logical trickery than the examples I was talking about, and it seems from my amateurish perspective that the reason is that NF “crosses levels” in stronger ways than the basic parametric polymorphism trick. Also, I’ve tried in the past to apply the trick to find simpler models of NFU and failed completely, though that’s very weak evidence.